Commits · c46af792ede76238b78f938ec1d79983629a3e19 · pub / frama-c · GitLab

Snippets Groups Projects

Nov 25, 2019
- [Eva] Adds a test of the summary of logical properties evaluation. · 889fea20
  David Bühler authored 5 years ago
  
  889fea20
- [Eva] In the summary, do not count unreachable logical properties as proven. · fb62c8fa
  David Bühler authored 5 years ago
  
  fb62c8fa
- [Eva] Adds a test of the summary when using both RTE and Eva. · 10560989
  David Bühler authored 5 years ago
  
  10560989
Nov 15, 2019
- [logic] make mk_cast aware of logic coercions · d9c0c704
  Virgile Prevosto authored 5 years ago
  
  d9c0c704
- test for conversion issue · ddee95a4
  Virgile Prevosto authored 5 years ago
  
  ddee95a4
- [logic] more precise error message when typing extension raises an exn · 9a473c43
  Virgile Prevosto authored 5 years ago
  
  9a473c43
Nov 14, 2019
- [analysis-scripts] fix template when stub for 'main' is generated · 41a59204
  Andre Maroneze authored 5 years ago
  
  41a59204
Nov 12, 2019
- [Kernel] better handling of non-existing filepaths · 0047eb3c
  Andre Maroneze authored 5 years ago
  
  0047eb3c
Nov 08, 2019
- [tests] simplify test · e7cdfd97
  Virgile Prevosto authored 5 years ago
  
  - no 3d party module dependency - don't have a stack dump as oracle
  e7cdfd97
- [test] test case for reported issue · 714a13d3
  Virgile Prevosto authored 5 years ago
  
  714a13d3
Oct 31, 2019
- [ghost] Checks consistency of ghost decl/def · 08d3e926
  Allan Blanchard authored 5 years ago
  
  08d3e926
- [Kernel] Ensures that infer_annotations assigns \result for ghost functions · c1e2d8da
  Allan Blanchard authored 5 years ago
  
  c1e2d8da
- [Test] Adds some tests related to insertion of formals in ghost functions · d35b9d4d
  Allan Blanchard authored 5 years ago
  
  d35b9d4d
- [test] Activate a test about pretty-printing of ghost functions · 314782be
  Allan Blanchard authored 5 years ago
  
  314782be
- [tests] update oracles · 164c758f
  Virgile Prevosto authored 5 years ago and Allan Blanchard committed 5 years ago
  
  164c758f
- [ghost] specialized error msg when ghost symbol appears in non-ghost context · 8b1aa759
  Virgile Prevosto authored 5 years ago and Allan Blanchard committed 5 years ago
  
  8b1aa759
- [ghost] prefer renaming a ghost local in case of name clash · de73787c
  Virgile Prevosto authored 5 years ago and Allan Blanchard committed 5 years ago
  
  de73787c
- [tests] preliminary work for fixing alpha-conversion of locals · 604c5820
  Virgile Prevosto authored 5 years ago and Allan Blanchard committed 5 years ago
  
  if a non-ghost local shadows a ghost one, the renaming should affect the ghost.
  604c5820
- [tests] checks that typing reject prog with two locals with same name and scope · 19475eec
  Virgile Prevosto authored 5 years ago and Allan Blanchard committed 5 years ago
  
  even if one is ghost and the other non-ghost
  19475eec
- [typing] fixes parsing and typing of ghost functions · 2cd04265
  Virgile Prevosto authored 5 years ago and Allan Blanchard committed 5 years ago
  
  2cd04265
- [cil] fixes scope of ghost variables under \at · 82398fda
  Virgile Prevosto authored 5 years ago and Allan Blanchard committed 5 years ago
  
  82398fda
- [tests] add access to ghost variable under at to show typing issue · b1dc329e
  Virgile Prevosto authored 5 years ago and Allan Blanchard committed 5 years ago
  
  b1dc329e
- [tests] fixes ill-formed test · 72e835e7
  Virgile Prevosto authored 5 years ago and Allan Blanchard committed 5 years ago
  
  72e835e7
- [typing] use dual ghost/non-ghost scope for variables lookup · f562009c
  Virgile Prevosto authored 5 years ago and Allan Blanchard committed 5 years ago
  
  f562009c
- add test case for 2421 · d23c315b
  Virgile Prevosto authored 5 years ago and Allan Blanchard committed 5 years ago
  
  d23c315b
Oct 29, 2019
- [Libc] more fixes after review · 6664c43f
  Andre Maroneze authored 5 years ago
  
  6664c43f
- [Libc] fix libc spec: utimes; add test · 4eab1f50
  Andre Maroneze authored 5 years ago
  
  4eab1f50
- [libc] minor fixes following review · 52059c39
  Andre Maroneze authored 5 years ago
  
  52059c39
- update test oracles · a7372004
  Andre Maroneze authored 5 years ago
  
  a7372004
- [Libc] fix/improve several specs in stdio.h · fd699101
  Andre Maroneze authored 5 years ago
  
  fd699101
- update test oracles · 2caafeae
  Andre Maroneze authored 5 years ago
  
  2caafeae
- [Libc] fix several specifications · 8dc15b11
  Andre Maroneze authored 5 years ago
  
  8dc15b11
- update test oracles · 4a315117
  Andre Maroneze authored 5 years ago
  
  4a315117
- [Libc] fix some specs in stdio.h · 659b93f6
  Andre Maroneze authored 5 years ago
  
  659b93f6
- [Libc] Fix specs in wchar.h · b337c046
  Andre Maroneze authored 5 years ago
  
  b337c046
Oct 22, 2019
- [Eva] New test file for the automatic loop unrolling heuristic. · f26cf0af
  David Bühler authored 5 years ago
  
  f26cf0af
Oct 21, 2019
- [Kernel] Interpreted_automata: comments the dataflow functor. · 8ef8e80a
  David Bühler authored 5 years ago
  
  8ef8e80a
- [Interpreted automata] Add a dataflow computation functor · 6bc0ed2d
  Valentin Perrelle authored 5 years ago and David Bühler committed 5 years ago
  
  6bc0ed2d
- [Eva] Disables the automatic loop unrolling by default. · 8409b706
  David Bühler authored 5 years ago
  
  8409b706
- [Eva] Updates test oracles. · d4f4058e
  David Bühler authored 5 years ago
  
  d4f4058e