Remove dbg.debug option

conf/incremental.json

@@ -28,11 +28,13 @@
     "trace": {
       "context": true
     },
-    "debug": true,
     "timing": {
       "enabled": true
     }
   },
+  "warn": {
+    "debug": true
+  },
   "result": "none",
   "solver": "td3",
   "solvers": {

conf/minimal_incremental.json

@@ -27,11 +27,13 @@
     "trace": {
       "context": true
     },
-    "debug": true,
     "timing": {
       "enabled": true
     }
   },
+  "warn": {
+    "debug": true
+  },
   "result": "none",
   "solver": "td3",
   "solvers": {

docs/developer-guide/firstanalysis.md

@@ -35,7 +35,7 @@ This program is in the Goblint repository: `tests/regression/99-tutorials/01-fir
 But if you run Goblint out of the box on this example, it will not work:
 
 ```console
-./goblint --enable dbg.debug tests/regression/99-tutorials/01-first.c
+./goblint --enable warn.debug tests/regression/99-tutorials/01-first.c
 ```
 
 This will claim that the assertion in unknown.

docs/developer-guide/testing.md

@@ -24,7 +24,7 @@ gobopt='--set ana.base.privatization write+lock' ./scripts/update_suite.rb
 ```
 
 ### Writing
-* Add parameters to a regression test in the first line: `// PARAM: --set dbg.debug true`
+* Add parameters to a regression test in the first line: `// PARAM: --set warn.debug true`
 * Annotate lines inside the regression test with comments: `arr[9] = 10; // WARN`
 
 ## Cram Tests

regtest.sh

@@ -14,7 +14,7 @@ if [[ $OSTYPE == 'darwin'* ]]; then
   grep="ggrep"
 fi
 params="`$grep -oP "PARAM: \K.*" $file`"
-cmd="./goblint --enable dbg.debug --enable dbg.regression --html $params ${@:3} $file" # -v
+cmd="./goblint --enable warn.debug --enable dbg.regression --html $params ${@:3} $file" # -v
 echo "$cmd"
 eval $cmd
 echo "See result/index.xml"

scripts/creduce/privPrecCompare.sh

@@ -22,7 +22,7 @@ for PRIV in "${PRIVS[@]}"; do
     PRIVDUMP="$OUTDIR/$PRIV"
     LOG="$OUTDIR/$PRIV.log"
     rm -f $PRIVDUMP
-    $GOBLINTDIR/goblint --sets exp.privatization $PRIV --sets exp.priv-prec-dump $PRIVDUMP $OPTS -v --enable dbg.debug &> $LOG
+    $GOBLINTDIR/goblint --sets exp.privatization $PRIV --sets exp.priv-prec-dump $PRIVDUMP $OPTS -v --enable warn.debug &> $LOG
     grep -F "Function definition missing" $LOG && exit 1
 done
 

scripts/spec/check.sh

@@ -12,7 +12,7 @@ else
     ana="spec"
     opt="--set ana.spec.file $spec"
 fi
-cmd="./goblint --set ana.activated[0][+] $ana $opt --html --set dbg.debug $debug $file"
+cmd="./goblint --set ana.activated[0][+] $ana $opt --html --set warn.debug $debug $file"
 echo -e "$(tput setaf 6)$cmd$(tput sgr 0)"
 $cmd
 

scripts/test-incremental-multiple.sh

@@ -7,7 +7,7 @@ conf=$base/$test.json
 patch1=$base/${test}_1.patch
 patch2=$base/${test}_2.patch
 
-args="--enable dbg.debug --enable dbg.timing.enabled -v"
+args="--enable warn.debug --enable dbg.timing.enabled -v"
 
 cat $source
 

scripts/test-incremental.sh

@@ -11,7 +11,7 @@ source=$base/$test.c
 conf=$base/$test.json
 patch=$base/$test.patch
 
-args="--enable dbg.debug --enable dbg.timing.enabled -v --enable allglobs"
+args="--enable warn.debug --enable dbg.timing.enabled -v --enable allglobs"
 
 ./goblint --conf $conf $args --enable incremental.save $source &> $base/$test.before.log
 

scripts/update_suite.rb

@@ -496,8 +496,8 @@ def create_test_set(lines)
   end
   def run ()
     filename = File.basename(@path)
-    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile}0 --enable dbg.debug --set dbg.timing.enabled true --enable witness.yaml.enabled --set goblint-dir .goblint-#{@id.sub('/','-')}-witness1 2>#{@testset.statsfile}0"
-    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set ana.activated[+] unassume --enable dbg.debug --set dbg.timing.enabled true --set witness.yaml.unassume witness.yml --set goblint-dir .goblint-#{@id.sub('/','-')}-witness2 2>#{@testset.statsfile}"
+    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile}0 --enable warn.debug --set dbg.timing.enabled true --enable witness.yaml.enabled --set goblint-dir .goblint-#{@id.sub('/','-')}-witness1 2>#{@testset.statsfile}0"
+    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set ana.activated[+] unassume --enable warn.debug --set dbg.timing.enabled true --set witness.yaml.unassume witness.yml --set goblint-dir .goblint-#{@id.sub('/','-')}-witness2 2>#{@testset.statsfile}"
     starttime = Time.now
     run_testset(@testset, cmd1, starttime)
     starttime = Time.now
