Commits · 3bf9500a79b809c216bd871b839deda44829b6af · pub / frama-c · GitLab

Snippets Groups Projects

Mar 27, 2020
- [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 5 years ago
  
  8c048b58
- [wp] New test to check float drivers bindings · b24dc837
  Allan Blanchard authored 5 years ago
  
  b24dc837
- [wp] Updates float drivers to match Cfloat MLW · 5f00774b
  Allan Blanchard authored 5 years ago
  
  5f00774b
- [wp] Adds missing 'round' functions to Cfloat MLW · a5ed19d0
  Allan Blanchard authored 5 years ago
  
  a5ed19d0
Mar 24, 2020
- [wp] builtin types are now registered in LogicBuiltins · 426c502a
  Allan Blanchard authored 5 years ago
  
  426c502a
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
Feb 25, 2020
- [wp] sequent API documentation · f6eec487
  Loïc Correnson authored 5 years ago
  
  f6eec487
Feb 21, 2020
- [wp] prover name fallback · 4252473c
  Loïc Correnson authored 5 years ago
  
  4252473c
Feb 20, 2020
- Update WP Changelog after merging !2543 · bee62de0
  Virgile Prevosto authored 5 years ago
  
  bee62de0
- [wp] fix documentation · ce57c4d4
  Loïc Correnson authored 5 years ago
  
  ce57c4d4
- [wp] smoke tests · 1560d044
  Loïc Correnson authored 5 years ago
  
  1560d044
- [wp] extended lemmas on div, mod & shifts · 7ac1fc42
  Loïc Correnson authored 5 years ago
  
  7ac1fc42
- [wp] more robust script session · 57f17599
  Loïc Correnson authored 5 years ago
  
  Share scripts among models. More robust against script errors.
  57f17599
- [wp] emit a warning when no generated goal · c635c818
  Loïc Correnson authored 5 years ago
  
  c635c818
- [wp] control over max split at cfg level · 78e6d5e5
  Loïc Correnson authored 5 years ago
  
  78e6d5e5
- [wp] extends undold assigns to all assignments · 37b836cd
  Loïc Correnson authored 5 years ago
  
  37b836cd
- [wp] move frame conditions to Type section · 905c8b40
  Loïc Correnson authored 5 years ago
  
  Allows for more efficient filtering. Also enhanced frame conditions with typing for globals.
  905c8b40
Feb 19, 2020
- [wp] fix loop-current label in loop annotations · 2ac59dd4
  Loïc Correnson authored 5 years ago
  
  2ac59dd4
- [wp] added test for loop-current · 750e38f2
  Loïc Correnson authored 5 years ago
  
  750e38f2
Feb 17, 2020
- [WP] raise an error on unsupported parametric types · b3fe1ae4
  Allan Blanchard authored 5 years ago
  
  b3fe1ae4