- Jan 26, 2012
-
-
Julien Signoles authored
-
- Jan 25, 2012
-
-
Julien Signoles authored
-
- Jan 05, 2012
-
-
Julien Signoles authored
-
Julien Signoles authored
-
- Dec 28, 2011
-
-
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
-
- Dec 21, 2011
-
-
Julien Signoles authored
-
- Dec 14, 2011
-
-
Julien Signoles authored
[e-acsl] do not stop anymore when detecting an invalid/unsupported annotation [e-acsl] tests for invalid quantifications
-
- Dec 07, 2011
-
-
Julien Signoles authored
[e-acsl] universal quantifiers over integers. Not yet finished: work only in some cases [e-acsl] logic variables (required by univ quantif)
-
- Nov 25, 2011
-
-
Julien Signoles authored
[e-acsl] tests now independent of GMP version (but GMP still required)
-
- Oct 04, 2011
-
-
Julien Signoles authored
-
- Sep 26, 2011
-
-
Julien Signoles authored
-
- Jun 01, 2011
-
-
Julien Signoles authored
-
- May 24, 2011
-
-
Julien Signoles authored
[e-acsl] support of assumes without ensures in stmt contracts [e-acsl] partial support of function contracts (the same subset than stmt contracts) [e-acsl] additional test for nested code annotation [e-acsl] code refactoring: visit.ml splitten into several compilation units
-
- Mar 30, 2011
-
-
Virgile Prevosto authored
-
- Mar 24, 2011
-
-
Julien Signoles authored
-
Julien Signoles authored
-
Virgile Prevosto authored
-
- Mar 22, 2011
-
-
Julien Signoles authored
[e-acsl] Makefile's target 'install' [e-acsl] test GMP linkage in non-regression suite ('make tests' now requires GMP >= 4.3.2) [e-acsl] fixed bugs of GMP compatibility
-
- Mar 17, 2011
-
-
Julien Signoles authored
- [Makefile] better generation of local_config.ml - [Options] new options for customized code generation (unused yet)
-
Julien Signoles authored
-
- Mar 04, 2011
-
-
Julien Signoles authored
- generated C headers in a separate file "share/e_acsl.h" - fixed generation for Pnot - some additional tests
-
- Mar 02, 2011
-
-
Julien Signoles authored
-
- Feb 22, 2011
-
-
Julien Signoles authored
-
Julien Signoles authored
-
- Feb 21, 2011
-
-
Julien Signoles authored
-