Commits · 8879feea506b034d485dbe13b01da0332870440c · pub / frama-c

Mar 06, 2015
- renaming pre_analysis.ml* into mmodel_analysis.ml* · 8879feea
  Julien Signoles authored 10 years ago
  
  8879feea
Jan 29, 2015
- header 2015 · 69cbc062
  Julien Signoles authored 10 years ago
  
  69cbc062
Dec 16, 2014
- fix compilation according to kernel changes · ab49e183
  Julien Signoles authored 10 years ago
  
  ab49e183
Aug 27, 2014
- update according to kernel changes (\specified) · 51790ff1
  Julien Signoles authored 10 years ago
  
  51790ff1
Mar 25, 2014
- fix bug #1716 about annotations in while(1) · 0591af49
  Julien Signoles authored 11 years ago
  
  0591af49
- replace tab by whitespaces · 43578ed5
  Julien Signoles authored 11 years ago
  
  43578ed5
- fix bug #1716 about annotations in while(1) · 783172b7
  Julien Signoles authored 11 years ago
  
  783172b7
Mar 24, 2014
- why tabulations? · fc34351a
  Julien Signoles authored 11 years ago
  
  fc34351a
- fixing the header ('licenses' is not 'license') · 378f93e2
  Julien Signoles authored 11 years ago
  
  378f93e2
Mar 14, 2014
- fixing the header ('licenses' is not 'license') · 5117fe98
  Julien Signoles authored 11 years ago
  
  5117fe98
Mar 07, 2014
- applying headers 2014 · 524689f4
  Julien Signoles authored 11 years ago
  
  524689f4
Jan 28, 2014
- [E-ACSL] fix bug #1634 occuring in presence of static addresses · 80230733
  Julien Signoles authored 11 years ago
  
  [E-ACSL] fix some headers and update TODO-list
  80230733
Oct 25, 2013
- [E-ACSL] compatibility with warning 7 · d87c0496
  Julien Signoles authored 11 years ago
  
  d87c0496
Oct 03, 2013
- [E-acsl] Use isPointerType instead of isPtrType · d850d021
  Boris Yakobowski authored 11 years ago
  
  d850d021
Sep 26, 2013
- [E-ACSL] fix incorrectness which may occur in presence of aliasing · d4856c40
  Julien Signoles authored 11 years ago
  
  d4856c40
Sep 25, 2013
- [E-ACSL] refactoring code about RTE · 9aff9588
  Julien Signoles authored 11 years ago
  
  9aff9588
- [E-ACSL] again compatible with the trunk and no more with Fluorine · aa5f7cf6
  Julien Signoles authored 11 years ago
  
  aa5f7cf6
Sep 23, 2013
- [E-ACSL] ready for v0_3 · 565aff54
  Julien Signoles authored 11 years ago
  
  565aff54
Sep 04, 2013
- [E-ACSL] fix previous commit in case of multiple initializers (requires an... · 48d16df9
  Julien Signoles authored 11 years ago
  
  [E-ACSL] fix previous commit in case of multiple initializers (requires an up-to-date Frama-C kernel)
  48d16df9
- [E-ACSL] fixed bug #1478 when monitored global variables have initializers · fbc77baf
  Julien Signoles authored 11 years ago
  
  fbc77baf
Jul 18, 2013
- fixes running tests in internal mode + DO NOT generate varinfo if the plug-in is not running · fc90887c
  Virgile Prevosto authored 11 years ago
  
  fc90887c
May 27, 2013
- [E-ACSL] fixed bug with series of addresses · fe218b78
  Julien Signoles authored 11 years ago
  
  fe218b78
May 22, 2013
- [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 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] 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
Apr 30, 2013

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] dataflow optimisation: ignore duplicated function contract · 9f0b656a
  Julien Signoles authored 11 years ago
  
  9f0b656a
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 19, 2013
- [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 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