Commits · 0a3fc3a71e37c611324e94a24a947a28f714be5a · pub / frama-c

Mar 28, 2014
- handle predicates \at in the same way than terms \at · 0a3fc3a7
  Julien Signoles authored 11 years ago
  
  0a3fc3a7
- still on the way of fixing bug #1717 · 655e541e
  Julien Signoles authored 11 years ago
  
  655e541e
- on the way of fixing bug #1717 · a30fab26
  Julien Signoles authored 11 years ago
  
  a30fab26
Mar 24, 2014
- fixing the header ('licenses' is not 'license') · 378f93e2
  Julien Signoles authored 11 years ago
  
  378f93e2
Mar 07, 2014
- applying headers 2014 · 524689f4
  Julien Signoles authored 11 years ago
  
  524689f4
Oct 25, 2013
- [E-ACSL] compatibility with warning 7 · d87c0496
  Julien Signoles authored 11 years ago
  
  d87c0496
Sep 25, 2013
- [E-ACSL] restore previous behavior of RTE's warnings · 6f69635b
  Julien Signoles authored 11 years ago
  
  6f69635b
- [E-ACSL] refactoring code about RTE · 9aff9588
  Julien Signoles authored 11 years ago
  
  9aff9588
Sep 10, 2013

[E-ACSL] update oracles according to Value changes · 8aa4fa00

Julien Signoles authored 11 years ago

[E-ACSL] improve ACSL contracts of its libraries
[E-ACSL] no more unknow locations in translation of quantifications

8aa4fa00

Sep 06, 2013
- [E-ACSL] loop invariants · f9dfde16
  Julien Signoles authored 11 years ago
  
  f9dfde16
Sep 05, 2013
- [E-ACSL] code factorisation which improves translation of ghost stmts · 1157b716
  Julien Signoles authored 11 years ago
  
  1157b716
Jun 21, 2013
- [E-ACSL] fewer unknown locations · 44bb94f0
  Julien Signoles authored 11 years ago
  
  44bb94f0
May 27, 2013
- [E-ACSL] rename __clean and e_acsl_global_init · 607e2e0c
  Julien Signoles authored 11 years ago
  
  607e2e0c
May 22, 2013
- [E-ACSL] fixing -e-acsl-check + manual · 4c354e56
  Julien Signoles authored 11 years ago
  
  4c354e56
- [E-ACSL] better handling of function without main + manual · 335960f5
  Julien Signoles authored 11 years ago
  
  335960f5
- [E-ACSL] better warnings + manual · 225b6812
  Julien Signoles authored 11 years ago
  
  225b6812
May 21, 2013
- [E-ACSL] fixed imprecise location on RTE generation + update oracles · e4360835
  Julien Signoles authored 11 years ago
  
  e4360835
May 17, 2013
- [E-ACSL] do not call __clean when not required + ongoing manual · 885730d0
  Julien Signoles authored 11 years ago
  
  885730d0
May 07, 2013
- [E-ACSL] fixed issue with extern ghost variable (definitively (?) fixed issue #1392 · 2490ce6d
  Julien Signoles authored 11 years ago
  
  2490ce6d
- [E-ACSL] update according to Value's printer changes · e79a5719
  Julien Signoles authored 11 years ago
  
  e79a5719
Apr 30, 2013

[E-ACSL] fixed bug #1411 · eec22888

Julien Signoles authored 11 years ago

[E-ACSL] fixed non-termination issue in presence of RTEs in RTE
[E-ACSl] pre-analysis: additional verbosing messages (level 4)

eec22888

Apr 25, 2013
- [E-ACSL] dataflow: fixed bug with function call when the returned value must be monitored · a13c858f
  Julien Signoles authored 11 years ago
  
  a13c858f
- [E-ACSL] more agressive inlining of conditional and initialized · 5ab779c2
  Julien Signoles authored 11 years ago
  
  5ab779c2
Apr 24, 2013
- [E-ACSL] reimplementing detection of RTE in annotations, RTE in GMP code still missing · c49e183b
  Julien Signoles authored 11 years ago
  
  c49e183b
Apr 23, 2013

[E-ACSL] faster initialization of the dataflow analysis · a1a09d0a

Julien Signoles authored 11 years ago

[E-ACSL] fixed bug with global declarations involved in the memory model (btw fixed but #1392)
[E-ACSL] additional feedback messages

a1a09d0a

Apr 22, 2013
- [E-ACSL] fixed incorrect previous commit :-( · 290d949b
  Julien Signoles authored 11 years ago
  
  290d949b
- [E-ACSL] fixed interprocedural dataflow analysis on function calls · 1c7363e6
  Julien Signoles authored 11 years ago
  
  1c7363e6
Apr 12, 2013
- [E-ACSL] new option -e-acsl-full-mmodel to monitor all pointers · 347c233b
  Julien Signoles authored 11 years ago
  
  347c233b
- [E-ACSL] restore compatibility with Frama-C kernel · 36586faf
  Julien Signoles authored 11 years ago
  
  36586faf
Mar 13, 2013
- fixed again according to kernel changes and fixed compatibility with the -no-obj mode · 5a0ab6a0
  Julien Signoles authored 12 years ago
  
  5a0ab6a0
- [E-ACSL] update according to kernel changes · fd5de66a
  Julien Signoles authored 12 years ago
  
  fd5de66a
Jan 30, 2013
- [E-ACSL] headers 2013 · 9a68d8fe
  Julien Signoles authored 12 years ago
  
  9a68d8fe
Jan 18, 2013
- [E-ACSL] new option -e-acsl-valid. Valid annotations are not translated by default anymore. · cde9885a
  Julien Signoles authored 12 years ago
  
  [E-ACSL] code of e_acsl_assert put in e_acsl.c (no more in e_acsl.h)
  cde9885a
Jan 09, 2013

[E-ACSL] handle specified function without code. BTW that fixes bugs #1300 and #1340. · f7a1cd74

Julien Signoles authored 12 years ago

[E-ACSL] convert postcondition even in presence of untranslated assigns clause
[E-ACSL] fix bug when the translation of a predicate containing \at is abruptely stopped because of a not-yet-implemented construct (the generated code contained undeclared __e_acsl_at variables)

f7a1cd74

Jan 04, 2013
- [E-ACSL] comments · c3ed4c2e
  Julien Signoles authored 12 years ago
  
  c3ed4c2e
Dec 20, 2012
- [E-ACSL] support of ghost variables and statements · f22c9a75
  Julien Signoles authored 12 years ago
  
  f22c9a75
Dec 19, 2012
- [E-ACSL] update according to kenel's changes · 33e5c8b7
  Julien Signoles authored 12 years ago
  
  33e5c8b7
Dec 05, 2012
- [E-ACSL] do not perform pre_analysis on E-ACSL's library files · bf19e6ff
  Julien Signoles authored 12 years ago
  
  bf19e6ff
- [E-ACSL] fixed bug #1324 with quantifications over integral types; more precise typing · c36e24ae
  Julien Signoles authored 12 years ago
  
  [E-ACSL] visit E-ACSL's library files slightly faster
  c36e24ae
Nov 30, 2012
- [E-ACSL] order of some generated instructions does not depend anymore on hash implementation · 39064bd0
  Julien Signoles authored 12 years ago
  
  39064bd0