Skip to content
  • 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