File tree Expand file tree Collapse file tree
tests/regression/witness/ghost.t Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -370,7 +370,6 @@ struct
370370 (* real beginning of the [analyze] function *)
371371 if get_bool " ana.sv-comp.enabled" then
372372 Witness. init (module FileCfg ); (* TODO: move this out of analyze_loop *)
373- YamlWitness. init () ;
374373
375374 AnalysisState. global_initialization := true ;
376375 GobConfig. earlyglobs := get_bool " exp.earlyglobs" ;
Original file line number Diff line number Diff line change @@ -541,6 +541,7 @@ let do_analyze change_info merged_AST =
541541 Messages. out := Legacy. open_out (get_string " outfile" ));
542542
543543 let module L = Printable. Liszt (CilType. Fundec ) in
544+ YamlWitness. init () ;
544545 if get_bool " justcil" then
545546 (* if we only want to print the output created by CIL: *)
546547 Cilfacade. print merged_AST
Original file line number Diff line number Diff line change 11Ghost variables declared in a YAML witness are injected into the CIL file before analysis:
22
3- $ goblint -- set witness. yaml. validate ghost. yml ghost. c
4- [Info][Deadcode] Logical lines of code (LLoC) summary:
5- live: 2
6- dead: 0
7- total lines : 2
8- [Warning][Witness] cannot validate entry of type ghost_instrumentation
9- [Info][Witness] witness validation summary:
10- confirmed: 0
11- unconfirmed: 0
12- refuted: 0
13- error: 0
14- unchecked: 0
15- unsupported: 1
16- disabled: 0
17- total validation entries: 1
3+ $ goblint --enable justcil --set dbg.justcil-printer clean --set witness.yaml.validate ghost.yml ghost.c | grep " m_locked"
4+ int m_locked = 0;
You can’t perform that action at this time.
0 commit comments