Skip to content
Snippets Groups Projects
  1. Sep 23, 2013
  2. May 24, 2013
  3. Jan 04, 2012
  4. Dec 28, 2011
    • Julien Signoles's avatar
      [e-acsl] Hollydays works (now ready for alpha release): · b2009ccd
      Julien Signoles authored
      * fixes bug:
        - fixed bug in quantifications when the bound variable got C type
        - fixed bug with DEV_FLAGS in Makefile.in
      * implements new E-ACSL features:
        - invariant as assertion
        - existential quantification \exists over integers
        - equivalence <==>
        - \at as a predicate
        - conditional _ ? _ : _ (for terms and predicates)
        - binary boolean operations over terms
        - mixed assumes and ensures in function contracts
      * other new features:
        - better error messages when runtime checks fail 
          (replace e_acsl_fail by e_acsl_assert)
        - remove option -e-acsl-assert
        - add E-ACSL manuals in doc/manuals
        - add files doc/Changelog, INSTALL, README and VERSION
        - new option -e-acsl-version
        - check Frama-C version at configure
        - make src-distrib
        - header 2012
      b2009ccd
Loading