Commits · 84aedec868d15cb2cb20cea2d739ee79a5b066ab · pub / frama-c · GitLab

Snippets Groups Projects

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
Jun 27, 2012
- [e-acsl] continue to convert other pre-/post-conditions when one fails · b81e92fe
  Julien Signoles authored 12 years ago
  
  [e-acsl] improve test of function contract
  b81e92fe
Jun 26, 2012
- [e-acsl] do not keep unused specified functions · 214eb122
  Julien Signoles authored 12 years ago
  
  214eb122
Jun 12, 2012
- [e-acsl] synchronizing with trunk + trying to fix share directory issue · 1094023d
  Julien Signoles authored 12 years ago
  
  1094023d
Apr 27, 2012
- [e-acsl] better specs for gmp functions · cce7ffe8
  Julien Signoles authored 12 years ago
  
  cce7ffe8
Apr 23, 2012
- [E-ACSL] update tests according to Value's changes · 3bb699eb
  Julien Signoles authored 12 years ago
  
  3bb699eb
Apr 12, 2012
- - Code independent of the location of directory 'share' · 2b2cb21e
  Julien Signoles authored 12 years ago
  
  - Fixed Makefile's bug
  2b2cb21e
- [E-ACSL] tests ok again thanks to -e-acsl-share · 233eb82a
  Julien Signoles authored 12 years ago
  
  233eb82a
Feb 21, 2012
- FRAMAC_VERSION is defined by main configure.ac, no need to do it here · 4ae521f6
  Virgile Prevosto authored 13 years ago
  
  4ae521f6
Feb 08, 2012
- [e-acsl] update according to kernel changes · a056124f
  Julien Signoles authored 13 years ago
  
  a056124f
Jan 27, 2012
- [e-acsl] extend test lazy.i since value analysis' bug #1072 is now fixed · 57989975
  Julien Signoles authored 13 years ago
  
  57989975
- [e-acsl] fix unexpected interaction with Frama-C compilation when compiling it... · 3210d06e
  Julien Signoles authored 13 years ago
  
  [e-acsl] fix unexpected interaction with Frama-C compilation when compiling it with --enable-external
  3210d06e
Jan 26, 2012
- [e-acsl] fixed install problem · 9f21e737
  Julien Signoles authored 13 years ago
  
  9f21e737