Commits · 97a2d825d7d65d5b34617544df5d7fbd9d22cf24 · Charles Southerland / frama-c · GitLab

Snippets Groups Projects

Oct 19, 2020
- [mdr] use deterministic output in test · 97a2d825
  Virgile Prevosto authored 4 years ago and Andre Maroneze committed 4 years ago
  
  97a2d825
- [MdR] test for sarif and save/load sequences · 928ab2b2
  Virgile Prevosto authored 4 years ago and Andre Maroneze committed 4 years ago
  
  928ab2b2
- [MdR] put list of invocations in correct order · e50be496
  Virgile Prevosto authored 4 years ago
  
  e50be496
- [MdR] change test dir name · 2c514004
  Virgile Prevosto authored 4 years ago
  
  2c514004
- [MdR] keep tracks of all arguments when -save/-load sequences occur · 37611ebd
  Virgile Prevosto authored 4 years ago
  
  37611ebd
- [MdR] fix deterministic sarif output to pass validation · 37dc88a3
  Virgile Prevosto authored 4 years ago
  
  37dc88a3
- [Filepath/MdR] fix issues with PWD in to_base_uri and SARIF reports · beb92eac
  Andre Maroneze authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  beb92eac
- [Markdown-report] add option -mdr-sarif-deterministic and test · 32a822dd
  Andre Maroneze authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  32a822dd
- [Markdown-report] placate SARIF validator · 17b9a5b7
  Andre Maroneze authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  17b9a5b7
- [Filepath] omit initial '/' in to_base_uri · 0c093eba
  Andre Maroneze authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  0c093eba
- [Markdown-report] add option -mdr-print-libc/-mdr-no-print-libc · 6d52012b
  Andre Maroneze authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  6d52012b
- [Markdown-report] pretty-print paths and add baseUris · 84f54ed0
  Andre Maroneze authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  84f54ed0
Oct 16, 2020
- [wp] Test: check that array defs are not shared · 08b3a7ae
  Allan Blanchard authored 4 years ago
  
  08b3a7ae
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
- [wp] fixed init-range lemmas · f38cca53
  Loïc Correnson authored 4 years ago
  
  f38cca53
- [wp] refactor matrix loaders · a25e5e7e
  Loïc Correnson authored 4 years ago
  
  a25e5e7e
- [wp] renamed is-array predicates · 90676872
  Loïc Correnson authored 4 years ago
  
  90676872
- [wp] renamed compound operations · 2f39567a
  Loïc Correnson authored 4 years ago
  
  2f39567a
- [wp] simplify pointer type · 85c0b2e5
  Loïc Correnson authored 4 years ago
  
  85c0b2e5
- [wp] type utilities · 89681265
  Loïc Correnson authored 4 years ago
  
  89681265
- several updates related to newer OCaml compiler version · b9a92229
  Andre Maroneze authored 4 years ago
  
  b9a92229
- [Kernel] update noalloc annotations to modern OCaml · 71e0ab5d
  Andre Maroneze authored 4 years ago
  
  71e0ab5d
- [wp] Clarifies Sigs.CodeSemantics.init doc · f5c9ca1d
  Allan Blanchard authored 4 years ago
  
  f5c9ca1d
- [wp] Small refacto for initializers in CfgWP · 68e3b43a
  Allan Blanchard authored 4 years ago
  
  68e3b43a
- [wp] Ranges in CodeSemantics: included up · 5221a79e
  Allan Blanchard authored 4 years ago
  
  5221a79e
- [wp] Factorize normalization in initialized MemVar · da4f3da9
  Allan Blanchard authored 4 years ago
  
  da4f3da9
Oct 14, 2020
- [wp] MemVar: normalize offset on initialized array · 51c9d57f
  Allan Blanchard authored 4 years ago
  
  51c9d57f
- [wp] Make sure that init are dispatched to MemTyped when needed · 885707e5
  Allan Blanchard authored 4 years ago
  
  885707e5
- [wp] Test local_init initialized + update oracles · 940608c0
  Allan Blanchard authored 4 years ago
  
  940608c0
- [wp] FIxes upper_bound on init range in semantics · 122a4bce
  Allan Blanchard authored 4 years ago
  
  122a4bce
- [wp] Initialized: deals with Local_init · 837b6f2a
  Allan Blanchard authored 4 years ago
  
  837b6f2a
- Add support for recursive Extended annotation in AST · f91260fb
  Lionel Blatter authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  f91260fb
- [wp] cross referencing in manual · b12b6553
  Loïc Correnson authored 4 years ago
  
  b12b6553
- [wp] beautify MemoryContext · d628c429
  Loïc Correnson authored 4 years ago
  
  d628c429
- [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