From ec68199b41d152a0d2bd8b5307c1bc18a3454ed8 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Feb 2022 13:28:16 +0200
Subject: [PATCH 01/12] Use .goblint directory for basic preprocessing

---
 .gitignore              |  2 +-
 src/util/goblintutil.ml | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/.gitignore b/.gitignore
index 8e15e92965..affdc5d5e0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -28,7 +28,7 @@ tests/regression/16-relinv/flags.json
 tests/regression/*/goblint_temp
 linux-headers
 
-.goblint/*
+.goblint*/
 goblint_temp_*/
 
 src/spec/graph
diff --git a/src/util/goblintutil.ml b/src/util/goblintutil.ml
index 20cfab3d6d..abca36937b 100644
--- a/src/util/goblintutil.ml
+++ b/src/util/goblintutil.ml
@@ -100,12 +100,12 @@ let create_temp_dir () =
   if Sys.file_exists (get_string "tempDir") then
     tempDirName := get_string "tempDir"
   else
-    (* Using the stdlib to create a free tmp file name. *)
-    let tmpDirRel = Filename.temp_file ~temp_dir:"" "goblint_temp_" "" in
-    (* ... and then delete it to create a directory instead. *)
-    Sys.remove tmpDirRel;
-    let tmpDirName = create_dir tmpDirRel in
-    tempDirName := tmpDirName
+    (* TODO: generalize .goblint for everything *)
+    ignore (create_dir ".goblint");
+    let preprocessed_dir = create_dir (Filename.concat ".goblint" "preprocessed") in
+    assert (Sys.file_exists preprocessed_dir);
+    (* raise Exit; *)
+    tempDirName := preprocessed_dir
 
 let remove_temp_dir () =
   if not (get_bool "keepcpp") then ignore (rm_rf !tempDirName)

From c0784ce830189316f81d22866c07c1c20a33ffb7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Feb 2022 13:31:05 +0200
Subject: [PATCH 02/12] Rename option keepcpp -> pre.keep

---
 src/util/goblintutil.ml      |  2 +-
 src/util/options.schema.json | 22 +++++++++++++++-------
 2 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/util/goblintutil.ml b/src/util/goblintutil.ml
index abca36937b..c7c35f4831 100644
--- a/src/util/goblintutil.ml
+++ b/src/util/goblintutil.ml
@@ -108,7 +108,7 @@ let create_temp_dir () =
     tempDirName := preprocessed_dir
 
 let remove_temp_dir () =
-  if not (get_bool "keepcpp") then ignore (rm_rf !tempDirName)
+  if not (get_bool "pre.keep") then ignore (rm_rf !tempDirName)
 
 exception Timeout
 
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 4722162d04..972287d1ff 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -88,13 +88,6 @@
       "type": "boolean",
       "default": false
     },
-    "keepcpp": {
-      "title": "keepcpp",
-      "description":
-        "Keep the intermediate output of running the C preprocessor.",
-      "type": "boolean",
-      "default": false
-    },
     "tempDir": {
       "title": "tempDir",
       "description": "Reuse temporary directory for preprocessed files.",
@@ -223,6 +216,21 @@
       "type": "integer",
       "default": 1
     },
+    "pre": {
+      "title": "Preprocessing",
+      "description": "Preprocessing options",
+      "type": "object",
+      "properties": {
+        "keep": {
+          "title": "pre.keep",
+          "description":
+            "Keep the intermediate output of running the C preprocessor.",
+          "type": "boolean",
+          "default": false
+        }
+      },
+      "additionalProperties": false
+    },
     "server": {
       "title": "Server",
       "description": "Server mode",

From 4f2829fa58f41ab29e84224a51e67d51b3bd8b64 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Feb 2022 13:35:07 +0200
Subject: [PATCH 03/12] Add option pre.exist

---
 src/maingoblint.ml           | 2 +-
 src/util/options.schema.json | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 5808350b10..09ce05a942 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -140,7 +140,7 @@ let handle_flags () =
 let basic_preprocess ~all_cppflags fname =
   (* The actual filename of the preprocessed sourcefile *)
   let nname =  Filename.concat !Goblintutil.tempDirName (Filename.basename fname) in
-  if Sys.file_exists (get_string "tempDir") then
+  if get_bool "pre.exist" then (* TODO: also support for compilation database *)
     (nname, None)
   else
     (* Preprocess using cpp. *)
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 972287d1ff..310c6ac1fe 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -227,6 +227,12 @@
             "Keep the intermediate output of running the C preprocessor.",
           "type": "boolean",
           "default": false
+        },
+        "exist": {
+          "title": "pre.exist",
+          "description": "Use existing preprocessed files.",
+          "type": "boolean",
+          "default": false
         }
       },
       "additionalProperties": false

From aa42fff96eeeeac866c9cbccbdcf888fa09b4765 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Feb 2022 13:37:31 +0200
Subject: [PATCH 04/12] Use .i extension for basic preprocessing

---
 src/maingoblint.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 09ce05a942..cf141cfc6c 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -139,7 +139,7 @@ let handle_flags () =
 (** Use gcc to preprocess a file. Returns the path to the preprocessed file. *)
 let basic_preprocess ~all_cppflags fname =
   (* The actual filename of the preprocessed sourcefile *)
