Add option witness.invariant.all-locals that can be turned off to only print locals definitely in scope

Author: michael-schwarz

src/cdomain/value/domains/invariantCil.ml

@@ -21,7 +21,11 @@ let exp_replace_original_name e =
 let var_is_in_scope scope vi =
   match Cilfacade.find_scope_fundec vi with
   | None -> vi.vstorage <> Static (* CIL pulls static locals into globals, but they aren't syntactically in global scope *)
-  | Some fd -> CilType.Fundec.equal fd scope
+  | Some fd -> 
+    if CilType.Fundec.equal fd scope then
+      GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)
+    else
+      false
 
 class exp_is_in_scope_visitor (scope: fundec) (acc: bool ref) = object
   inherit nopCilVisitor

src/config/options.schema.json

@@ -2449,6 +2449,12 @@
                 "RETURN"
               ]
             },
+            "all-locals": {
+              "title": "witness.invariant.all-locals",
+              "description": "Emit invariants for local variables under the assumption they are always in scope within their function.",
+              "type": "boolean",
+              "default": true
+            },
             "goblint": {
               "title": "witness.invariant.goblint",
               "description": "Emit non-standard Goblint-specific invariants. Currently array invariants with all_index offsets.",

src/maingoblint.ml

@@ -143,6 +143,7 @@ let check_arguments () =
   if get_bool "incremental.restart.sided.enabled" && get_string_list "incremental.restart.list" <> [] then warn "Passing a non-empty list to incremental.restart.list (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated.";
   if get_bool "ana.autotune.enabled" && get_bool "incremental.load" then (set_bool "ana.autotune.enabled" false; warn "ana.autotune.enabled implicitly disabled by incremental.load");
   if get_bool "exp.basic-blocks" && not (get_bool "justcil") && List.mem "assert" @@ get_string_list "trans.activated" then (set_bool "exp.basic-blocks" false; warn "The option exp.basic-blocks implicitely disabled by activating the \"assert\" tranformation.");
+  if (not @@ get_bool "witness.invariant.all-locals") && (not @@ get_bool "cil.addNestedScopeAttr") then (set_bool "cil.addNestedScopeAttr" true; warn "Disabling witness.invariant.all-locals implicitly enables cil.addNestedScopeAttr.");
   if List.mem "remove_dead_code" @@ get_string_list "trans.activated" then (
     (* 'assert' transform happens before 'remove_dead_code' transform *)
     ignore @@ List.fold_left