Commits · a85779b066bca7b4a8361863fbb829ca522d7731 · pub / frama-c

Oct 04, 2011
- [E-ACSL] fix Makefile bug · a85779b0
  Julien Signoles authored 13 years ago
  
  a85779b0
Oct 03, 2011
- update according to better precision of value analysis · 597159cd
  Julien Signoles authored 13 years ago
  
  597159cd
Sep 29, 2011
- updating oracles according to kernel changes · f9cff19d
  Julien Signoles authored 13 years ago
  
  f9cff19d
Sep 26, 2011
- bug fixed in Makefile + small improvment in configure · aa2217a4
  Julien Signoles authored 13 years ago
  
  aa2217a4
Sep 22, 2011
- use correct kf when adding annotations in visitor + upgrade oracles · 8d4b5e0f
  Virgile Prevosto authored 13 years ago
  
  8d4b5e0f
Sep 13, 2011
- update according to change of Value's message · 6b93bd9e
  Julien Signoles authored 13 years ago
  
  6b93bd9e
Aug 23, 2011
- Update according to kernel changes. Some oracles still broken (see comment in Env.add_assert) · 3476e2d7
  Julien Signoles authored 13 years ago
  
  3476e2d7
Jul 04, 2011
- e-acsl todo · 6396713b
  Julien Signoles authored 13 years ago
  
  6396713b
- [e-acsl] svn ignore · 367827fc
  Julien Signoles authored 13 years ago
  
  367827fc
Jul 01, 2011
- [e-acsl] improve handling of integer division and modulo · 6cb99627
  Julien Signoles authored 13 years ago
  
  6cb99627
Jun 30, 2011
- [e-acsl] handle acsl subtyping relation. · 2746b0e2
  Julien Signoles authored 13 years ago
  
  2746b0e2
Jun 29, 2011

[e-acsl] fixed bug with casts from integer to integral C type · fc6c62e2

Julien Signoles authored 13 years ago

[e-acsl] support of field accesses in logic
[e-acsl] support of array accesses (yet missing guards) in logic
[e-acsl] support of pointer dereferences (yet missing guards) in logic
[e-acsl] support of \null in logic

fc6c62e2

Jun 15, 2011
- Fixed Big_int compatibility · 9fc266a3
  Benjamin Monate authored 13 years ago
  
  9fc266a3
Jun 09, 2011
- e-acsl TODO · 13011535
  Julien Signoles authored 13 years ago
  
  13011535
Jun 01, 2011
- update according to kernel changes + -warn-error · aeb13566
  Julien Signoles authored 13 years ago
  
  aeb13566
May 26, 2011
- RIP parameters.ml* · 8a5a907a
  Julien Signoles authored 13 years ago
  
  8a5a907a
- [e-acsl] comment · 57e15850
  Julien Signoles authored 13 years ago
  
  57e15850
- [e-acsl] convert annotations into C code in the right project · 2d9728a5
  Julien Signoles authored 13 years ago
  
  2d9728a5
- [e-acsl] fix bugs of sharing between the old AST and the new one · 0acd43ee
  Julien Signoles authored 13 years ago
  
  0acd43ee
May 25, 2011
- [e-acsl] Fixing bug in handling of statement contracts (duplication of blocks) · 7d0e9489
  Virgile Prevosto authored 13 years ago
  
  7d0e9489
- [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