-  let nname =  Filename.concat !Goblintutil.tempDirName (Filename.basename fname) in
+  let nname =  Filename.concat !Goblintutil.tempDirName (Filename.chop_extension (Filename.basename fname) ^ ".i") in
   if get_bool "pre.exist" then (* TODO: also support for compilation database *)
     (nname, None)
   else

From 63489badf9e2b036b670b5b8bee967f3a98bdb89 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Feb 2022 14:12:30 +0200
Subject: [PATCH 05/12] Remove .goblint directory if empty

---
 src/util/gobSys.ml      | 6 ++++++
 src/util/goblintutil.ml | 4 +++-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/util/gobSys.ml b/src/util/gobSys.ml
index 4bb5122485..53068fff0f 100644
--- a/src/util/gobSys.ml
+++ b/src/util/gobSys.ml
@@ -6,3 +6,9 @@ let rec mkdir_parents filename =
     mkdir_parents dirname;
     Unix.mkdir dirname 0o770; (* TODO: what permissions? *)
   )
+
+let rmdir_if_empty dirname =
+  try
+    Unix.rmdir dirname
+  with Unix.Unix_error (Unix.ENOTEMPTY, _, _) ->
+    ()
diff --git a/src/util/goblintutil.ml b/src/util/goblintutil.ml
index c7c35f4831..8f1b3e39c3 100644
--- a/src/util/goblintutil.ml
+++ b/src/util/goblintutil.ml
@@ -108,7 +108,9 @@ let create_temp_dir () =
     tempDirName := preprocessed_dir
 
 let remove_temp_dir () =
-  if not (get_bool "pre.keep") then ignore (rm_rf !tempDirName)
+  if not (get_bool "pre.keep") then
+    ignore (rm_rf !tempDirName);
+  GobSys.rmdir_if_empty ".goblint"
 
 exception Timeout
 

From 679b59bedf58d6791a6db8e4545cb0a10e2d284a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Feb 2022 14:18:12 +0200
Subject: [PATCH 06/12] Extract tempDir to GoblintDir module

---
 src/goblint.ml          |  4 ++--
 src/maingoblint.ml      |  4 ++--
 src/util/goblintDir.ml  | 21 +++++++++++++++++++++
 src/util/goblintutil.ml | 19 -------------------
 src/util/oilUtil.ml     |  2 +-
 src/util/server.ml      |  4 ++--
 6 files changed, 28 insertions(+), 26 deletions(-)
 create mode 100644 src/util/goblintDir.ml

diff --git a/src/goblint.ml b/src/goblint.ml
index d90053e10f..60768e2584 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -17,13 +17,13 @@ let main () =
     Cilfacade.init ();
 
     handle_extraspecials ();
-    create_temp_dir ();
+    GoblintDir.create_temp_dir ();
     handle_flags ();
     if get_bool "dbg.verbose" then (
       print_endline (localtime ());
       print_endline command;
     );
