Commits · 0bd1a084749d45c007095ff893b7cbd6268aeabd · pub / frama-c

Nov 28, 2012

[E-ACSL] fixed bug #1317 about \valid("literal_string") · 0bd1a084

Julien Signoles authored 12 years ago

[E-ACSL] prevent runtime errors in annotations (all of them)
[E-ACSL] fixed bug in interpretation of \valid(\at(...))
[E-ACSL] fixed bug in interpretation of locals in blocks involved in memory model

0bd1a084

fixed bug #1319 · 87b4c33e
Guillaume Petiot authored 12 years ago

87b4c33e

Nov 27, 2012
- [E-ACSL] optimizing tests again · 2ed5e442
  Julien Signoles authored 12 years ago
  
  2ed5e442
- [E-ACLS] optimize test procedure · f31ec064
  Julien Signoles authored 12 years ago
  
  f31ec064
Nov 26, 2012
- [E-ACSL] oracle bugfixes · af3d0770
  Guillaume Petiot authored 12 years ago
  
  af3d0770
- [E-ACSL] update according to kernel's change. Still remain to fix GP's invalid commit r20854 · 860fd6a8
  Julien Signoles authored 12 years ago
  
  860fd6a8
- + fix _valid_read · a0f8d8c2
  Guillaume Petiot authored 12 years ago
  
  a0f8d8c2
Nov 23, 2012
- [E-ACSL] add configure's dependencies · 131b3ad9
  Julien Signoles authored 12 years ago
  
  131b3ad9
- [E-ACSL] fixed bug #1307 (again) · 3b0bbdc6
  Julien Signoles authored 12 years ago
  
  3b0bbdc6
- [E-ACSL] use RTE to prevent arithmetic runtime errors in the generated code for non GMP expressions · 7c8a2a8b
  Julien Signoles authored 12 years ago
  
  7c8a2a8b
- [E-ACSL] Update for commit 20821 · 382c3f8b
  Boris Yakobowski authored 12 years ago
  
  382c3f8b
- [E-ACSL] fixed bug with global literal strings · 14a99a47
  Julien Signoles authored 12 years ago
  
  14a99a47
Nov 22, 2012
- [E-ACSL] generate initialization of globals in a separated function · 84aedec8
  Julien Signoles authored 12 years ago
  
  84aedec8
Nov 21, 2012
- [E-ACSL] add missing oracle · d139dce7
  Julien Signoles authored 12 years ago
  
  d139dce7
- [E-ACSL] compatibility with recent AST's change about LReal · 09bdef38
  Julien Signoles authored 12 years ago
  
  09bdef38
Nov 19, 2012
- [E-ACSL] add test for bug #1307 · 5773603a
  Julien Signoles authored 12 years ago
  
  5773603a
- [E-ACSL] support of float in specification. Reals are approximated by float. · dbb4f7a6
  Julien Signoles authored 12 years ago
  
  [E-ACSL] fixed bug #1307 (typing crash in presence of reals) [E-ACSL] fixed bug in the pre-analysis on function call [E-ACSL] fixed bug with non-integer operators with a GMP operand
  dbb4f7a6
Nov 16, 2012
- [E-ACSL] do not crash anymore when there is no main entry point · d130f453
  Julien Signoles authored 12 years ago
  
  d130f453
- [E-ACSL] do not crash anymore on unsupported features in the preliminary static analysis · 60dab7ed
  Julien Signoles authored 12 years ago
  
  60dab7ed
Nov 15, 2012
- [E-ACSL] fully fixed bug #1304 · 1565534f
  Julien Signoles authored 12 years ago
  
  [E-ACSL] fixed bug with array as argument of functions
  1565534f
Nov 14, 2012
- [E-ACSL] fixed first part of bug #1304 : call _initialize instead of _full_init... · 1a5ff2d0
  Julien Signoles authored 12 years ago
  
  [E-ACSL] fixed first part of bug #1304: call _initialize instead of _full_init for left-values which are not variables
  1a5ff2d0
- [E-ACSL] update according to Value's changes · fb643d36
  Julien Signoles authored 12 years ago
  
  fb643d36
Nov 07, 2012
- [E-ACSL] fixed typing bug with field access · f735d6dc
  Julien Signoles authored 12 years ago
  
  [E-ACSL] fixed bug #1298 about \valid(v) when v is a formal
  f735d6dc
Nov 06, 2012
- [e-acsl] remove last GP's · 0de9dde2
  Julien Signoles authored 12 years ago
  
  0de9dde2
- [e-acsl] fixed bug #1297 about \valid in contracts · daa4b67f
  Julien Signoles authored 12 years ago
  
  daa4b67f
- [e-acsl] update TODO-list · c0405399
  Julien Signoles authored 12 years ago
  
  c0405399
- [e-acsl] do not generate calls to 'initialize' after the annotations which require them · a11f9105
  Julien Signoles authored 12 years ago
  
  a11f9105
- [e-acsl] fixed bug #1296 about deallocation of local variables · 096c40e4
  Julien Signoles authored 12 years ago
  
  096c40e4
- [e-acsl] update refman according to ACSL 1.6 · 8296e423
  Julien Signoles authored 12 years ago
  
  8296e423
- [E-ACSL] update implementation manual according to Guillaume's works · 6466afdc
  Julien Signoles authored 12 years ago
  
  6466afdc
- moving E-ACSL reference manual from trunk to plugins/e-acsl · 4718c650
  Julien Signoles authored 12 years ago
  
  4718c650
- [e-acsl] update changelog · f874a3ed
  Julien Signoles authored 12 years ago
  
  f874a3ed
Nov 05, 2012
- [E-ACSL] update according to kernel's changes · cc7c4a2d
  Julien Signoles authored 12 years ago
  
  cc7c4a2d
Oct 29, 2012
- [E-ACSL] platform-independent oracles · 857f9f4f
  Julien Signoles authored 12 years ago
  
  857f9f4f
- fixes OCaml 4.00 compilation · 7a1af4ad
  Virgile Prevosto authored 12 years ago
  
  7a1af4ad
Oct 25, 2012
- [e-acsl] merging the e-acsl-mmodel branch into the main branch · 2821b923
  Julien Signoles authored 12 years ago
  
  2821b923
Sep 13, 2012
- change translation of constants according to kernel changes · 5289a95e
  Julien Signoles authored 12 years ago
  
  5289a95e
Sep 07, 2012
- [E-ACSL] fixing oracles · f73e5cf7
  Julien Signoles authored 12 years ago
  
  f73e5cf7
Aug 07, 2012
- ocaml 4.00 compatibility + cleanup unused code · 07eb99e5
  Virgile Prevosto authored 12 years ago
  
  07eb99e5
Jul 20, 2012
- remove incorrect tests about sizeof(literal_string) · aae80256
  Julien Signoles authored 12 years ago
  
  aae80256