diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 3df3a71ae5..04dcfee606 100644 --- a/src/common/util/cilfacade.ml +++ b/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 diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 5d69990499..abba08fca9 100644 --- a/src/config/options.schema.json +++ b/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": diff --git a/tests/regression/55-loop-unrolling/01-simple-cases.t b/tests/regression/55-loop-unrolling/01-simple-cases.t index 3c5677086d..8539810091 100644 --- a/tests/regression/55-loop-unrolling/01-simple-cases.t +++ b/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 diff --git a/tests/regression/55-loop-unrolling/02-break.t b/tests/regression/55-loop-unrolling/02-break.t index b230ae6df9..125842394b 100644 --- a/tests/regression/55-loop-unrolling/02-break.t +++ b/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 ) ; diff --git a/tests/regression/55-loop-unrolling/03-break-right-place.t b/tests/regression/55-loop-unrolling/03-break-right-place.t index 8e87e6eebd..dd4d4f658e 100644 --- a/tests/regression/55-loop-unrolling/03-break-right-place.t +++ b/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 ) ; diff --git a/tests/regression/55-loop-unrolling/04-simple.t b/tests/regression/55-loop-unrolling/04-simple.t index 1b0a200477..dab702cc7c 100644 --- a/tests/regression/55-loop-unrolling/04-simple.t +++ b/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 ) ; diff --git a/tests/regression/55-loop-unrolling/05-continue.t b/tests/regression/55-loop-unrolling/05-continue.t index 9835d0f9c5..e8fc6c2a4a 100644 --- a/tests/regression/55-loop-unrolling/05-continue.t +++ b/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 ) ; diff --git a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t index ebbbb25ce0..8a2a6b5f5e 100644 --- a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t +++ b/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 diff --git a/tests/regression/55-loop-unrolling/07-nested-unroll.t b/tests/regression/55-loop-unrolling/07-nested-unroll.t index 39cf4205c8..8242d42805 100644 --- a/tests/regression/55-loop-unrolling/07-nested-unroll.t +++ b/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 diff --git a/tests/regression/55-loop-unrolling/08-bad.t b/tests/regression/55-loop-unrolling/08-bad.t index a57a3cb278..84724005ed 100644 --- a/tests/regression/55-loop-unrolling/08-bad.t +++ b/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) diff --git a/tests/regression/55-loop-unrolling/09-weird.t b/tests/regression/55-loop-unrolling/09-weird.t index 19cf16ff08..be6c824ab3 100644 --- a/tests/regression/55-loop-unrolling/09-weird.t +++ b/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 ) ;