diff --git a/src/plugins/e-acsl/tests/print.ml b/src/plugins/e-acsl/tests/print.ml index da98696a1043b123459d356400232c803b028687..bcf83012c2cd7d578e01eaccc139afb346941c4c 100644 --- a/src/plugins/e-acsl/tests/print.ml +++ b/src/plugins/e-acsl/tests/print.ml @@ -20,6 +20,20 @@ (* *) (**************************************************************************) +(* return true if the global g has been generated by E-ACSL *) +let is_generated (g: Cil_datatype.Global.t) = + let name = + match g with + | GType (ti, _) -> ti.tname + | GCompTagDecl (ci, _) | GCompTag(ci, _) -> ci.cname + | GEnumTagDecl (ei, _) | GEnumTag (ei, _) -> ei.ename + | GVarDecl (vi, _) | GVar(vi, _, _) -> vi.vname + | GFun (fundec, _) -> fundec.svar.vname + | GFunDecl (_, vi, _) -> vi.vname + | _ -> "" + in + E_ACSL.Functions.RTL.is_generated_name name + module Printer_extension(X: Printer.PrinterClass) = struct class printer = object @@ -29,7 +43,8 @@ module Printer_extension(X: Printer.PrinterClass) = struct let loc, _ = Cil_datatype.Global.loc g in let file = loc.Filepath.pos_path in if file = Datatype.Filepath.dummy || - List.exists (fun s -> s = file) (Kernel.Files.get ()) + List.exists (fun s -> s = file) (Kernel.Files.get ()) || + is_generated g then super#global fmt g end