Commits · e1d5e166f1ba48f78ba0941eb3f59dcaea932500 · pub / frama-c · GitLab

Snippets Groups Projects

Feb 09, 2021
- [wp/doc] -wp-dump and -wp-legacy · e1d5e166
  Allan Blanchard authored 4 years ago
  
  e1d5e166
- [wp] Post/Exit state unreachable · 6b6d9b36
  Allan Blanchard authored 4 years ago
  
  6b6d9b36
- [wp] fix RTE generation · a8f203f2
  Loïc Correnson authored 4 years ago
  
  a8f203f2
- [wp] fix smoke dead calls · 7df8d089
  Loïc Correnson authored 4 years ago
  
  7df8d089
- [wp] smoke unreachable stmt · 69262e6a
  Loïc Correnson authored 4 years ago
  
  69262e6a
Feb 08, 2021
- [wp] (some) smoke fixes · 64c8febb
  Loïc Correnson authored 4 years ago
  
  64c8febb
- [wp] dead-call smoke tests · 7b6417f4
  Loïc Correnson authored 4 years ago
  
  7b6417f4
- [wp] smoke deadcode · 226fb436
  Loïc Correnson authored 4 years ago
  
  226fb436
- [wp] smoke requires · ea4b851d
  Loïc Correnson authored 4 years ago
  
  ea4b851d
- [wp] refactor function-body · 3ee159f6
  Loïc Correnson authored 4 years ago
  
  3ee159f6
- [wp] Clear CFG tables after WP · 8be82aee
  Allan Blanchard authored 4 years ago
  
  8be82aee
- [wp] Use OcamlGraph for reachability · 09eca65f
  Allan Blanchard authored 4 years ago
  
  09eca65f
- [wp] Fixes filter props · bb1bc134
  Allan Blanchard authored 4 years ago
  
  bb1bc134
- [wp] Reachability: less memoization · a90614e2
  Allan Blanchard authored 4 years ago
  
  a90614e2
- [wp] Do not ignore main declaration · 699c1f84
  Allan Blanchard authored 4 years ago
  
  699c1f84
- [wp] Generate RTE before getting cfg infos · cb6150a1
  Allan Blanchard authored 4 years ago
  
  cb6150a1
- [wp] CfgInfos collects loop annots · 00ea6982
  Allan Blanchard authored 4 years ago
  
  00ea6982
Feb 05, 2021
- [wp] fix spurius specs · e91f90a2
  Loïc Correnson authored 4 years ago
  
  e91f90a2
- [wp] fix cfg-infos annots · 448ae659
  Loïc Correnson authored 4 years ago
  
  448ae659
- [wp] use cfg-infos · af0df02b
  Loïc Correnson authored 4 years ago
  
  af0df02b
- [wp] refactor wp-function-body structure · 50be0578
  Loïc Correnson authored 4 years ago
  
  50be0578
- Merge branch 'master' into 'feature/wp/new-cfg-control' · cf5de66d
  Loïc Correnson authored 4 years ago and Loïc Correnson committed 4 years ago
  
  # Conflicts: # src/plugins/wp/wpStrategy.ml
  cf5de66d
Feb 04, 2021
- Merge branch 'feature/kernel/admit' into 'master' · 70644a1d
  Loïc Correnson authored 4 years ago
  
  new predicate kind Admit See merge request frama-c/frama-c!2911
  70644a1d
- Merge branch 'master' into feature/wp/new-cfg-control · 43ad47a5
  Loïc Correnson authored 4 years ago
  
  # Conflicts: # src/kernel_services/analysis/interpreted_automata.ml # src/plugins/wp/wpAnnot.mli
  43ad47a5
Feb 03, 2021
- [wp] memoize call & loop contacts · e6fb4cb3
  Loïc Correnson authored 4 years ago
  
  e6fb4cb3
- [wp] memoized cfg-annotations · 0328b4e8
  Loïc Correnson authored 4 years ago
  
  0328b4e8
- [wp] memoized cfg-infos · 69f5d8cc
  Loïc Correnson authored 4 years ago
  
  69f5d8cc
- [wp] collect cfg infos · 2e6c67ee
  Loïc Correnson authored 4 years ago
  
  2e6c67ee
- [kernel] Minor renaming in property_status. · 19ffbb92
  David Bühler authored 4 years ago
  
  19ffbb92
- [kernel] Property status: changes [automatically_proven] into [automatically_computed]. · 4f2fe874
  David Bühler authored 4 years ago
  
  4f2fe874
- [kernel] Property status: new type and function to classify properties. · 3e57d055
  David Bühler authored 4 years ago
  
  3e57d055
- [wp] fix use/verify predicate kinds · 28b2cccc
  Loïc Correnson authored 4 years ago and David Bühler committed 4 years ago
  
  28b2cccc
- [Eva] Do not record the logical status of "admit" predicates. · 51960af6
  David Bühler authored 4 years ago
  
  51960af6
- [kernel] Admitted properties always have the Considered_valid status. · 1a7d7665
  David Bühler authored 4 years ago
  
  Plugins cannot emit a status for admitted properties.
  1a7d7665
- [kernel] New predicate kind: Assert, Check or Admit. · 49f1590f
  David Bühler authored 4 years ago
  
  49f1590f
- Merge branch 'feature/wp/smoke-unreachable' into 'master' · 760be04b
  Allan Blanchard authored 4 years ago
  
  [wp] fix corner cases for unreachability See merge request frama-c/frama-c!3051
  760be04b
Feb 02, 2021
- [wp] Move some functions in CfgCalculus · bbe369d8
  Allan Blanchard authored 4 years ago
  
  bbe369d8
- [wp] Partial refactoring of main compute procedure · 159e2efc
  Allan Blanchard authored 4 years ago
  
  159e2efc
- [wp] compute smoking tests for unreachables · e4524eae
  Loïc Correnson authored 4 years ago
  
  e4524eae
- [wp] take into accounts unreachable in final count · 6a90eb30
  Loïc Correnson authored 4 years ago
  
  6a90eb30