Commits · 4e793ff044003a26394e795ce7256d8f63f21003 · pub / frama-c

May 17, 2013
- [E-ACSL] fixed bug when upgrading unconstant long long expressions into GMP + ongoing manual · 4e793ff0
  Julien Signoles authored 11 years ago
  
  4e793ff0
- [E-ACSL] do not call __clean when not required + ongoing manual · 885730d0
  Julien Signoles authored 11 years ago
  
  885730d0
May 16, 2013
- [E-ACSL] userman is on the way · ed2cc51f
  Julien Signoles authored 11 years ago
  
  ed2cc51f
- [E-ACSL] detailled outline of user manual · 28f5eecc
  Julien Signoles authored 11 years ago
  
  28f5eecc
May 07, 2013
- [E-ACSL] analysis: fixed soundness bug when calling several times the same function · bbf3b0a0
  Julien Signoles authored 11 years ago
  
  bbf3b0a0
- [E-ACSL] analysis: fixed bug in presence of an alias with an explicit address · bfb9f650
  Julien Signoles authored 11 years ago
  
  bfb9f650
- [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
May 06, 2013
- [E-ACSL] known bugs · ecb68968
  Julien Signoles authored 11 years ago
  
  ecb68968
- [E-ACSL] start user manual · 0d55a223
  Julien Signoles authored 11 years ago
  
  0d55a223
Apr 30, 2013
- [e-acsl] useless loop deleted in function mask · 3d2cbc28
  Guillaume Petiot authored 11 years ago
  
  3d2cbc28
- [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 26, 2013
- [E-ACSL] dataflow: fixed bug in detecting variables of interest in annotations · 62c6da61
  Julien Signoles authored 11 years ago
  
  62c6da61
Apr 25, 2013
- [E-ACSL] monitor only pointers and arrays · 9390f2d1
  Julien Signoles authored 11 years ago
  
  9390f2d1
- [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
- [E-ACSL] dataflow optimisation: ignore duplicated function contract · 9f0b656a
  Julien Signoles authored 11 years ago
  
  9f0b656a
- [E-ACSL] do not monitor initialization of E-ACSL's generated variables · aacb7335
  Julien Signoles authored 11 years ago
  
  aacb7335
- [E-ACSL] simplified translation for \at(_,Here) · 2cb631d3
  Julien Signoles authored 11 years ago
  
  2cb631d3
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] improve test · fbbd4716
  Julien Signoles authored 11 years ago
  
  fbbd4716
- [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 19, 2013
- [E-ACSL] fixed bug #1398 about calling variadic functions · 99f261fe
  Julien Signoles authored 11 years ago
  
  99f261fe
- [E-ACSL] fixed bug #1399 about typing of index of arrays in field · 30bae7ef
  Julien Signoles authored 11 years ago
  
  [E-ACSL] prevent RTE while executing memory-related constructs
  30bae7ef
- [E-ACSL] fixed warning messages · 511ab9e7
  Julien Signoles authored 11 years ago
  
  511ab9e7
- [E-ACSL] do not monitor anymore memory locations involved in constructs not... · 3e0535e4
  Julien Signoles authored 11 years ago
  
  [E-ACSL] do not monitor anymore memory locations involved in constructs not yet supported like \freeable
  3e0535e4
Apr 18, 2013
- [E-ACSL] more precise pre-analysis · d71fc0af
  Julien Signoles authored 11 years ago
  
  d71fc0af
Apr 16, 2013

[E-ACSL] fixed bug #1390 about typing of logic variables of type long long · 1e75b7af

Julien Signoles authored 11 years ago

[E-ACSL] compute a more precise type for quantified variable with a strict upper bound
[E-ACSL] do not modify the type of a quantified variable anymore

1e75b7af

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
Apr 10, 2013
- [e-acsl] +number of dyn allocated bytes · 623a44af
  Guillaume Petiot authored 11 years ago
  
  623a44af
Apr 02, 2013
- [e-acsl] article déplacé · 30588d10
  Guillaume Petiot authored 11 years ago
  
  30588d10
Mar 28, 2013
- [e-acsl] resync for new definition of Cil_types.logic_real · 7c296de9
  Guillaume Petiot authored 12 years ago
  
  7c296de9
Mar 14, 2013
- [e-acsl] issue #1379 : __out_of_bound implemented · 296931a7
  Guillaume Petiot authored 12 years ago
  
  296931a7
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] fixed bug with property which are false if reachable · f7388753
  Julien Signoles authored 12 years ago
  
  f7388753
- [E-ACSL] update according to kernel changes · fd5de66a
  Julien Signoles authored 12 years ago
  
  fd5de66a
Mar 07, 2013
- + get_sub · 01c55716
  Guillaume Petiot authored 12 years ago
  
  01c55716