Commits · 79c5b7bc8360f70e260f7dbf8c882884248efa52 · pub / frama-c · GitLab

19 Oct, 2020 8 commits
- [MdR] fix deterministic sarif output to pass validation · 37dc88a3
  Virgile Prevosto authored Oct 19, 2020
  
  37dc88a3
- [Filepath/MdR] fix issues with PWD in to_base_uri and SARIF reports · beb92eac
  Andre Maroneze authored Oct 15, 2020
  
  beb92eac
- [Markdown-report] add option -mdr-sarif-deterministic and test · 32a822dd
  Andre Maroneze authored Oct 14, 2020
  
  32a822dd
- [Markdown-report] placate SARIF validator · 17b9a5b7
  Andre Maroneze authored Oct 08, 2020
  
  17b9a5b7
- [Filepath] omit initial '/' in to_base_uri · 0c093eba
  Andre Maroneze authored Oct 08, 2020
  
  0c093eba
- [Markdown-report] add option -mdr-print-libc/-mdr-no-print-libc · 6d52012b
  Andre Maroneze authored Sep 23, 2020
  
  6d52012b
- [Markdown-report] pretty-print paths and add baseUris · 84f54ed0
  Andre Maroneze authored Oct 08, 2020
  
  84f54ed0
- [wp] commit all residuals in prover script · a5a4a2c5
  Loïc Correnson authored Oct 16, 2020 and Allan Blanchard committed Oct 19, 2020
```
(cherry picked from commit c7db4956edbec05151fd4a298ae856a6ac10b404)
```
  a5a4a2c5
16 Oct, 2020 1 commit
- [wp] Test: check that array defs are not shared · 08b3a7ae
  Allan Blanchard authored Oct 16, 2020
  
  08b3a7ae
15 Oct, 2020 14 commits
- [eacsl] Add tests for memory models compilation · 078a1a27
  Basile Desloges authored Oct 15, 2020
  
  078a1a27
- [eacsl] Fix bittree model compilation · 4774cd29
  Basile Desloges authored Oct 15, 2020
  
  4774cd29
- [wp] fixed init-range lemmas · f38cca53
  Loïc Correnson authored Oct 15, 2020
  
  f38cca53
- [wp] refactor matrix loaders · a25e5e7e
  Loïc Correnson authored Oct 15, 2020
  
  a25e5e7e
- [wp] renamed is-array predicates · 90676872
  Loïc Correnson authored Oct 15, 2020
  
  90676872
- [wp] renamed compound operations · 2f39567a
  Loïc Correnson authored Oct 15, 2020
  
  2f39567a
- [wp] simplify pointer type · 85c0b2e5
  Loïc Correnson authored Oct 15, 2020
  
  85c0b2e5
- [wp] type utilities · 89681265
  Loïc Correnson authored Oct 15, 2020
  
  89681265
- several updates related to newer OCaml compiler version · b9a92229
  Andre Maroneze authored Oct 15, 2020
  
  b9a92229
- [Kernel] update noalloc annotations to modern OCaml · 71e0ab5d
  Andre Maroneze authored Oct 15, 2020
  
  71e0ab5d
- [wp] Clarifies Sigs.CodeSemantics.init doc · f5c9ca1d
  Allan Blanchard authored Oct 15, 2020
  
  f5c9ca1d
- [wp] Small refacto for initializers in CfgWP · 68e3b43a
  Allan Blanchard authored Oct 15, 2020
  
  68e3b43a
- [wp] Ranges in CodeSemantics: included up · 5221a79e
  Allan Blanchard authored Oct 15, 2020
  
  5221a79e
- [wp] Factorize normalization in initialized MemVar · da4f3da9
  Allan Blanchard authored Oct 15, 2020
  
  da4f3da9
14 Oct, 2020 17 commits
- [wp] MemVar: normalize offset on initialized array · 51c9d57f
  Allan Blanchard authored Oct 08, 2020
  
  51c9d57f
- [wp] Make sure that init are dispatched to MemTyped when needed · 885707e5
  Allan Blanchard authored Oct 08, 2020
  
  885707e5
- [wp] Test local_init initialized + update oracles · 940608c0
  Allan Blanchard authored Oct 08, 2020
  
  940608c0
- [wp] FIxes upper_bound on init range in semantics · 122a4bce
  Allan Blanchard authored Oct 08, 2020
  
  122a4bce
- [wp] Initialized: deals with Local_init · 837b6f2a
  Allan Blanchard authored Oct 08, 2020
  
  837b6f2a
- Add support for recursive Extended annotation in AST · f91260fb
  Lionel Blatter authored Jun 25, 2020
  
  f91260fb
- [wp] cross referencing in manual · b12b6553
  Loïc Correnson authored Oct 14, 2020
  
  b12b6553
- [wp] beautify MemoryContext · d628c429
  Loïc Correnson authored Oct 14, 2020
  
  d628c429
- [eacsl][variadic] Update changelogs · e882d048
  Basile Desloges authored Oct 14, 2020
  
  e882d048
- [eacsl] Update tests · c8704c5d
  Basile Desloges authored Oct 09, 2020
  
  c8704c5d
- [eacsl] Remove `-variadic-no-translation` when calling E-ACSL · df56487d
  Basile Desloges authored Oct 09, 2020
  
  df56487d
- [eacsl] Variadic translation is incompatible with `-e-acsl-validate-format-string` · b1ecbcfb
  Basile Desloges authored Oct 09, 2020
  
  b1ecbcfb
- [eacsl] Don't process Variadic generated functions · ba25aa73
  Basile Desloges authored Oct 09, 2020
  
  ba25aa73
- [variadic] Fix lint · ec8dd1b7
  Basile Desloges authored Oct 09, 2020
  
  ec8dd1b7
- [variadic] Update tests · 73f98190
  Basile Desloges authored Oct 09, 2020
  
  73f98190
- [variadic] Print original functions in output · 9fef4530
  Basile Desloges authored Oct 09, 2020
  
  9fef4530
- [variadic] Store the translation · 41b68f17
  Basile Desloges authored Oct 09, 2020
  
  41b68f17