3 ms·
I'm glad that I wasn't the only persion pondering the similar thing (referring to the theses), but I'm not sure if the current direction can produce a small eno
by lifthrasiir 3y ago
I'm glad that I wasn't the only persion pondering the similar thing (referring to the theses), but I'm not sure if the current direction can produce a small enough solution. For example I expected the following to work even with the currently restricted xlib:
#include <stdlib.h>
foo(int **pp) [
if (@pp) {
.alloc *pp;
} else {
.undefined;
}
] {
*pp = malloc(4);
// or: int *qq = malloc(4); *pp = qq;
}
It seems that `*pp` doesn't even work in the abstraction. (I originally tried structs, but realized that Xr0 currently doesn't support them.) This is crucial because you can't just do pattern matching against abstractions and axioms, there should be some sort of tactics that massage abstractions so that appropriate axioms can be used if any. Even keeping track of non-variable places (here `*qq`) is not trivial, please consider how to handle the commented code.
- akiarie 3y agoAppreciate the thinking and tinkering. Xr0 has a long way ahead of it before we have a fully-consistent, reliable syntax and set of axioms. For one thing, we delayed implementing the dereference operator `*p` because we were focused on getting our basic model to work with loops (which led us to focus on the array-indexing syntax, e.g. `p[0]`). The below works, but I note that quite a few meaningless or incorrect permutations of the abstract work (and shouldn't). #include <stdlib.h> foo(void **pp) [ .alloc pp[0]; ] { void *q; q = malloc(4); pp[0] = q; }