The packaged version of this release, which omits many inessential subdirectories, is available at
http://vst.cs.princeton.edu/download/vst-2.1.tgz.
It is compatible with CompCert 3.2 and Coq 8.7.0, 8.7.1, 8.7.2, 8.8.0.
Changes since version 2.0:
-
hint tactic, makes suggestions about what Verifiable C tactic to apply (see "Hint" chapter of VC.pdf)
-
Require Import VST.floyd.functional_base.
If you have a theory file containing a pure functional model WITHOUT separation logic but WITH the theory of CompCert Integers, and you want to use a lot of relevant Floyd tactics and lemmas without having to import all of VST.floyd.proofauto, you can import this file instead. -
Various efficiency improvements in forward, forward_call, entailer, with_library, make_compspecs, make_varspecs.
-
No holes in the proof: The entire VST development up to VST.floyd.proofauto is now proved without any axioms, assumptions, admitted lemmas, etc. except for some standard axioms: extensionality, proof irrelevance, excluded middle, and (for use by CompCert's floating-point stuff) a lengthy axiomatization of the real numbers.
-
Private global variables: better encapsulation of modules that use private extern (or static) variables: see the chapter "gvars: Private global variables" in the reference manual (VC.pdf).
-
Ramification tactics, for more flexible framing than the ordinary freezer or frame rule: tactics localize, unlocalize; documentation to follow.
-
Magic wand as frame: new library of lemmas and tactics, documentation to follow (but see the hash-table exercise).
-
Concurrency with ghost state: Verifiable C now supports shared-memory concurrent programming with ghost state in the form of (for example) partial commutative monoids. Documentation to follow.
-
Overhaul of the control-flow tactics: forward_for deprecated, forward_if more intelligent, forward_loop very capable. See the reference manual chapters "If, While, For" and "For loops (general iterators)" .
-
Improved rep_omega tactic, which is a more powerful replacement for the previous repable_signed tactic. See chapter "rep_omega".
-
Fixed issues: 48, 90, 107, 113, 120, 133, 134, 136, 142, 145, 147, 148, 159, 162, 187.