Commits · af732f7275b1c77c0716fcb124cb632fa6565803 · Charles Southerland / frama-c · GitLab

Snippets Groups Projects

Nov 16, 2020
- [e-acsl] more explicit changelog message · af732f72
  Julien Signoles authored 4 years ago
  
  af732f72
- [eacsl] Update changelog · 17b2a353
  Basile Desloges authored 4 years ago
  
  17b2a353
- [eacsl] Update tests · f14e917c
  Basile Desloges authored 4 years ago
  
  f14e917c
- [eacsl] Fix heap initialization during reallocation · 424081d4
  Basile Desloges authored 4 years ago
  
  424081d4
Nov 13, 2020
- [eacsl] Fix testing of heap initialization · d4c7bcc7
  Basile Desloges authored 4 years ago
  
  d4c7bcc7
Oct 26, 2020
- [eacsl] Fix E-ACSL source distribution · 31326420
  Basile Desloges authored 4 years ago
  
  - Include all C files - Include dev oracles
  31326420
Oct 23, 2020
- Prepare Changelogs for 22.0-Titanium · 51235bfa
  Allan Blanchard authored 4 years ago
  
  51235bfa
Oct 15, 2020
- [eacsl] Add tests for memory models compilation · 078a1a27
  Basile Desloges authored 4 years ago
  
  078a1a27
- [eacsl] Fix bittree model compilation · 4774cd29
  Basile Desloges authored 4 years ago
  
  4774cd29
- several updates related to newer OCaml compiler version · b9a92229
  Andre Maroneze authored 4 years ago
  
  b9a92229
Oct 14, 2020
- [eacsl][variadic] Update changelogs · e882d048
  Basile Desloges authored 4 years ago
  
  e882d048
- [eacsl] Update tests · c8704c5d
  Basile Desloges authored 4 years ago
  
  c8704c5d
- [eacsl] Remove `-variadic-no-translation` when calling E-ACSL · df56487d
  Basile Desloges authored 4 years ago
  
  df56487d
- [eacsl] Variadic translation is incompatible with `-e-acsl-validate-format-string` · b1ecbcfb
  Basile Desloges authored 4 years ago
  
  b1ecbcfb
- [eacsl] Don't process Variadic generated functions · ba25aa73
  Basile Desloges authored 4 years ago
  
  ba25aa73
Oct 13, 2020
- [eacsl] Add test for debug RTL compilation · 15a5ef12
  Basile Desloges authored 4 years ago
  
  15a5ef12
- [eacsl] Fix RTL function prefix in debug compilation · cdd24213
  Basile Desloges authored 4 years ago
  
  cdd24213
Oct 09, 2020
- [eacsl] Fix warning when compiling RTL · 76068771
  Basile Desloges authored 4 years ago
  
  76068771
- [eacsl] Fix paper name in segment tracking comment · ec69ae60
  Basile Desloges authored 4 years ago
  
  ec69ae60
Oct 06, 2020
- [eacsl:runtime] Factorize segment indexes in `validate_shadow_layout()` · 0a6bb3d7
  Basile Desloges authored 4 years ago
  
  0a6bb3d7
- [eacsl:runtime] Use address conversion specifier for the messages when validating the shadow layout · af701914
  Basile Desloges authored 4 years ago
  
  af701914
- [eacsl:runtime] Add `eacsl` prefix to C defines · 82788932
  Basile Desloges authored 4 years ago
  
  82788932
- [eacsl:runtime] Merge RTL pragmas into the user's AST · e5faf939
  Basile Desloges authored 4 years ago
  
  e5faf939
- [eacsl:runtime] Add segment name in the message for failed validation · 620fc8b2
  Basile Desloges authored 4 years ago
  
  620fc8b2
- [eacsl:runtime] Print layout in debug verbose · 1041de0a
  Basile Desloges authored 4 years ago
  
  1041de0a
- [eacsl:codegen] Move `Memory_translate.exp_to_base_and_baseaddr` to `Misc.ptr_base` · c3a9599d
  Basile Desloges authored 4 years ago
  
  c3a9599d
- [eacsl:codegen] Move `Misc.mk_ptr_sizeof` to `Smart_exp.ptr_sizeof` · c9e1c224
  Basile Desloges authored 4 years ago
  
  c9e1c224
- [eacsl:doc] Update changelog · 86b4dbeb
  Basile Desloges authored 4 years ago
  
  86b4dbeb
- [eacsl:doc] Update reference and implementation manual · ad6228ad
  Basile Desloges authored 4 years ago
  
  ad6228ad
- [eacsl:doc] Update comments · 3a59ad27
  Basile Desloges authored 4 years ago
  
  3a59ad27
- [eacsl] Update tests · a8fe2b10
  Basile Desloges authored 4 years ago
  
  a8fe2b10
- [eacsl:codegen] Fix soundness bug when translating a range with a logic variable · 35d900fa
  Basile Desloges authored 4 years ago
  
  35d900fa
- [eacsl:runtime] Fix `\valid` and `\valid_read` when the memory location is an empty set · 4ad7247c
  Basile Desloges authored 4 years ago
  
  4ad7247c
- [eacsl:tests] Add tests for `\separated` · e27b38d2
  Basile Desloges authored 4 years ago
  
  e27b38d2
- [eacsl:codegen] Add support of `\separated` for non-explicit range · 7b0eea9f
  Basile Desloges authored 4 years ago
  
  7b0eea9f
- [eacsl:codegen] Add support of `\separated` for explicit range · 9bde4b5d
  Basile Desloges authored 4 years ago
  
  9bde4b5d
- [eacsl:runtime] Add a C function for the `separated` predicate · 8f5e8808
  Basile Desloges authored 4 years ago
  
  8f5e8808
Sep 23, 2020
- [eacsl:doc] Update changelog · 217dc987
  Basile Desloges authored 4 years ago
  
  217dc987
- [eacsl:doc] Update reference manual to add support of complete and disjoint behavior · 8c497fbf
  Basile Desloges authored 4 years ago
  
  8c497fbf
- [eacsl:tests] Update tests oracles · dfdaaf67
  Basile Desloges authored 4 years ago
  
  dfdaaf67