Commits · d37b98370caa8b6622937d9816cc0912567fc124 · pub / frama-c · GitLab

Snippets Groups Projects

Apr 10, 2020
- [wp] extended smoke tests · d37b9837
  Loïc Correnson authored 4 years ago
  
  d37b9837
- [lib] improved dotgraph API · 8185a987
  Loïc Correnson authored 4 years ago
  
  8185a987
- [wp] removed -wp-check option · 6099010a
  Loïc Correnson authored 4 years ago
  
  6099010a
Mar 31, 2020
- [kernel] refactor expr-to-term · cef75793
  Loïc Correnson authored 4 years ago
  
  cef75793
Mar 30, 2020
- [wp] support for float builtins · b1355b8b
  Loïc Correnson authored 4 years ago
  
  b1355b8b
- [wp] fix sub-float operation · a3616e89
  Loïc Correnson authored 4 years ago
  
  a3616e89
Mar 27, 2020
- [wp] changelog for invalid pointers · b8874fb7
  Loïc Correnson authored 4 years ago and David Bühler committed 4 years ago
  
  b8874fb7
- [wp] test for invalid pointers · a83af155
  Loïc Correnson authored 4 years ago and David Bühler committed 4 years ago
  
  a83af155
- [wp] implement OBJ validity access mode · de4c7793
  Loïc Correnson authored 4 years ago and David Bühler committed 4 years ago
  
  de4c7793
- [typing] properly register __builtin_offsetof as a builtin · 3bf9500a
  David Bühler authored 5 years ago
  
  Avoid warning about missing proto during typechecking. Also changes a warning into an error, and improves the error message.
  3bf9500a
- [Logic] New predicate object_pointer. Not yet supported by the plugins. · 5b4c1196
  David Bühler authored 5 years ago
  
  5b4c1196
Mar 26, 2020
- [wp] cache updates · 8c048b58
  Loïc Correnson authored 4 years ago
  
  8c048b58
- [wp] New test to check float drivers bindings · b24dc837
  Allan Blanchard authored 4 years ago
  
  b24dc837
- [wp] Updates float drivers to match Cfloat MLW · 5f00774b
  Allan Blanchard authored 4 years ago
  
  5f00774b
- [wp] Adds missing 'round' functions to Cfloat MLW · a5ed19d0
  Allan Blanchard authored 4 years ago
  
  a5ed19d0
Mar 24, 2020
- [wp] builtin types are now registered in LogicBuiltins · 426c502a
  Allan Blanchard authored 5 years ago
  
  426c502a
Mar 23, 2020
- [wp] fix duplicated block in · 36104e93
  Loïc Correnson authored 5 years ago
  
  36104e93
- [wp] fix scope of function body · 8b39f0cd
  Loïc Correnson authored 5 years ago
  
  8b39f0cd
- [wp] optimise block in/out · 3f344200
  Loïc Correnson authored 5 years ago
  
  3f344200
- [wp] fix open/close blocks · 16c65085
  Loïc Correnson authored 5 years ago
  
  16c65085
- [wp] test exhibiting the scope problem · 81fbce4e
  Loïc Correnson authored 5 years ago
  
  81fbce4e
Mar 18, 2020
- [wp] Supports sqrt/f · 8dc7935d
  Allan Blanchard authored 5 years ago
  
  8dc7935d
- [wp] Slightly improves float constant handling · 061a773f
  Allan Blanchard authored 5 years ago
  
  061a773f
- [wp] Do not fail on unimplemented ACSL builtins · 8af979fa
  Allan Blanchard authored 5 years ago
  
  8af979fa
- [wp] Removes unused elements in Cfloat.mlw · 0a6c8b8e
  Allan Blanchard authored 5 years ago
  
  0a6c8b8e
- [wp] Improves float literal translation · c3dbc9a7
  Allan Blanchard authored 5 years ago
  
  c3dbc9a7
- [wp] Make Why3 float literal whenever possible · 5f357ad4
  Allan Blanchard authored 5 years ago
  
  5f357ad4
- [wp] Bind Cfloat simple symbols on Why3 IEEE float · c1c1b877
  Allan Blanchard authored 5 years ago
  
  c1c1b877
Mar 17, 2020
- [wp] fix latex manual · 23b50db8
  Loïc Correnson authored 5 years ago
  
  23b50db8
- [WP] some more tests · 729d5da5
  Patrick Baudin authored 5 years ago
  
  729d5da5
Mar 16, 2020
- [wp] fix quantified int simplifier · 9dd99c6d
  Loïc Correnson authored 5 years ago
  
  keep bottom domain in the right place
  9dd99c6d
- [wp] added test for integer quantifiers · 41a62d00
  Loïc Correnson authored 5 years ago
  
  41a62d00
Mar 13, 2020
- [config] change name of config.ml to avoid clash with compiler internal lib · aedae7e6
  Virgile Prevosto authored 5 years ago
  
  aedae7e6
Mar 06, 2020
- remove unnecessary header from test file · cad60c24
  Andre Maroneze authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  cad60c24
- update copyright to 2020 · 325661e6
  Andre Maroneze authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  325661e6
- update .gitignore to match tracked files · 174fdd41
  Andre Maroneze authored 5 years ago
  
  174fdd41
- [wp] update cache · ac3a1f07
  Loïc Correnson authored 5 years ago
  
  No cleanup (yet)
  ac3a1f07
- [wp] fix makefile wp-qualif-oracle & wp-qualif-cleanup · d11bde3c
  Loïc Correnson authored 5 years ago
  
  d11bde3c
Mar 02, 2020
- [wp] oracle changes (no prover version) · 4f21fff3
  Loïc Correnson authored 5 years ago
  
  4f21fff3
- [wp] hide prover versions in qualif tests · eee9a6a9
  Loïc Correnson authored 5 years ago
  
  eee9a6a9