Commit 593c2891 authored by Thibault Martin's avatar Thibault Martin
Browse files

ident

parent e9caf1ac
......@@ -59,6 +59,7 @@ Authors
- Mickaël Delahaye
- Michaël Marcozzi
- Thibault Martin
Also many thanks to the rest of LTest's team:
- Nikolai Kosmatov
- Sébastien Bardin
......
......@@ -126,7 +126,7 @@ class visitor mk_label = object(self)
(* Handles inlined block to avoid annotating them *)
method! vblock b =
if not (Options.InlinedBlock.get ())
&& Cil.hasAttribute Cil.frama_c_inlined b.battrs then begin
&& Cil.hasAttribute Cil.frama_c_inlined b.battrs then begin
Stack.push true is_inlined_block;
Cil.DoChildrenPost (fun b' ->
ignore(Stack.pop is_inlined_block);
......@@ -137,8 +137,9 @@ class visitor mk_label = object(self)
Cil.DoChildren
(* Handles lannotate macro and generates mutations and labels as such :
- START, handles all if statements between START and SUCCESS
- SUCCESS, ends "annotating" zone, and generates labels
- START, handles all if statements between START and END
- END, ends "annotating" zone
- TARGET, generates labels
- DOUBLE IF, remember for the next instrumented if form
- If, mutate if expression
*)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment