[eacsl:tests] Update `print.ml` script to output E-ACSL generated globals

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