Commits · 22f35ea3681569292b2ebea2963775f09eb16711 · pub / frama-c

Mar 07, 2014
- preparing release 0.4 compatible with Neon · 22f35ea3
  Julien Signoles authored 11 years ago
  
  22f35ea3
Sep 25, 2013
- [E-ACSL] again compatible with the trunk and no more with Fluorine · aa5f7cf6
  Julien Signoles authored 11 years ago
  
  aa5f7cf6
Sep 23, 2013
- [E-ACSL] ready for v0_3 · 565aff54
  Julien Signoles authored 11 years ago
  
  565aff54
May 27, 2013
- [E-ACSL] version 0.2 ready to be released · eec72901
  Julien Signoles authored 11 years ago
  
  eec72901
Jan 13, 2012
- [e-acsl] type system implemented. Yet unused and untested. · 621d615d
  Julien Signoles authored 13 years ago
  
  621d615d
Dec 28, 2011

[e-acsl] Hollydays works (now ready for alpha release): · b2009ccd

Julien Signoles authored 13 years ago

* 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