- Aug 02, 2017
-
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
- Apr 12, 2017
-
-
Virgile Prevosto authored
-
- Aug 31, 2016
-
-
Boris Yakobowski authored
-
- Jun 09, 2016
-
-
Julien Signoles authored
- add some missing cases in the new one - fixes several bugs - still all the test cases are not ok
-
- Feb 11, 2016
-
-
Julien Signoles authored
-
- Jan 29, 2015
-
-
Julien Signoles authored
-
- Mar 24, 2014
-
-
Julien Signoles authored
-
- Mar 14, 2014
-
-
Julien Signoles authored
-
- Mar 07, 2014
-
-
Julien Signoles authored
-
- Apr 24, 2013
-
-
Julien Signoles authored
-
- Apr 19, 2013
-
-
Julien Signoles authored
[E-ACSL] prevent RTE while executing memory-related constructs
-
- Jan 30, 2013
-
-
Julien Signoles authored
-
- Nov 23, 2012
-
-
Julien Signoles authored
-
- Jan 19, 2012
-
-
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 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
-
Julien Signoles authored
[e-acsl] tests now independent of GMP version (but GMP still required)
-
- Aug 23, 2011
-
-
Julien Signoles 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)
-
- Feb 22, 2011
-
-
Julien Signoles authored
-
- Feb 21, 2011
-
-
Julien Signoles authored
-