-    let file = Fun.protect ~finally:remove_temp_dir preprocess_and_merge in
+    let file = Fun.protect ~finally:GoblintDir.remove_temp_dir preprocess_and_merge in
     if get_bool "server.enabled" then Server.start file else (
       let changeInfo = if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then diff_and_rename file else Analyses.empty_increment_data file in
       file|> do_analyze changeInfo;
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index cf141cfc6c..1f0cd11fa0 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -139,7 +139,7 @@ let handle_flags () =
 (** Use gcc to preprocess a file. Returns the path to the preprocessed file. *)
 let basic_preprocess ~all_cppflags fname =
   (* The actual filename of the preprocessed sourcefile *)
-  let nname =  Filename.concat !Goblintutil.tempDirName (Filename.chop_extension (Filename.basename fname) ^ ".i") in
+  let nname =  Filename.concat !GoblintDir.tempDirName (Filename.chop_extension (Filename.basename fname) ^ ".i") in
   if get_bool "pre.exist" then (* TODO: also support for compilation database *)
     (nname, None)
   else
@@ -188,7 +188,7 @@ let preprocess_files () =
 
   (* fill include flags *)
   let one_include_f f x = include_dirs := f x :: !include_dirs in
-  if get_string "ana.osek.oil" <> "" then include_files := Filename.concat !Goblintutil.tempDirName OilUtil.header :: !include_files;
+  if get_string "ana.osek.oil" <> "" then include_files := Filename.concat !GoblintDir.tempDirName OilUtil.header :: !include_files;
   (* if get_string "ana.osek.tramp" <> "" then include_files := get_string "ana.osek.tramp" :: !include_files; *)
   get_string_list "includes" |> List.iter (one_include_f identity);
 
diff --git a/src/util/goblintDir.ml b/src/util/goblintDir.ml
new file mode 100644
index 0000000000..b8de00b105
--- /dev/null
+++ b/src/util/goblintDir.ml
@@ -0,0 +1,21 @@
+open GobConfig
+
+(** Temp directory, set by create_temp_dir, but used by the OSEK analysis. *)
+let tempDirName = ref "goblint_temp"
+
+(* The temp directory for preprocessing the input files *)
+let create_temp_dir () =
+  if Sys.file_exists (get_string "tempDir") then
+    tempDirName := get_string "tempDir"
+  else
+    (* TODO: generalize .goblint for everything *)
+    ignore (Goblintutil.create_dir ".goblint");
+    let preprocessed_dir = Goblintutil.create_dir (Filename.concat ".goblint" "preprocessed") in
+    assert (Sys.file_exists preprocessed_dir);
+    (* raise Exit; *)
+    tempDirName := preprocessed_dir
+
+let remove_temp_dir () =
+  if not (get_bool "pre.keep") then
+    ignore (Goblintutil.rm_rf !tempDirName);
+  GobSys.rmdir_if_empty ".goblint"
diff --git a/src/util/goblintutil.ml b/src/util/goblintutil.ml
index 8f1b3e39c3..6411571c24 100644
--- a/src/util/goblintutil.ml
+++ b/src/util/goblintutil.ml
@@ -23,9 +23,6 @@ let inthack = Int64.of_int (-19012009) (* TODO do we still need this? *)
 (** The file where everything is output *)
 let out = ref stdout
 
-(** Temp directory, set by create_temp_dir, but used by the OSEK analysis. *)
-let tempDirName = ref "goblint_temp"
-
 (** Command for assigning an id to a varinfo. All varinfos directly created by Goblint should be modified by this method *)
 let create_var (var: varinfo) =
   (* TODO Hack: this offset should preempt conflicts with ids generated by CIL *)
@@ -95,22 +92,6 @@ let rm_rf path =
   in
   f path
 
-(* The temp directory for preprocessing the input files *)
-let create_temp_dir () =
-  if Sys.file_exists (get_string "tempDir") then
-    tempDirName := get_string "tempDir"
-  else
-    (* TODO: generalize .goblint for everything *)
-    ignore (create_dir ".goblint");
-    let preprocessed_dir = create_dir (Filename.concat ".goblint" "preprocessed") in
-    assert (Sys.file_exists preprocessed_dir);
-    (* raise Exit; *)
-    tempDirName := preprocessed_dir
-
-let remove_temp_dir () =
-  if not (get_bool "pre.keep") then
-    ignore (rm_rf !tempDirName);
-  GobSys.rmdir_if_empty ".goblint"
 
 exception Timeout
 
diff --git a/src/util/oilUtil.ml b/src/util/oilUtil.ml
index f80966ab2a..0674be6338 100644
--- a/src/util/oilUtil.ml
+++ b/src/util/oilUtil.ml
@@ -99,7 +99,7 @@ let is_starting f = (List.mem f !concurrent_tasks) || (List.mem f !starting_task
 
 (*print id header *)
 let generate_header () =
-  let f = open_out (Filename.concat !Goblintutil.tempDirName header) in
+  let f = open_out (Filename.concat !GoblintDir.tempDirName header) in
   let print_resources id value = if not(is_task_res id) then output_string f ("int " ^ id ^ ";\n") else () in
   let print_events id value 	 = output_string f ("int " ^ id           ^ ";\n") in
   let print_tasks id value     = output_string f ("int " ^ trim_task id ^ ";\n") in
diff --git a/src/util/server.ml b/src/util/server.ml
index 02459dd764..d613e54d5e 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -110,8 +110,8 @@ let start file =
 
 let reparse (s: t) =
   if GobConfig.get_bool "server.reparse" then (
-    Goblintutil.create_temp_dir ();
-    Fun.protect ~finally:Goblintutil.remove_temp_dir Maingoblint.preprocess_and_merge, true)
+    GoblintDir.create_temp_dir ();
+    Fun.protect ~finally:GoblintDir.remove_temp_dir Maingoblint.preprocess_and_merge, true)
   else s.file, false
 
 (* Only called when the file has not been reparsed, so we can skip the expensive CFG comparison. *)

From 2b3d9b50a36ef23545e96a4c4f39848ef174c9ac Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Feb 2022 14:43:13 +0200
Subject: [PATCH 07/12] Replace tempDir with goblint-dir

---
 src/goblint.ml                  |  4 ++--
 src/maingoblint.ml              |  4 ++--
 src/util/compilationDatabase.ml |  4 +---
 src/util/goblintDir.ml          | 26 ++++++++++----------------
 src/util/oilUtil.ml             |  2 +-
 src/util/options.schema.json    | 12 ++++++------
 src/util/server.ml              |  4 ++--
 7 files changed, 24 insertions(+), 32 deletions(-)

diff --git a/src/goblint.ml b/src/goblint.ml
index 60768e2584..7b635d770a 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -17,13 +17,13 @@ let main () =
     Cilfacade.init ();
 
     handle_extraspecials ();
-    GoblintDir.create_temp_dir ();
+    GoblintDir.init ();
     handle_flags ();
     if get_bool "dbg.verbose" then (
       print_endline (localtime ());
       print_endline command;
     );
-    let file = Fun.protect ~finally:GoblintDir.remove_temp_dir preprocess_and_merge in
+    let file = Fun.protect ~finally:GoblintDir.finalize preprocess_and_merge in
     if get_bool "server.enabled" then Server.start file else (
       let changeInfo = if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then diff_and_rename file else Analyses.empty_increment_data file in
       file|> do_analyze changeInfo;
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 1f0cd11fa0..ec2ad6b4a7 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -139,7 +139,7 @@ let handle_flags () =
 (** Use gcc to preprocess a file. Returns the path to the preprocessed file. *)
 let basic_preprocess ~all_cppflags fname =
   (* The actual filename of the preprocessed sourcefile *)
-  let nname =  Filename.concat !GoblintDir.tempDirName (Filename.chop_extension (Filename.basename fname) ^ ".i") in
+  let nname =  Filename.concat (GoblintDir.preprocessed ()) (Filename.chop_extension (Filename.basename fname) ^ ".i") in
   if get_bool "pre.exist" then (* TODO: also support for compilation database *)
     (nname, None)
   else
@@ -188,7 +188,7 @@ let preprocess_files () =
 
   (* fill include flags *)
   let one_include_f f x = include_dirs := f x :: !include_dirs in
-  if get_string "ana.osek.oil" <> "" then include_files := Filename.concat !GoblintDir.tempDirName OilUtil.header :: !include_files;
+  if get_string "ana.osek.oil" <> "" then include_files := Filename.concat (GoblintDir.preprocessed ()) OilUtil.header :: !include_files;
   (* if get_string "ana.osek.tramp" <> "" then include_files := get_string "ana.osek.tramp" :: !include_files; *)
   get_string_list "includes" |> List.iter (one_include_f identity);
 
diff --git a/src/util/compilationDatabase.ml b/src/util/compilationDatabase.ml
index ee4115d926..2cbcd9f7ce 100644
--- a/src/util/compilationDatabase.ml
+++ b/src/util/compilationDatabase.ml
@@ -33,9 +33,7 @@ let load_and_preprocess ~all_cppflags filename =
     else
       Fun.id
   in
-  (* TODO: generalize .goblint for everything *)
-  ignore (Goblintutil.create_dir ".goblint");
-  let preprocessed_dir = Goblintutil.create_dir (Filename.concat ".goblint" "preprocessed") in
+  let preprocessed_dir = GobFilename.absolute (GoblintDir.preprocessed ()) in (* absolute due to cwd changes *)
   let preprocess obj =
     let file = obj.file in
     let extension = Filename.extension file in
diff --git a/src/util/goblintDir.ml b/src/util/goblintDir.ml
index b8de00b105..2cc0fbd5f2 100644
--- a/src/util/goblintDir.ml
+++ b/src/util/goblintDir.ml
@@ -1,21 +1,15 @@
 open GobConfig
 
-(** Temp directory, set by create_temp_dir, but used by the OSEK analysis. *)
-let tempDirName = ref "goblint_temp"
+let root () = get_string "goblint-dir"
 
-(* The temp directory for preprocessing the input files *)
-let create_temp_dir () =
-  if Sys.file_exists (get_string "tempDir") then
-    tempDirName := get_string "tempDir"
-  else
-    (* TODO: generalize .goblint for everything *)
-    ignore (Goblintutil.create_dir ".goblint");
-    let preprocessed_dir = Goblintutil.create_dir (Filename.concat ".goblint" "preprocessed") in
-    assert (Sys.file_exists preprocessed_dir);
-    (* raise Exit; *)
-    tempDirName := preprocessed_dir
+let preprocessed () = Filename.concat (root ()) "preprocessed"
 
-let remove_temp_dir () =
+let init () =
+  (* TODO: generalize .goblint for everything *)
+  ignore (Goblintutil.create_dir (root ()));
+  ignore (Goblintutil.create_dir (preprocessed ()))
+
+let finalize () =
   if not (get_bool "pre.keep") then
-    ignore (Goblintutil.rm_rf !tempDirName);
-  GobSys.rmdir_if_empty ".goblint"
+    ignore (Goblintutil.rm_rf (preprocessed ()));
+  GobSys.rmdir_if_empty (root ())
diff --git a/src/util/oilUtil.ml b/src/util/oilUtil.ml
index 0674be6338..237aca6470 100644
--- a/src/util/oilUtil.ml
+++ b/src/util/oilUtil.ml
@@ -99,7 +99,7 @@ let is_starting f = (List.mem f !concurrent_tasks) || (List.mem f !starting_task
 
 (*print id header *)
 let generate_header () =
-  let f = open_out (Filename.concat !GoblintDir.tempDirName header) in
+  let f = open_out (Filename.concat (GoblintDir.preprocessed ()) header) in
   let print_resources id value = if not(is_task_res id) then output_string f ("int " ^ id ^ ";\n") else () in
   let print_events id value 	 = output_string f ("int " ^ id           ^ ";\n") in
   let print_tasks id value     = output_string f ("int " ^ trim_task id ^ ";\n") in
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 310c6ac1fe..fa4e1c5b02 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -88,12 +88,6 @@
       "type": "boolean",
       "default": false
     },
-    "tempDir": {
-      "title": "tempDir",
-      "description": "Reuse temporary directory for preprocessed files.",
-      "type": "string",
-      "default": ""
-    },
     "cppflags": {
       "title": "cppflags",
       "description": "Pre-processing parameters.",
@@ -216,6 +210,12 @@
       "type": "integer",
       "default": 1
     },
+    "goblint-dir": {
+      "title": "goblint-dir",
+      "description": "Directory used for intermediate data.",
+      "type": "string",
+      "default": ".goblint"
+    },
     "pre": {
       "title": "Preprocessing",
       "description": "Preprocessing options",
diff --git a/src/util/server.ml b/src/util/server.ml
index d613e54d5e..e64d4b36e6 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -110,8 +110,8 @@ let start file =
 
 let reparse (s: t) =
   if GobConfig.get_bool "server.reparse" then (
-    GoblintDir.create_temp_dir ();
-    Fun.protect ~finally:GoblintDir.remove_temp_dir Maingoblint.preprocess_and_merge, true)
+    GoblintDir.init ();
+    Fun.protect ~finally:GoblintDir.finalize Maingoblint.preprocess_and_merge, true)
   else s.file, false
 
 (* Only called when the file has not been reparsed, so we can skip the expensive CFG comparison. *)

From 6e8a284fe2f0e91bca9f711246de5fdcdf8cf873 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Feb 2022 14:50:50 +0200
Subject: [PATCH 08/12] Fix goblint-dir in parallel test execution

---
 scripts/update_suite.rb | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb
index 51fa8b1603..c5717cc5e7 100755
--- a/scripts/update_suite.rb
+++ b/scripts/update_suite.rb
@@ -357,7 +357,7 @@ def run_testset (testset, cmd, starttime)
 
   def run
     filename = File.basename(@path)
-    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code 2>#{@testset.statsfile}"
+    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --set goblint-dir .goblint-#{@id.sub('/','-')} 2>#{@testset.statsfile}"
     starttime = Time.now
     run_testset(@testset, cmd, starttime)
   end
@@ -418,8 +418,8 @@ def create_test_set(lines)
 
   def run
     filename = File.basename(@path)
-    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --enable incremental.save 2>#{@testset.statsfile}"
-    cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --set printstats true --enable dbg.print_dead_code --enable incremental.load 2>#{@testset_incr.statsfile}"
+    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --enable incremental.save --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-save 2>#{@testset.statsfile}"
+    cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --set printstats true --enable dbg.print_dead_code --enable incremental.load --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-load 2>#{@testset_incr.statsfile}"
     starttime = Time.now
     run_testset(@testset_incr, cmd, starttime)
     # apply patch
@@ -462,8 +462,8 @@ def create_test_set(lines)
   end
   def run ()
     filename = File.basename(@path)
-    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --set save_run run  2>#{@testset.statsfile}"
-    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --conf run/config.json --set save_run '' --set load_run run  2>#{@testset.statsfile}"
+    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --set save_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-save 2>#{@testset.statsfile}"
+    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --conf run/config.json --set save_run '' --set load_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-load 2>#{@testset.statsfile}"
     starttime = Time.now
     run_testset(@testset, cmd1, starttime)
     run_testset(@testset, cmd2, starttime)

From 6863722f4034919c67de58dd157aa212cb1cf63e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Feb 2022 15:07:33 +0200
Subject: [PATCH 09/12] Extract GobSys.mkdir_or_exists

---
 src/framework/control.ml     |  2 +-
 src/incremental/serialize.ml |  4 ++--
 src/solvers/generic.ml       |  2 +-
 src/solvers/postSolver.ml    |  2 +-
 src/util/gobSys.ml           |  6 ++++++
 src/util/goblintDir.ml       |  4 ++--
 src/util/goblintutil.ml      | 16 ++--------------
 7 files changed, 15 insertions(+), 21 deletions(-)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index 8332b4f40a..0c55301f9e 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -468,7 +468,7 @@ struct
             if get_bool "dbg.verbose" then (
               print_endline ("Saving the current configuration to " ^ config ^ ", meta-data about this run to " ^ meta ^ ", and solver statistics to " ^ solver_stats);
             );
-            ignore @@ GU.create_dir (save_run); (* ensure the directory exists *)
+            GobSys.mkdir_or_exists save_run;
             GobConfig.write_file config;
             let module Meta = struct
                 type t = { command : string; version: string; timestamp : float; localtime : string } [@@deriving to_yojson]
diff --git a/src/incremental/serialize.ml b/src/incremental/serialize.ml
index b206b7519f..3648552132 100644
--- a/src/incremental/serialize.ml
+++ b/src/incremental/serialize.ml
@@ -65,9 +65,9 @@ let store_data (data : 'a) (data_type : incremental_data_kind) =
     | AnalysisData -> server_analysis_data := Some (Obj.repr data)
     | _ -> ()
   else (
-    ignore @@ Goblintutil.create_dir (gob_directory ());
+    GobSys.mkdir_or_exists (gob_directory ());
     let d = gob_results_tmp_dir () in
-    ignore @@ Goblintutil.create_dir d;
+    GobSys.mkdir_or_exists d;
     let p = Filename.concat d (type_to_file_name data_type) in
     marshal data p)
 
diff --git a/src/solvers/generic.ml b/src/solvers/generic.ml
index 20402c2a95..5cc78aa50c 100644
--- a/src/solvers/generic.ml
+++ b/src/solvers/generic.ml
@@ -107,7 +107,7 @@ struct
   let stats_csv =
     let save_run = GobConfig.get_string "save_run" in
     if save_run <> "" then (
-      ignore @@ Goblintutil.create_dir save_run;
+      GobSys.mkdir_or_exists save_run;
       save_run ^ Filename.dir_sep ^ "solver_stats.csv" |> open_out |> Option.some
     ) else None
   let write_csv xs oc = output_string oc @@ String.concat ",\t" xs ^ "\n"
diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml
index 0b09f166fe..8a44c51ca6 100644
--- a/src/solvers/postSolver.ml
+++ b/src/solvers/postSolver.ml
@@ -126,7 +126,7 @@ module SaveRun: F =
       let solver = Filename.concat save_run solver_file in
       if get_bool "dbg.verbose" then
         print_endline ("Saving the solver result to " ^ solver);
-      ignore @@ GU.create_dir save_run; (* ensure the directory exists *)
+      GobSys.mkdir_or_exists save_run;
       Serialize.marshal vh solver
   end
 
diff --git a/src/util/gobSys.ml b/src/util/gobSys.ml
index 53068fff0f..f7a6c8b757 100644
--- a/src/util/gobSys.ml
+++ b/src/util/gobSys.ml
@@ -7,6 +7,12 @@ let rec mkdir_parents filename =
     Unix.mkdir dirname 0o770; (* TODO: what permissions? *)
   )
 
+let mkdir_or_exists dirname =
+  try
+    Unix.mkdir dirname 0o770 (* TODO: what permissions? *)
+  with Unix.Unix_error (Unix.EEXIST, _, _) ->
+    assert (Sys.is_directory dirname) (* may exist, but as a file *)
+
 let rmdir_if_empty dirname =
   try
     Unix.rmdir dirname
diff --git a/src/util/goblintDir.ml b/src/util/goblintDir.ml
index 2cc0fbd5f2..024189fdab 100644
--- a/src/util/goblintDir.ml
+++ b/src/util/goblintDir.ml
@@ -6,8 +6,8 @@ let preprocessed () = Filename.concat (root ()) "preprocessed"
 
 let init () =
   (* TODO: generalize .goblint for everything *)
-  ignore (Goblintutil.create_dir (root ()));
-  ignore (Goblintutil.create_dir (preprocessed ()))
+  GobSys.mkdir_or_exists (root ());
+  GobSys.mkdir_or_exists (preprocessed ())
 
 let finalize () =
   if not (get_bool "pre.keep") then
diff --git a/src/util/goblintutil.ml b/src/util/goblintutil.ml
index 6411571c24..83375568a1 100644
--- a/src/util/goblintutil.ml
+++ b/src/util/goblintutil.ml
@@ -64,20 +64,8 @@ let escape = XmlUtil.escape (* TODO: inline everywhere *)
 
 (** Creates a directory and returns the absolute path **)
 let create_dir name =
-  let dirName = if Filename.is_relative name then Filename.concat (Unix.getcwd ()) name else name in
-  (* The directory should be writable to group and user *)
-  let dirPerm = 0o770 in
-  let _ =
-    try
-      Unix.mkdir dirName dirPerm
-    with Unix.Unix_error(err, ctx1, ctx) as ex ->
-      (* We can discared the EEXIST, we are happy to use the existing directory *)
-      if err != Unix.EEXIST then begin
-        (* Hopefully will be friendly enough :) *)
-        print_endline ("Error, " ^ (Unix.error_message err));
-        raise ex
-      end
-  in
+  let dirName = GobFilename.absolute name in
+  GobSys.mkdir_or_exists dirName;
   dirName
 
 (** Remove directory and its content, as "rm -rf" would do. *)

From 4c913ae21a27d548f04add0b3617c24590b38765 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Feb 2022 15:29:41 +0200
Subject: [PATCH 10/12] Extend pre.exist to compilation database

---
 src/maingoblint.ml | 27 +++++++++++++--------------
 1 file changed, 13 insertions(+), 14 deletions(-)

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index ec2ad6b4a7..e1adf8f5c0 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -140,14 +140,11 @@ let handle_flags () =
 let basic_preprocess ~all_cppflags fname =
   (* The actual filename of the preprocessed sourcefile *)
   let nname =  Filename.concat (GoblintDir.preprocessed ()) (Filename.chop_extension (Filename.basename fname) ^ ".i") in
-  if get_bool "pre.exist" then (* TODO: also support for compilation database *)
-    (nname, None)
-  else
-    (* Preprocess using cpp. *)
-    (* ?? what is __BLOCKS__? is it ok to just undef? this? http://en.wikipedia.org/wiki/Blocks_(C_language_extension) *)
-    let command = (Preprocessor.get_cpp ()) ^ " --undef __BLOCKS__ " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " \"" ^ fname ^ "\" -o \"" ^ nname ^ "\"" in
-    if get_bool "dbg.verbose" then print_endline command;
-    (nname, Some {ProcessPool.command; cwd = None})
+  (* Preprocess using cpp. *)
+  (* ?? what is __BLOCKS__? is it ok to just undef? this? http://en.wikipedia.org/wiki/Blocks_(C_language_extension) *)
+  let command = (Preprocessor.get_cpp ()) ^ " --undef __BLOCKS__ " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " \"" ^ fname ^ "\" -o \"" ^ nname ^ "\"" in
+  if get_bool "dbg.verbose" then print_endline command;
+  (nname, Some {ProcessPool.command; cwd = None})
 
 (** Preprocess all files. Return list of preprocessed files and the temp directory name. *)
 let preprocess_files () =
@@ -264,12 +261,14 @@ let preprocess_files () =
     extra_arg_files := find_custom_include "sv-comp.c" :: !extra_arg_files;
 
   let preprocessed = List.concat_map preprocess_arg_file (!extra_arg_files @ !arg_files) in
-  let preprocess_tasks = List.filter_map snd preprocessed in
-  let terminated task = function
-    | Unix.WEXITED 0 -> ()
-    | process_status -> failwith (GobUnix.string_of_process_status process_status)
-  in
-  ProcessPool.run ~jobs:(Goblintutil.jobs ()) ~terminated preprocess_tasks;
+  if not (get_bool "pre.exist") then (
+    let preprocess_tasks = List.filter_map snd preprocessed in
+    let terminated task = function
+      | Unix.WEXITED 0 -> ()
+      | process_status -> failwith (GobUnix.string_of_process_status process_status)
+    in
+    ProcessPool.run ~jobs:(Goblintutil.jobs ()) ~terminated preprocess_tasks
+  );
   List.map fst preprocessed
 
 (** Possibly merge all postprocessed files *)

From 07e66bd1f188747df75b0107361f6067d32f4499 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Feb 2022 15:34:59 +0200
Subject: [PATCH 11/12] Use Filename.quote_command for basic preprocessing

---
 src/maingoblint.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index e1adf8f5c0..561640d5cf 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -142,7 +142,8 @@ let basic_preprocess ~all_cppflags fname =
   let nname =  Filename.concat (GoblintDir.preprocessed ()) (Filename.chop_extension (Filename.basename fname) ^ ".i") in
   (* Preprocess using cpp. *)
   (* ?? what is __BLOCKS__? is it ok to just undef? this? http://en.wikipedia.org/wiki/Blocks_(C_language_extension) *)
-  let command = (Preprocessor.get_cpp ()) ^ " --undef __BLOCKS__ " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " \"" ^ fname ^ "\" -o \"" ^ nname ^ "\"" in
+  let arguments = "--undef" :: "__BLOCKS__" :: all_cppflags @ fname :: "-o" :: nname :: [] in
+  let command = Filename.quote_command (Preprocessor.get_cpp ()) arguments in
   if get_bool "dbg.verbose" then print_endline command;
   (nname, Some {ProcessPool.command; cwd = None})
 

From 5eb63ce29446e7b51b3815ac1adecc6395e1e33c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Feb 2022 17:05:41 +0200
Subject: [PATCH 12/12] Move preprocessing options to pre category

---
 .github/workflows/unlocked.yml          |  4 +-
 src/maingoblint.ml                      | 14 ++---
 src/util/options.schema.json            | 68 ++++++++++++-------------
 tests/regression/41-stdlib/03-noqsort.c |  2 +-
 4 files changed, 44 insertions(+), 44 deletions(-)

diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index f16db384d3..ba480c8eb9 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -217,8 +217,8 @@ jobs:
       - name: Symlink installed goblint to repository # because tests want to use locally built one
         run: ln -s $(opam exec -- which goblint) goblint
 
-      - name: Set gobopt with kernel-root # because linux-headers are not installed
-        run: echo "gobopt=--set kernel-root $PWD/linux-headers" >> $GITHUB_ENV
+      - name: Set gobopt with pre.kernel-root # because linux-headers are not installed
+        run: echo "gobopt=--set pre.kernel-root $PWD/linux-headers" >> $GITHUB_ENV
 
       - name: Test regression
         run: ./make.sh headers testci
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 561640d5cf..cf58c5a857 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -76,8 +76,8 @@ let option_spec_list =
   [ "-o"                   , Arg.String (set_string "outfile"), ""
   ; "-v"                   , Arg.Unit (fun () -> set_bool "dbg.verbose" true; set_bool "printstats" true), ""
   ; "-j"                   , Arg.Int (set_int "jobs"), ""
-  ; "-I"                   , Arg.String (set_string "includes[+]"), ""
-  ; "-IK"                  , Arg.String (set_string "kernel_includes[+]"), ""
+  ; "-I"                   , Arg.String (set_string "pre.includes[+]"), ""
+  ; "-IK"                  , Arg.String (set_string "pre.kernel_includes[+]"), ""
   ; "--set"                , Arg.Tuple [Arg.Set_string tmp_arg; Arg.String (fun x -> set_auto !tmp_arg x)], ""
   ; "--sets"               , Arg.Tuple [Arg.Set_string tmp_arg; Arg.String (fun x -> prerr_endline "--sets is deprecated, use --set instead."; set_string !tmp_arg x)], ""
   ; "--enable"             , Arg.String (fun x -> set_bool x true), ""
@@ -152,11 +152,11 @@ let preprocess_files () =
   Hashtbl.clear Preprocessor.dependencies; (* clear for server mode *)
 
   (* Preprocessor flags *)
-  let cppflags = ref (get_string_list "cppflags") in
+  let cppflags = ref (get_string_list "pre.cppflags") in
 
   (* the base include directory *)
   let custom_include_dirs =
-    get_string_list "custom_includes" @
+    get_string_list "pre.custom_includes" @
     Filename.concat exe_dir "includes" ::
     Goblint_sites.includes
   in
@@ -188,14 +188,14 @@ let preprocess_files () =
   let one_include_f f x = include_dirs := f x :: !include_dirs in
   if get_string "ana.osek.oil" <> "" then include_files := Filename.concat (GoblintDir.preprocessed ()) OilUtil.header :: !include_files;
   (* if get_string "ana.osek.tramp" <> "" then include_files := get_string "ana.osek.tramp" :: !include_files; *)
-  get_string_list "includes" |> List.iter (one_include_f identity);
+  get_string_list "pre.includes" |> List.iter (one_include_f identity);
 
   include_dirs := custom_include_dirs @ !include_dirs;
 
   (* If we analyze a kernel module, some special includes are needed. *)
   if get_bool "kernel" then (
     let kernel_roots = [
-      get_string "kernel-root";
+      get_string "pre.kernel-root";
       Filename.concat exe_dir "linux-headers";
       (* linux-headers not installed with goblint package *)
     ]
@@ -205,7 +205,7 @@ let preprocess_files () =
     let kernel_dir = kernel_root ^ "/include" in
     let arch_dir = kernel_root ^ "/arch/x86/include" in (* TODO add arm64: https://github.com/goblint/analyzer/issues/312 *)
 
-    get_string_list "kernel_includes" |> List.iter (Filename.concat kernel_root |> one_include_f);
+    get_string_list "pre.kernel_includes" |> List.iter (Filename.concat kernel_root |> one_include_f);
 
     let preconf = find_custom_include "linux/goblint_preconf.h" in
     let autoconf = Filename.concat kernel_dir "linux/kconfig.h" in
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index fa4e1c5b02..ecb73608f1 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -8,33 +8,6 @@
       "type": "string",
       "default": ""
     },
-    "includes": {
-      "title": "includes",
-      "description": "List of directories to include.",
-      "type": "array",
-      "items": { "type": "string" },
-      "default": []
-    },
-    "kernel_includes": {
-      "title": "kernel_includes",
-      "description": "List of kernel directories to include.",
-      "type": "array",
-      "items": { "type": "string" },
-      "default": []
-    },
-    "custom_includes": {
-      "title": "custom_includes",
-      "description": "List of custom directories to include.",
-      "type": "array",
-      "items": { "type": "string" },
-      "default": []
-    },
-    "kernel-root": {
-      "title": "kernel-root",
-      "description": "Root directory for Linux kernel (linux-headers)",
-      "type": "string",
-      "default": ""
-    },
     "justcil": {
       "title": "justcil",
       "description": "Just parse and output the CIL.",
@@ -88,13 +61,6 @@
       "type": "boolean",
       "default": false
     },
-    "cppflags": {
-      "title": "cppflags",
-      "description": "Pre-processing parameters.",
-      "type": "array",
-      "items": { "type": "string" },
-      "default": []
-    },
     "kernel": {
       "title": "kernel",
       "description": "For analyzing Linux Device Drivers.",
@@ -233,6 +199,40 @@
           "description": "Use existing preprocessed files.",
           "type": "boolean",
           "default": false
+        },
+        "includes": {
+          "title": "pre.includes",
+          "description": "List of directories to include.",
+          "type": "array",
+          "items": { "type": "string" },
+          "default": []
+        },
+        "kernel_includes": {
+          "title": "pre.kernel_includes",
+          "description": "List of kernel directories to include.",
+          "type": "array",
+          "items": { "type": "string" },
+          "default": []
+        },
+        "custom_includes": {
+          "title": "pre.custom_includes",
+          "description": "List of custom directories to include.",
+          "type": "array",
+          "items": { "type": "string" },
+          "default": []
+        },
+        "kernel-root": {
+          "title": "pre.kernel-root",
+          "description": "Root directory for Linux kernel (linux-headers)",
+          "type": "string",
+          "default": ""
+        },
+        "cppflags": {
+          "title": "pre.cppflags",
+          "description": "Pre-processing parameters.",
+          "type": "array",
+          "items": { "type": "string" },
+          "default": []
         }
       },
       "additionalProperties": false
diff --git a/tests/regression/41-stdlib/03-noqsort.c b/tests/regression/41-stdlib/03-noqsort.c
index 1953fb182e..e7a1de89a3 100644
--- a/tests/regression/41-stdlib/03-noqsort.c
+++ b/tests/regression/41-stdlib/03-noqsort.c
@@ -1,4 +1,4 @@
-// PARAM: --set cppflags[+] -DGOBLINT_NO_QSORT
+// PARAM: --set pre.cppflags[+] -DGOBLINT_NO_QSORT
 #include<stddef.h>
 
 // There should be no CIL warning about multiple definitions here