Add option dbg.justcil-printer

src/common/util/cilfacade.ml

@@ -66,7 +66,7 @@ let parse fileName =
     E.s (E.error "There were parsing errors in %s" fileName_str);
   file
 
-class myCilPrinter =
+class cleanCilPrinterClass =
 object
   inherit defaultCilPrinterClass as super
 
@@ -79,14 +79,19 @@ object
     | _ -> super#pGlobal () g
 end
 
-let dumpFile (pp: cilPrinter) (out : out_channel) (outfile: string) file =
+let cleanCilPrinter = new cleanCilPrinterClass
+
+let cleanDumpFile (pp: cilPrinter) (out : out_channel) (outfile: string) file =
   Pretty.printDepth := 99999;
   Pretty.fastMode := true;
   iterGlobals file (fun g -> dumpGlobal pp out g);
   flush out
 
 let print (fileAST: file) =
-  dumpFile (new myCilPrinter) stdout "stdout" fileAST
+  match GobConfig.get_string "dbg.justcil-printer" with
+  | "default" -> dumpFile defaultCilPrinter stdout "stdout" fileAST
+  | "clean" -> cleanDumpFile cleanCilPrinter stdout "stdout" fileAST
+  | _ -> assert false
 
 let rmTemps fileAST =
   RmUnused.removeUnused fileAST

src/config/options.schema.json

@@ -1860,6 +1860,13 @@
           "type": "string",
           "default": ""
         },
+        "justcil-printer": {
+          "title": "dbg.justcil-printer",
+          "description": "Printer to use for justcil",
+          "type": "string",
+          "enum": ["default", "clean"],
+          "default": "default"
+        },
         "timeout": {
           "title": "dbg.timeout",
           "description":

tests/regression/55-loop-unrolling/01-simple-cases.t

@@ -1,4 +1,4 @@
-  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil 01-simple-cases.c
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 01-simple-cases.c
   [Info] unrolling loop at 01-simple-cases.c:27:5-30:5 with factor 5
   [Info] unrolling loop at 01-simple-cases.c:42:5-45:19 with factor 5
   [Info] unrolling loop at 01-simple-cases.c:57:5-60:5 with factor 5

tests/regression/55-loop-unrolling/02-break.t

@@ -1,4 +1,4 @@
-  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil 02-break.c
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 02-break.c
   [Info] unrolling loop at 02-break.c:6:5-15:2 with factor 5
   extern void __goblint_check(int exp ) ;
   extern void __goblint_assume(int exp ) ;

tests/regression/55-loop-unrolling/03-break-right-place.t

@@ -1,4 +1,4 @@
-  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil 03-break-right-place.c
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 03-break-right-place.c
   [Info] unrolling loop at 03-break-right-place.c:8:5-15:5 with factor 5
   extern void __goblint_check(int exp ) ;
   extern void __goblint_assume(int exp ) ;

tests/regression/55-loop-unrolling/04-simple.t

@@ -1,4 +1,4 @@
-  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil 04-simple.c
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 04-simple.c
   [Info] unrolling loop at 04-simple.c:10:5-13:5 with factor 5
   extern void __goblint_check(int exp ) ;
   extern void __goblint_assume(int exp ) ;

tests/regression/55-loop-unrolling/05-continue.t

@@ -1,4 +1,4 @@
-  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil 05-continue.c
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 05-continue.c
   [Info] unrolling loop at 05-continue.c:9:5-17:5 with factor 5
   extern void __goblint_check(int exp ) ;
   extern void __goblint_assume(int exp ) ;

tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t

@@ -1,4 +1,4 @@
-  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil 06-simple-cases-unrolled.c
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 06-simple-cases-unrolled.c
   [Info] unrolling loop at 06-simple-cases-unrolled.c:27:5-30:5 with factor 5
   [Info] unrolling loop at 06-simple-cases-unrolled.c:42:5-45:19 with factor 5
   [Info] unrolling loop at 06-simple-cases-unrolled.c:57:5-60:5 with factor 5

tests/regression/55-loop-unrolling/07-nested-unroll.t

@@ -1,4 +1,4 @@
-  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil 07-nested-unroll.c
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 07-nested-unroll.c
   [Info] unrolling loop at 07-nested-unroll.c:7:9-9:9 with factor 5
   [Info] unrolling loop at 07-nested-unroll.c:6:5-10:5 with factor 5
   [Info] unrolling loop at 07-nested-unroll.c:13:9-15:9 with factor 5

tests/regression/55-loop-unrolling/08-bad.t

@@ -1,4 +1,4 @@
-  $ goblint --set lib.activated '[]' --set exp.unrolling-factor 1 --enable justcil 08-bad.c
+  $ goblint --set lib.activated '[]' --set exp.unrolling-factor 1 --enable justcil --set dbg.justcil-printer clean 08-bad.c
   [Info] unrolling loop at 08-bad.c:8:7-8:23 with factor 1
   [Info] unrolling loop at 08-bad.c:14:8-14:24 with factor 1
   int main(void) 

tests/regression/55-loop-unrolling/09-weird.t

@@ -1,4 +1,4 @@
-  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 2 --enable justcil 09-weird.c
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 2 --enable justcil --set dbg.justcil-printer clean 09-weird.c
   [Info] unrolling loop at 09-weird.c:8:5-11:5 with factor 2
   extern void __goblint_check(int exp ) ;
   extern void __goblint_assume(int exp ) ;