Commits · 54e374b194630bddeb150dcd2e23b8fc961e3b57 · pub / frama-c · GitLab

Snippets Groups Projects

Apr 22, 2022
- [Eva] multidim: use Lattice_bounds · 54e374b1
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  54e374b1
- [Eva] multidim: reorganize files · 4c3dbd90
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  - split Abstract_memory into multiple file - move from kernel_services to value/domains/multidim
  4c3dbd90
- [Eva] multidim: small fixes · b45036b2
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  b45036b2
- [Eva] multidim: more precise oracles for indexes increment · 506306c7
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  506306c7
- [Eva] multidim: improve precision when an expression is not in the valuation · 56ff49f9
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  56ff49f9
- [Eva] multidim: replace most exceptions by `Top handling · 47820e55
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  47820e55
- [Eva] multidim: use Int_val instead of Ival for array indexes · 4402875a
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  4402875a
- [Eva] multidim: simplified interface for offset with no more exceptions · 538d329a
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  538d329a
- [Eva] multidim: a bit of cleaning · 7e48fc1c
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  7e48fc1c
- [Eva] multidim: fix unhandled exception in offset addition · 1f174257
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  1f174257
- [Eva] multidim: fix convergence issue and possible asserts · 9315a045
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  9315a045
- [Eva] slight improvements · c9947f0e
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  c9947f0e
- [Eva] multidim: fix correction of variables tracking and missing oracle crashes · cef56ae8
  Valentin Perrelle authored 2 years ago and David Bühler committed 2 years ago
  
  cef56ae8
- [Eva] multidim: use better oracles whenever possible · fc41ac53
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  fc41ac53
- [Eva] Multidim: registers a hook to access other domain states in the join. · 18cd9ce3
  David Bühler authored 3 years ago
  
  18cd9ce3
- [Eva] multidim: update test · c95a9e83
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  c95a9e83
- [Eva] multidim: remove obviously empty slices after bound replacement · 7518364c
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  - many cases where equality/inclusions are verified
  7518364c
- [Eva] multidim: more coherent bound aging in segmentation · 20bf3701
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  20bf3701
- [Eva] Multidim: fixes a performance issue. · 537232bc
  David Bühler authored 3 years ago
  
  Do not consider the age of bounds in comparison and hash functions.
  537232bc
- [Eva] multidim: add a test for eva_domain_scope · b93ad013
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  b93ad013
- [Eva] multidim: display a proper error message when the scoped variables cannot be found · 5a5b2260
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  5a5b2260
- [Eva] multidim: add an annotation to control which bases are tracked · 7883e630
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  7883e630
- [Eva] remove the now useless rectype flag · b6af1359
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  b6af1359
- [IVal] float to int32 · e18ad67b
  François Bobot authored 3 years ago and David Bühler committed 2 years ago
  
  topify can create top for floats
  e18ad67b
- [Eva] multidim: handle floating point constants · 4e37d7bb
  François Bobot authored 3 years ago and David Bühler committed 2 years ago
  
  4e37d7bb
- [Eva] multidim: Prove initialization alarms · 9c61e985
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  9c61e985
- [Eva] multidim: ensure join correction and allow partition hints on raw memory · 47b24b36
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  47b24b36
- [Eva] multidim: accept array iterations through *(p + i) · ae0cbc8a
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  ae0cbc8a
- [Eva] multidim: infer disjunctive structure invariants · b8d363d5
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  b8d363d5
- [Eva] multidim: the limit on the number of segments is now a parameter · efc29e71
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  efc29e71
- [Eva] multidim: limit the size of the segmentation to 10 · 6f7e4a33
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  6f7e4a33
- [Eva] multidim: add annotation to hint the apropriate segmentation · 1ce73b95
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  1ce73b95
- [Eva] multidim: improved temporary oracle precision · b49231db
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  b49231db
- [Eva] multidim: fix writing overlaping the last bound · 7ad2c7af
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  7ad2c7af
- [Eva] multidim: merges tests into one · 2600bd3b
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  2600bd3b
- [Eva] multidim: fix a non termination bug · 8837765c
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  - Unification doesn't keep empty slices anymore so they can't accumulate - Fix the conversion of bounds to constants
  8837765c
- [Eva] multidim: prevent offsets to volatile fields to be taken · d9c0c9a8
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  d9c0c9a8
- [Eva] multidim: do not update segmentations that do not contain assigned variables · 876dcf7c
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  876dcf7c
- [Eva] multidim: fix more bugs · a8fd134d
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  a8fd134d
- [Eva] multidim: more readable bound pretty printing · 3fe455ce
  Valentin Perrelle authored 3 years ago and David Bühler committed 2 years ago
  
  3fe455ce