Skip to content
Snippets Groups Projects
  1. Aug 07, 2014
  2. Aug 04, 2014
  3. Mar 24, 2014
  4. Mar 14, 2014
  5. Mar 07, 2014
  6. Sep 25, 2013
  7. Sep 23, 2013
  8. Sep 04, 2013
  9. Jul 18, 2013
  10. May 24, 2013
  11. Jan 30, 2013
  12. Nov 23, 2012
  13. Feb 21, 2012
  14. Jan 24, 2012
  15. Jan 23, 2012
  16. 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
  17. Dec 07, 2011
    • Julien Signoles's avatar
      [e-acsl] update headers · b1f8150d
      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)
      b1f8150d
  18. Nov 25, 2011
  19. Sep 26, 2011
  20. Mar 22, 2011
  21. Mar 17, 2011
  22. Feb 21, 2011
Loading