@@ -544,7 +544,7 @@ def run ()
       if $1 then params = $1 else params = "" end
     end
     # always enable debugging so that the warnings would work
-    params << " --set dbg.debug true"
+    params << " --set warn.debug true"
     p = if incremental then
           patch = f[0..-3] + ".patch"
           patch_path = File.expand_path(patch, grouppath)

src/analyses/spec.ml

@@ -444,7 +444,6 @@ struct
     | _ -> ctx.local
 
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    (* let _ = GobConfig.set_bool "dbg.debug" false in *)
     let arglist = List.map (Cil.stripCasts) arglist in (* remove casts, TODO safe? *)
     let get_key c = match SC.get_key_variant c with
       | `Lval s ->

src/domains/access.ml

@@ -462,17 +462,11 @@ let incr_summary safe vulnerable unsafe (lv, ty) grouped_accs =
 
 let print_accesses (lv, ty) grouped_accs =
   let allglobs = get_bool "allglobs" in
-  let debug = get_bool "dbg.debug" in
   let race_threshold = get_int "warn.race-threshold" in
   let msgs race_accs =
     let h (conf,kind,node,e,a) =
       let d_msg () = dprintf "%a with %a (conf. %d)" AccessKind.pretty kind MCPAccess.A.pretty a conf in
-      let doc =
-        if debug then
-          dprintf "%t  (exp: %a)" d_msg d_exp e
-        else
-          d_msg ()
-      in
+      let doc = dprintf "%t  (exp: %a)" d_msg d_exp e in
       (doc, Some (Messages.Location.Node node))
     in
     AS.elements race_accs

src/framework/control.ml

@@ -590,7 +590,7 @@ struct
 
       (* check for dead code at the last state: *)
       let main_sol = try LHT.find lh (List.hd startvars') with Not_found -> Spec.D.bot () in
-      if get_bool "dbg.debug" && Spec.D.is_bot main_sol then
+      if Spec.D.is_bot main_sol then
         M.warn_noloc ~category:Deadcode "Function 'main' does not return";
 
       if get_bool "dump_globs" then

src/maingoblint.ml

@@ -170,9 +170,6 @@ let handle_flags () =
     Errormsg.verboseFlag := true
   );
 
-  if get_bool "dbg.debug" then
-    set_bool "warn.debug" true;
-
   if get_bool "ana.sv-comp.functions" then
     set_auto "lib.activated[+]" "sv-comp";
 

src/solvers/postSolver.ml

@@ -61,7 +61,7 @@ module Prune: F =
     include Unit (S) (VH)
 
     let finalize ~vh ~reachable =
-      if get_bool "dbg.debug" then
+      if get_bool "dbg.verbose" then
         print_endline "Pruning result";
 
       VH.filteri_inplace (fun x _ ->

src/util/options.schema.json

@@ -1737,12 +1737,6 @@
       "description": "Debugging options",
       "type": "object",
       "properties": {
-        "debug": {
-          "title": "dbg.debug",
-          "description": "Debug mode: for testing the analyzer itself.",
-          "type": "boolean",
-          "default": false
-        },
         "verbose": {
           "title": "dbg.verbose",
           "description": "Prints some status information.",

tests/incremental/00-basic/09-unreach.json

@@ -1,5 +1,5 @@
 {
-    "dbg": {
+    "warn": {
         "debug": true
     },
     "incremental" : {

tests/incremental/00-basic/10-reach.json

@@ -1,5 +1,5 @@
 {
-    "dbg": {
+    "warn": {
         "debug": true
     },
     "incremental" : {

tests/incremental/00-basic/11-unreach-reusesuper.json

@@ -1,5 +1,5 @@
 {
-    "dbg": {
+    "warn": {
         "debug": true
     },
     "incremental" : {