Commits · c71cb50586a7afeb7eb6ac7cb39aa22e5ed077ec · pub / frama-c · GitLab

Snippets Groups Projects

Sep 18, 2020
- [wp] only output information on loaded driver when 'driver' category is on · c71cb505
  Virgile Prevosto authored 4 years ago
  
  c71cb505
Sep 17, 2020
- ChangeLog · 978d2f2c
  Allan Blanchard authored 4 years ago
  
  978d2f2c
- [wp] Lint register · b1d770b2
  Allan Blanchard authored 4 years ago
  
  b1d770b2
- [wp] Memoisation for hypotheses · d607cbe7
  Allan Blanchard authored 4 years ago
  
  d607cbe7
Sep 16, 2020
- [eacsl:runtime] Fix include of segment_tracking.h · 931c4425
  Basile Desloges authored 4 years ago
  
  931c4425
- [eacsl:runtime] Fix installation of runtime library files · 3d402d58
  Basile Desloges authored 4 years ago
  
  3d402d58
Sep 15, 2020
- [eacsl] Update changelog · c38ab1d5
  Basile Desloges authored 4 years ago
  
  c38ab1d5
- [eacsl:runtime] Fix lint · e4e6e7ac
  Basile Desloges authored 4 years ago
  
  e4e6e7ac
- [eacsl:runtime] Fix stack size handling · f2643727
  Basile Desloges authored 4 years ago
  
  f2643727
- [eacsl:runtime] Remove unused extern definition · 77fa4678
  Basile Desloges authored 4 years ago
  
  77fa4678
- [eacsl] Update tests · d3a6265c
  Basile Desloges authored 4 years ago
  
  d3a6265c
- [eacsl] Update E-ACSL to use the new organisation of RTL files · a3a64c43
  Basile Desloges authored 4 years ago
  
  a3a64c43
- [eacsl:runtime] Update rtl to separate header and source files · 05be80b9
  Basile Desloges authored 4 years ago
  
  05be80b9
- [eacsl:runtime] Move files to thematic folders · 62f96fde
  Basile Desloges authored 4 years ago
  
  62f96fde
- [eacsl] Update changelog · 3747bf6c
  Basile Desloges authored 4 years ago
  
  3747bf6c
Sep 14, 2020
- [eacsl] Update tests · be960328
  Basile Desloges authored 4 years ago
  
  be960328
- [eacsl] Rename `full-mmodel` option to `full-mtracking` · e385bffe
  Basile Desloges authored 4 years ago
  
  - Deprecate old `full-mmodel` option in E-ACSL plugin and in `e-acsl-gcc.sh` - Create new `full-mtracking` option - Update documentation to use the new option
  e385bffe
- [eacsl] Propagate renaming changes · 815fd4cf
  Basile Desloges authored 4 years ago
  
  815fd4cf
- [eacsl] Rename `mmodel_translate` to `memory_translate` · 597a77f5
  Basile Desloges authored 4 years ago
  
  597a77f5
- [eacsl] Rename `mmodel_analysis` to `memory_tracking` · d41e9698
  Basile Desloges authored 4 years ago
  
  The functions `must_model` have also been renamed to `must_monitor`.
  d41e9698
Sep 11, 2020
- Update ChangeLog · 6db33b9e
  Allan Blanchard authored 4 years ago
  
  6db33b9e
- [wp] ignore check loop when searching for dead annot · 1699baad
  Allan Blanchard authored 4 years ago
  
  1699baad
Sep 10, 2020
- [wp] update to new WP API after rebase · 0052e04e
  Virgile Prevosto authored 4 years ago
  
  0052e04e
- [wp] fix check lemma category · 628bfb5d
  Loïc Correnson authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  628bfb5d
- [wp] fix help for -wp-prop · 1ce69a31
  Loïc Correnson authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  1ce69a31
- [wp-qualif] update oracles · 38bef5b1
  Virgile Prevosto authored 4 years ago
  
  38bef5b1
- [kernel] refine names of properties related to check annotations · b73effbd
  Virgile Prevosto authored 4 years ago
  
  b73effbd
- [wp] added @check category to -wp-prop · 965fb25a
  Loïc Correnson authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  965fb25a
- [wp] unit test for checks · fd1eb2c7
  Loïc Correnson authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  fd1eb2c7
- [wp] don't put check lemma in proof context · cbed8092
  Loïc Correnson authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  cbed8092
- [wp] introduce lemma kind · cf255eef
  Loïc Correnson authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  cf255eef
- [eva] factor identical cases in pattern-matching · e1d75182
  Virgile Prevosto authored 4 years ago
  
  e1d75182
- [eva] rename argument · 66f225d7
  Virgile Prevosto authored 4 years ago
  
  as proposed in [MR](https://git.frama-c.com/frama-c/frama-c/-/merge_requests/2817#note_95099)
  66f225d7
- [wp] don't put check-only loop invariants in hypotheses · bb58530a
  Virgile Prevosto authored 4 years ago
  
  bb58530a
- [eva] don't reduce check-only loop invariants · 147c0a38
  Virgile Prevosto authored 4 years ago
  
  147c0a38
- [eva] don't reduce on a check ensures/requires · 0bcdf987
  Virgile Prevosto authored 4 years ago
  
  0bcdf987
- [wp] do not put check requires in environment of other PO for caller · 0366fc38
  Virgile Prevosto authored 4 years ago
  
  0366fc38
- [wp] do not put 'check lemma' in environment. · f4e86d8b
  Virgile Prevosto authored 4 years ago
  
  f4e86d8b
- [wp] check requires are not put as hypothesis · 5dbe9132
  Virgile Prevosto authored 4 years ago
  
  5dbe9132
- [wp] start supporting generalized check · 5901dc9f
  Virgile Prevosto authored 4 years ago
  
  5901dc9f