Skip to content

VST version 2.1
Compare
Choose a tag to compare
@andrew-appel andrew-appel released this 19 Apr 12:03
· 2714 commits to master since this release
v2.1
755b868

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.

Assets 2
Loading