Commits · fde36fa19a557f45c17c0cd266fd87a4823e8e6d · pub / frama-c

May 25, 2011
- [e-acsl] use a function type instead of void when required · fde36fa1
  Julien Signoles authored 13 years ago
  
  fde36fa1
- [e-acsl] prevent to add twice a generated variable to the locals of a function · 3854f457
  Julien Signoles authored 13 years ago
  
  3854f457
- [e-acsl] do not generate block for only 1 stmt · b8b2338f
  Julien Signoles authored 13 years ago
  
  b8b2338f
- [e-acsl] fix one more bug with merging of environment · b30ae45b
  Julien Signoles authored 13 years ago
  
  b30ae45b
- [e-acsl] correctly add generated variables to locals of the visited function · 2c4dbe28
  Julien Signoles authored 13 years ago
  
  2c4dbe28
May 24, 2011

[e-acsl] support of requires in stmt contracts · 83d441a0

Julien Signoles authored 13 years ago

[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

May 18, 2011
- Propagate oracle from enum typing fix · acee652a
  Benjamin Monate authored 13 years ago
  
  acee652a
May 16, 2011
- Fixed oracle broken by kernel fix · 8ddd387d
  Benjamin Monate authored 13 years ago
  
  8ddd387d
May 13, 2011
- [e-acsl] a little bit more permissive for preconditions · 59225723
  Julien Signoles authored 13 years ago
  
  59225723
- [e-acsl] a little bit more permissive for preconditions · 78b39b31
  Julien Signoles authored 13 years ago
  
  78b39b31
- first step for support of statement/function contracts (statement ensures... · 21c18cf2
  Julien Signoles authored 13 years ago
  
  first step for support of statement/function contracts (statement ensures could work but yet untested)
  21c18cf2
May 12, 2011
- [e-acsl] little refactoring · 80b25403
  Julien Signoles authored 13 years ago
  
  80b25403
- [e-acsl] minor code+tests improvements · 144f42bb
  Julien Signoles authored 13 years ago
  
  144f42bb
- [e-acsl] support of all missing constants + add a missing oracle · fc491ce5
  Julien Signoles authored 13 years ago
  
  fc491ce5
- e-acsl code comments · 092ab753
  Julien Signoles authored 13 years ago
  
  092ab753
- explicitely mark as unimplement function contracts + overload vglob_aux instead of vglob · b2925f8b
  Julien Signoles authored 13 years ago
  
  b2925f8b
- [e-acsl] remove useless commented code · c7fd9476
  Julien Signoles authored 13 years ago
  
  c7fd9476
- [e-acsl] fixed bug for ! (not) · 678a99c8
  Julien Signoles authored 13 years ago
  
  [e-acsl] fixed bug for negative modulos [e-acsl] full reimplementation of environments (only one now, and it is persistent) [e-acsl] support of lazy operators &&, || and ==> [e-acsl] tests now execute the generated C code and check that no runtime assertion is raised
  678a99c8
May 11, 2011
- [e-acsl] simplifying Visit.New_block · 3d075af6
  Julien Signoles authored 13 years ago
  
  3d075af6
- [e-acsl] fixed broken previous commit · 40d0adc3
  Julien Signoles authored 13 years ago
  
  [e-acsl] add guard before divisions and modulos
  40d0adc3
- comment API of internal module Visit.New_vars + factorize code for CInt64 · 2552cff1
  Julien Signoles authored 13 years ago
  
  2552cff1
- [e-acsl] shorter name for generated variable · ea4fd21a
  Julien Signoles authored 13 years ago
  
  ea4fd21a
May 05, 2011
- update oracles according to changes of kernel message · 96fd47bd
  Julien Signoles authored 13 years ago
  
  96fd47bd
May 04, 2011
- svnignore ok again · 0ca5c947
  Julien Signoles authored 13 years ago
  
  0ca5c947
- global svn:ignore · 01dd3ae8
  Benjamin Monate authored 13 years ago
  
  01dd3ae8
May 03, 2011
- upgrade to new kernel API · 61b08f91
  Virgile Prevosto authored 13 years ago
  
  61b08f91
Apr 28, 2011
- updating oracles according to kernel changes · 0c776cdd
  Julien Signoles authored 13 years ago
  
  0c776cdd
Apr 22, 2011

- update tests according to new messages of Value · b76e04d6

Julien Signoles authored 13 years ago

- update TODO-list
- location for new constructs whenever possible
- additional warnings when guards are missing

b76e04d6

Apr 13, 2011
- \valid* now not implemented, update TODO · 4605b83e
  Julien Signoles authored 13 years ago
  
  4605b83e
Apr 06, 2011
- in tests, use @frama-c@, not a direct call to frama-c · 8dbbd674
  Virgile Prevosto authored 13 years ago
  
  8dbbd674
Apr 05, 2011
- [e-acsl] updating oracle according to kernel changes · d1b21266
  Julien Signoles authored 13 years ago
  
  d1b21266
Apr 04, 2011
- ptests works better when it has a result directory where it can put files · 6630a082
  Virgile Prevosto authored 13 years ago
  
  6630a082
Mar 30, 2011
- fix install target for use as internal plugin · 1ab0e818
  Virgile Prevosto authored 13 years ago
  
  1ab0e818
Mar 25, 2011
- updating according to changes in Frama-C kernel · edb12060
  Julien Signoles authored 14 years ago
  
  edb12060
Mar 24, 2011
- more readable Makefile · ef077987
  Julien Signoles authored 14 years ago
  
  ef077987
- posix 'make install' + make uninstall · 62c0e613
  Julien Signoles authored 14 years ago
  
  62c0e613
- fix install issue in internal plugin mode · 6946b797
  Virgile Prevosto authored 14 years ago
  
  6946b797
Mar 22, 2011

[e-acsl] implement options for direct linking with GMP · 3ec70885

Julien Signoles authored 14 years ago

[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

3ec70885

Mar 17, 2011
- fixed bug · d518b849
  Julien Signoles authored 14 years ago
  
  d518b849
- - [configure] search GMP sources · 1d86aa12
  Julien Signoles authored 14 years ago
  
  - [Makefile] better generation of local_config.ml - [Options] new options for customized code generation (unused yet)
  1d86aa12