Merge pull request #1280 from goblint/fix_setjmpname

Fix name of `modifiedSinceSetjmp`
goblint · Dec 4, 2023 · 456b287 · 456b287
2 parents db49fe9 + 11516b1
commit 456b287
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 7 deletions.
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
@@ -29,7 +29,7 @@ struct
   let init _ =
     collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
     let activated = get_string_list "ana.activated" in
-    emit_single_threaded := List.mem (ModifiedSinceLongjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
+    emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
 
   let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (kind:AccessKind.t) (reach:bool) (e:exp) =
     if M.tracing then M.trace "access" "do_access %a %a %B\n" d_exp e AccessKind.pretty kind reach;

diff --git a/src/analyses/modifiedSinceLongjmp.ml → src/analyses/modifiedSinceSetjmp.ml b/src/analyses/modifiedSinceLongjmp.ml → src/analyses/modifiedSinceSetjmp.ml
@@ -1,6 +1,4 @@
-(** Analysis of variables modified since [setjmp] ([modifiedSinceLongjmp]). *)
-
-(* TODO: this name is wrong *)
+(** Analysis of variables modified since [setjmp] ([modifiedSinceSetjmp]). *)
 
 open GoblintCil
 open Analyses
@@ -9,7 +7,7 @@ module Spec =
 struct
   include Analyses.IdentitySpec
 
-  let name () = "modifiedSinceLongjmp"
+  let name () = "modifiedSinceSetjmp"
   module D = JmpBufDomain.LocallyModifiedMap
   module VS = D.VarSet
   module C = Lattice.Unit

diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -200,7 +200,7 @@ let reduceThreadAnalyses () =
 
 (* This is run independent of the autotuner being enabled or not to be sound in the presence of setjmp/longjmp  *)
 (* It is done this way around to allow enabling some of these analyses also for programs without longjmp *)
-let longjmpAnalyses = ["activeLongjmp"; "activeSetjmp"; "taintPartialContexts"; "modifiedSinceLongjmp"; "poisonVariables"; "expsplit"; "vla"]
+let longjmpAnalyses = ["activeLongjmp"; "activeSetjmp"; "taintPartialContexts"; "modifiedSinceSetjmp"; "poisonVariables"; "expsplit"; "vla"]
 
 let activateLongjmpAnalysesWhenRequired () =
   let isLongjmp = function

diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
@@ -130,7 +130,7 @@ module ExtractPthread = ExtractPthread
     Analyses related to [longjmp] and [setjmp]. *)
 
 module ActiveSetjmp = ActiveSetjmp
-module ModifiedSinceLongjmp = ModifiedSinceLongjmp
+module ModifiedSinceSetjmp = ModifiedSinceSetjmp
 module ActiveLongjmp = ActiveLongjmp
 module PoisonVariables = PoisonVariables
 module Vla = Vla