Commits · 1b807716385f9ab8ebc7273bf5f8bed9bbfad276 · pub / frama-c · GitLab

Snippets Groups Projects

Oct 03, 2019
- [Variadic] Moves .c tests into .i when possible · 1b807716
  Allan Blanchard authored 5 years ago
  
  1b807716
- [Kernel] CabsVisit does not erase ghost parameters anymore · 2f1c5a53
  Allan Blanchard authored 5 years ago
  
  2f1c5a53
- [Kernel] argsToPairOfLists uses "isGhostFormalVarDecl" · 9edc0b62
  Allan Blanchard authored 5 years ago
  
  9edc0b62
- [Kernel] Cabs2Cil - ensures that formals inherit the ghost status from the function · 5ce29e51
  Allan Blanchard authored 5 years ago
  
  5ce29e51
Sep 30, 2019
- [Kernel] Failure if cparser generates attributes with ghost parameters · b01ad1e1
  Allan Blanchard authored 5 years ago
  
  b01ad1e1
- [Kernel] Improves controls on "void" parameters with ghost · 1a46c657
  Allan Blanchard authored 5 years ago
  
  1a46c657
Sep 27, 2019
- [Parsing] Removes an old comment · 5acb926f
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  5acb926f
- [Attributes] Attribute detection and deletion both strip underscores · bb5a3d41
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  bb5a3d41
- [Cil] More precise name for the ghost formal attribute · 3d8aab88
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  3d8aab88
- [AST Printing] Adds a test for pretty-printing of ghost parameters · e75ec668
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  e75ec668
- [Variadic] Fixes a bug related to pointer to function with ghost parameters · 745808de
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  745808de
- [Tests] Removes -load-script in ghost parameters tests · b7a56c93
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  b7a56c93
- [Kernel] Adapt Infer_annotations to ghost parameters. · 6b0ea837
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  Assume that ghost parameters are well-typed.
  6b0ea837
- [Kernel] Changes the behavior of makeFormalVar to make it easier to use · 3d246b6c
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  3d246b6c
- [Kernel] Ensures that makeFormalVar can deal with ghost parameters · 8b4232b9
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  8b4232b9
- [Tests] Moves an old test related to makeFormalVar in the right dir and add a... · 550e5559
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  [Tests] Moves an old test related to makeFormalVar in the right dir and add a new test related to ghost parameters
  550e5559
- [Kernel] Adds an optional parameter for varinfo creation and simplifies ghost parameters treatment · 44eb2f6e
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  44eb2f6e
- [Tests] Ghost parameters: side-effects on ghost call · 66ee58ea
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  66ee58ea
- [Kernel - Printer] Ensures that ghost function pointers are correctly printed · f0389771
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  f0389771
- [Kernel] Propagation of ghost status from formal to fun-type does not need... · b715eaaf
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  [Kernel] Propagation of ghost status from formal to fun-type does not need ghost attribute on formal anymore
  b715eaaf
- Cabs2Cil: ensures that the local_env is ghost when dealing with ghost arguments · c5cd98bf
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  c5cd98bf
- Cabs2Cil: Ensures that tmp variable are ghost when created from a ghost local_env · 1d314b5b
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  1d314b5b
- Fixes a test · eb3fa40c
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  eb3fa40c
- Adds a test for argument with side-effetcs in ghost parameters · b1ae8fd0
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  b1ae8fd0
- Adds a test to check that ghost parameters lead to ghost formals · b9cc5751
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  b9cc5751
- Fixes function declaration compatibility check in presence of ghost parameters · d07b0c5d
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  d07b0c5d
- Adds a set of tests about the parsing of ghost parameters · 253e1c8d
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  253e1c8d
- [Variadic] ghost parameters taken in account · ba5869f1
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  ba5869f1
- Ensures that ghost function declarations lead to ghost formals · 403765b3
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  403765b3
- makeFormalVarDecl considers frama_c_ghost attribute · dcba9c74
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  dcba9c74
- [Variadic] A set of tests for the support of ghost parameters · 775d03e1
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  775d03e1
- Renames and fixes the behavior of getNameLastFormal is presence of ghost parameters for variadic · 931459d1
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  931459d1
- Makes argsToList usable again and adds a variant that differenciates ghost/non-ghosts · e0de5711
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  e0de5711
- Fixes issues with tests · d725f018
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  d725f018
- Ghost parameters pretty printing OK · 37519b3b
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  37519b3b
- Added placeholders for ghosts · 5071ca13
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  5071ca13
- Fixes ghost parameter list in declaration (removes VA_list) && makes ghosts... · 5afa52d9
  Allan Blanchard authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  Fixes ghost parameter list in declaration (removes VA_list) && makes ghosts arguments optional on call
  5afa52d9
- Add support for ghost parameter in cabs · b79d4f36
  Lionel Blatter authored 6 years ago and Virgile Prevosto committed 5 years ago
  
  b79d4f36
- WIP · 94fbd5d7
  Jean-Christophe Léchenet authored 7 years ago and Virgile Prevosto committed 5 years ago
  
  94fbd5d7
- [Parsing] Parsing of ghost parameters · 53efdd8c
  Jean-Christophe Léchenet authored 7 years ago and Virgile Prevosto committed 5 years ago
  
  Ghost parameters are parsed, but thrown after parsing
  53efdd8c