From 11516b13fc1070ac0463a51ccf79c46e8cf5ea8f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 1 Dec 2023 20:23:31 +0100 Subject: [PATCH] Fix name of modifiedSinceSetjmp --- src/analyses/accessAnalysis.ml | 2 +- .../{modifiedSinceLongjmp.ml => modifiedSinceSetjmp.ml} | 6 ++---- src/autoTune.ml | 2 +- src/goblint_lib.ml | 2 +- 4 files changed, 5 insertions(+), 7 deletions(-) rename src/analyses/{modifiedSinceLongjmp.ml => modifiedSinceSetjmp.ml} (96%) diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index b181a1c70e..efad8b4c2e 100644 --- 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 b/src/analyses/modifiedSinceSetjmp.ml similarity index 96% rename from src/analyses/modifiedSinceLongjmp.ml rename to src/analyses/modifiedSinceSetjmp.ml index a129c9f92c..93e55b2a17 100644 --- a/src/analyses/modifiedSinceLongjmp.ml +++ b/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 index 0c3d3727f0..3cda36a302 100644 --- 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 index 70f331b5ac..66ab2c76a4 100644 --- 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