Commits · 978d2f2cd25d45deb5ff75411a363422fbbf0055 · pub / frama-c · GitLab

Snippets Groups Projects

Sep 17, 2020
- ChangeLog · 978d2f2c
  Allan Blanchard authored 4 years ago
  
  978d2f2c
- Merge branch 'master' into feature/blanchard/wp/hypotheses · 071e59d0
  Allan Blanchard authored 4 years ago
  
  071e59d0
- [wp] Lint register · b1d770b2
  Allan Blanchard authored 4 years ago
  
  b1d770b2
- Update nix/frama-ci.* · 63289038
  Virgile Prevosto authored 4 years ago and Allan Blanchard committed 4 years ago
  
  (cherry picked from commit 4df7a8d6) (cherry picked from commit 8bd2c0f8e3852fc4a4c02036d7f496746de2f9bf)
  63289038
- [wp] Memoisation for hypotheses · d607cbe7
  Allan Blanchard authored 4 years ago
  
  d607cbe7
Sep 11, 2020
- Merge branch 'feature/ACSL/generalized-check' into 'master' · 58f3a9dd
  Allan Blanchard authored 4 years ago
  
  Generalized check-only annotations See merge request frama-c/frama-c!2824
  58f3a9dd
- 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
- Merge branch 'master' into feature/ACSL/generalized-check · da629511
  Allan Blanchard authored 4 years ago
  
  da629511
- [GUI] Correctly prints check requires in precond at call site · 9b64abde
  Allan Blanchard authored 4 years ago
  
  9b64abde
Sep 10, 2020
- Merge branch 'fix/andre/dockerfiles' into 'master' · 9c3455df
  Andre Maroneze authored 4 years ago
  
  [Dev] improve Docker files with best practices See merge request frama-c/frama-c!2753
  9c3455df
- Update nix/frama-ci.* · 4df7a8d6
  Virgile Prevosto authored 4 years ago
  
  4df7a8d6
- [wp] update to new WP API after rebase · 0052e04e
  Virgile Prevosto authored 4 years ago
  
  0052e04e
- [tests] update to new WP msg keys · a85ed511
  Virgile Prevosto authored 4 years ago
  
  a85ed511
- [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
- [spec] separate wp objectives from kernel ones in check test · da2e73df
  Loïc Correnson authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  da2e73df
- [spec] remove wp debug infos from check test · 15fe85ab
  Loïc Correnson authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  15fe85ab
- [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
- [kernel] support for parsing/printing check of generalized invariant · 0d2b237b
  Virgile Prevosto authored 4 years ago
  
  0d2b237b
- [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
- [tests] update test case for generalized check · b6323d44
  Virgile Prevosto authored 4 years ago
  
  b6323d44
- [wp] start supporting generalized check · 5901dc9f
  Virgile Prevosto authored 4 years ago
  
  5901dc9f
- [tests] Update WP tests README · a4b46333
  Virgile Prevosto authored 4 years ago
  
  a4b46333
- [tests] fix wp-qualif ml script · 414814ae
  Virgile Prevosto authored 4 years ago
  
  414814ae
- [tests] update Aorai oracles · 674a3ef2
  Virgile Prevosto authored 4 years ago
  
  674a3ef2
- [tests] add test for generalized check · 8a03176a
  Virgile Prevosto authored 4 years ago
  
  8a03176a
- [printer] printer for generalized check · b70a8d35
  Virgile Prevosto authored 4 years ago
  
  b70a8d35