Andrew Appel

That's all fine, but if you would like to document this within VST more permanently, I suggest: 1. Prune the example down to one file, progs/alias.c (with progs/verif_alias.v) 2. Add...

More questions: I presume you are testing your stuff with BITSIZE=32. Can you use size_t instead of int, therefore making your demonstration portable to BITSIZE=64 as well? (Or do I...

Sorry, in 64-bit C compilers, `long` is the same as `int`. If you want 64-bit integers, you have to say `long long`. Is that what you meant? Also, can you...

I found a second instance where this is necessary. In this case I'm trying to prove a particular general-purpose Hoare triple (semax) usable in many different functycontexts and/or compspecs, etc....

And also, similarly: in `solve_store_rule_evaluation`, add an @ to the change command as in: ``` change (@upd_reptype cs t gfs h0 h1 = rhs); ```

And similarly, in tactic `SEP_field_at_strong_unify` the cs argument should be made explicit: ``` | |- @data_at_ ?cs ?sh ?t ?p = _ /\ _ => change (@data_at_ cs sh t...

Not necessary to support 8.16. If you can support 8.18 and newer, that will be good enough for any release AFTER April of 2024, which will (presumably) be for a...

But please do support 32-bit mode.

Aside from the 32-bit question, how fast is the performance of VST-Floyd in this branch, compared to the master branch?

My most recent commit c4a2d30 brings @lennartberinger's recent proofs about VSU dry safety into the vst_on_iris branch, all commented out. I wonder how difficult it will be to uncomment and...