Commits · 1db5dc3cb1c1c1cfa27a4889912fcaa1700d6be2 · pub / frama-c · GitLab

Snippets Groups Projects

May 31, 2021
- Update Changelog · 1db5dc3c
  Allan Blanchard authored 3 years ago
  
  1db5dc3c
- Merge branch 'feature/wp/extend-overflow-tactic' into 'master' · 854184c1
  Allan Blanchard authored 3 years ago
  
  Generalized Overflow tactic See merge request frama-c/frama-c!3210
  854184c1
- [wp/doc] Document new Overflow behavior · c145059a
  Allan Blanchard authored 3 years ago
  
  c145059a
- [wp] Generalize overflow tactic · 7be87e6c
  Allan Blanchard authored 3 years ago
  
  7be87e6c
May 26, 2021
- Merge branch 'stable/vanadium' into 'master' · 31796e8f
  François Bobot authored 3 years ago
  
  Stable/vanadium See merge request frama-c/frama-c!3208
  31796e8f
- Merge branch 'bugfix/basile/eacsl-valid-regression' into 'stable/vanadium' · 54e6af01
  Julien Signoles authored 3 years ago
  
  [eacsl] Fix regression on `-e-acsl-no-valid` in the presence of behaviors See merge request frama-c/frama-c!3207
  54e6af01
- Merge branch 'feature/wp/stable-vanadium-fix-memlimit' into 'stable/vanadium' · fdcb0d60
  François Bobot authored 3 years ago
  
  [WP] Fix for memlimit See merge request frama-c/frama-c!3206
  fdcb0d60
May 25, 2021
- [eacsl] Update changelog · 527588a4
  Basile Desloges authored 3 years ago
  
  527588a4
- [eacsl] Update e-acsl-valid test · 8c53fc4c
  Basile Desloges authored 3 years ago
  
  8c53fc4c
- [eacsl] Remove optional dependency to Eva · 8a55809d
  Basile Desloges authored 3 years ago
  
  8a55809d
- [eacsl] Remove Eva builtin registering for contract init function · 768669c7
  Basile Desloges authored 3 years ago
  
  768669c7
- [eacsl] Admit post-condition of contract init function · dc684f95
  Basile Desloges authored 3 years ago
  
  dc684f95
- Merge branch 'feature/andre/libc-utmp-for-who' into 'master' · 550fa231
  Andre Maroneze authored 3 years ago
  
  Feature/andre/libc utmp for who See merge request frama-c/frama-c!3188
  550fa231
- Merge branch 'feature/julien/array_forall' into 'master' · b9bd8317
  Allan Blanchard authored 3 years ago
  
  use Array.for_all in structural_descr.ml See merge request frama-c/frama-c!3183
  b9bd8317
- Merge branch 'feature/changelog-manual' into 'stable/vanadium' · 21b49440
  Allan Blanchard authored 3 years ago
  
  [manuals] update version name of Changelog section See merge request frama-c/frama-c!3197
  21b49440
- remove custom version of Array.for_all · 2df4e4ea
  Julien Signoles authored 3 years ago and Allan Blanchard committed 3 years ago
  
  2df4e4ea
May 21, 2021
- Merge remote-tracking branch 'origin/stable/vanadium' into stable/vanadium · 91372690
  François Bobot authored 3 years ago
  
  91372690
- [WP] Side step mis-documentation in Why3 by always setting a memlimit · 65312ded
  François Bobot authored 3 years ago
  
  65312ded
- [Eva] Updates test oracle for the apron config. · 52cf2ad1
  David Bühler authored 3 years ago
  
  The apron config disables the warning about experimental domains.
  52cf2ad1
- [git] add linting commit to be ignored · 3707b0da
  Andre Maroneze authored 3 years ago
  
  3707b0da
- Merge branch 'feature/andre/mass-linting' into 'master' · 27369ac0
  Andre Maroneze authored 3 years ago
  
  Mass-lint all remaining OCaml files See merge request frama-c/frama-c!3192
  27369ac0
- Mass-lint all remaining OCaml files · 89b69ec2
  Andre Maroneze authored 3 years ago
  
  89b69ec2
May 20, 2021
- Merge branch 'feature/eva/taint-analysis' into 'master' · 91438b7f
  David Bühler authored 3 years ago
  
  New Eva domain for taint analysis See merge request frama-c/frama-c!3130
  91438b7f
- [Eva] Very short description of the taint domain. · 895ab631
  David Bühler authored 3 years ago
  
  895ab631
- [Eva] Make annotation zone contribute to data-tainted locations in state. · f4467870
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  f4467870
- [Eva] Simplify bases computation. · 78fc7db6
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  78fc7db6
- [Eva] Untaint left value only when the corresponding location is a singleton. · ab8f901f
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  ab8f901f
- [Eva] Do not add lv_zone once again if tainted because of annotation. · 44bb6ab0
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  44bb6ab0
- [Eva] Remove test result predications as not maintanable. · 3bb6dcb0
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  3bb6dcb0
- [Eva] Rework test file. · a0b7d17f
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  a0b7d17f
- [Eva] Update to changes for recursion support. · ac91930f
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  ac91930f
- [Eva] Add taint domain files into header_spec.txt list. · 01f1bdc8
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  01f1bdc8
- [Eva] Simplify filter assume function by using postdominators. · 09850650
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  09850650
- [Eva] Add test with goto. · 2efb5ab9
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  2efb5ab9
- [Eva] Taint domain: tries to fix the computation of control-dependencies. · c85fa0a7
  David Bühler authored 3 years ago
  
  c85fa0a7
- [Eva] Add test on control-dependency with combined assumes. · 57b15ee4
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  57b15ee4
- [Eva] Avoid breaking format boxing. · ad28e7dd
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  ad28e7dd
- [Eva] Rework assign support so that control and data dependency taint analysis... · 55235580
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  [Eva] Rework assign support so that control and data dependency taint analysis are performed as not alternatives to each other.
  55235580
- [Eva] Do not consider the indirect zones of the lval in assignments. · f8dfc621
  Michele Alberti authored 3 years ago and David Bühler committed 3 years ago
  
  f8dfc621
- [Eva] Add support for ACSL assigns clause via logic_assign. · a8165276
  Michele Alberti authored 4 years ago and David Bühler committed 3 years ago
  
  a8165276