Skip to content
Snippets Groups Projects
  1. May 24, 2013
  2. May 23, 2013
  3. Jan 30, 2013
  4. Jan 24, 2013
  5. Jan 21, 2013
  6. Jan 18, 2013
  7. Jan 09, 2013
  8. Oct 25, 2012
  9. Jun 12, 2012
  10. Apr 12, 2012
  11. Feb 08, 2012
  12. Jan 27, 2012
  13. Jan 26, 2012
  14. Jan 25, 2012
  15. Jan 05, 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 21, 2011
  18. Dec 14, 2011
    • Julien Signoles's avatar
      [e-acsl] license · b8237817
      Julien Signoles authored
      [e-acsl] do not stop anymore when detecting an invalid/unsupported annotation
      [e-acsl] tests for invalid quantifications
      b8237817
  19. 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
  20. Nov 25, 2011
  21. Oct 04, 2011
  22. Sep 26, 2011
  23. Jun 01, 2011
  24. May 24, 2011
    • Julien Signoles's avatar
      [e-acsl] support of requires in stmt contracts · 83d441a0
      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
      83d441a0
  25. Mar 30, 2011
  26. Mar 24, 2011
  27. Mar 22, 2011
  28. Mar 17, 2011
  29. Mar 04, 2011
  30. Mar 02, 2011
  31. Feb 22, 2011
  32. Feb 21, 2011
Loading