Skip to content

Commit 2c257b6

Browse files
committed
Fix privatization unsoundness without threadflag
Happened in sv-benchmarks/c/systemc/pipeline.cil-1.
1 parent 74b0e86 commit 2c257b6

File tree

3 files changed

+5
-3
lines changed

3 files changed

+5
-3
lines changed

src/analyses/apron/apronAnalysis.apron.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -684,7 +684,8 @@ let get_spec (): (module MCPSpec) =
684684

685685
let after_config () =
686686
let module Spec = (val get_spec ()) in
687-
MCP.register_analysis (module Spec : MCPSpec);
687+
(* Need threadflag to emit EnterMultithreaded to have sound MUTEX_INITS. *)
688+
MCP.register_analysis ~dep:["threadflag"] (module Spec : MCPSpec);
688689
GobConfig.set_string "ana.path_sens[+]" (Spec.name ())
689690

690691
let _ =

src/analyses/base.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2844,7 +2844,8 @@ let get_main (): (module MainSpec) =
28442844
let after_config () =
28452845
let module Main = (val get_main ()) in
28462846
(* add ~dep:["expRelation"] after modifying test cases accordingly *)
2847-
MCP.register_analysis ~dep:["mallocWrapper"] (module Main : MCPSpec)
2847+
(* Need threadflag to emit EnterMultithreaded to have sound MUTEX_INITS. *)
2848+
MCP.register_analysis ~dep:["mallocWrapper"; "threadflag"] (module Main : MCPSpec)
28482849

28492850
let _ =
28502851
AfterConfig.register after_config

src/autoTune.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -135,7 +135,7 @@ let disableIntervalContextsInRecursiveFunctions () =
135135
(*escape is also still enabled, because otherwise we get a warning*)
136136
(*does not consider dynamic calls!*)
137137

138-
let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadflag"; "threadid"; "threadJoins"; "threadreturn"]
138+
let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"]
139139
let reduceThreadAnalyses () =
140140
let hasThreadCreate () =
141141
ResettableLazy.force functionCallMaps

0 commit comments

Comments
 (0)