Andrew Appel
Andrew Appel
Invoking `clightgen --help` describes an option `-version-file` but invoking `clightgen -version-file foo` says `ccomp: error: Unknown option -version-file` (in CompCert 3.8). I am not advocating for restoring this option, I...
[in any recent version of VST such as 2.9, 2.10, master branch] Consider this program, ``` void f (struct foo {int x,y;} *p, unsigned i, unsigned n) { p[i].x =...
VST is formally proved sound w.r.t. the operational semantics of CompCert Clight. VST is _supposed to be sound_ for gcc and clang, but is not formally proved sound. In this...
The data_at predicate is defined in terms of the underlying mapsto predicate, which in turn is layered on address_mapsto: `res_predicates.address_mapsto: memory_chunk -> val -> share -> pred rmap.` `address_mapsto` defines...
In veric/superprecise.v there are several ill-maintained lemmas that are now Aborted or commented-out. They relate to the `superprecise` property of an mpred, which is a stronger version of the standard...
The lemma `semax_external_funspec_sub` in `veric/semax.v` is Admitted. There is a part at the end related to the aging of the ghost state. This should be fixed a.s.a.p., since it's part...
This line of Clightnotations.v does not work properly, `Notation "'for' ( s1 ; e ; s2 ) { s3 }" := (Sfor s1%print_stmt_for e%expr s3%C s2%print_stmt_for) ... : C_scope.` and...
On 12/15/2014 8:11 PM, [email protected] wrote: Just wanted to let you know that the [cont] directory makefile doesn’t seem to work as is on my system. I needed to add...
I installed the Windows-executable installer for the Coq Platform 2022.04 with Coq 8.15. In the dialog box for where to install it, I specified C:\Coq88, which is a directory that...
This is a more accurate description of issue #213 The Coq 8.14 and Coq 8.15 platform installs, on Windows, can fail if they are installed into a nonempty directory that...