For #1977, we would have liked for threadJoins to not have its own bottom element, as all threads being must-joined is equivalent to unreachability, which should be represented by the bottom element of the DeadcodeLifter.
However, MCP explicitly creates S.D.bot () abstract elements when an analysis does raise Deadcode, which means any analysis that raises deadcode has to have it's own bottom element.
|
let map_deadcode f xs = |
|
let dead = ref false in |
|
let one_el xs (n,(module S:MCPSpec),d) = try f xs (n,(module S:MCPSpec),d) :: xs with Deadcode -> dead:=true; (n,Obj.repr @@ S.D.bot ()) :: xs in |
|
let ys = fold_left one_el [] xs in |
|
List.rev ys, !dead |
Getting rid of this would allow us to do some more simplications to the domain of the locals in threadJoins and potentially elsewhere.
For #1977, we would have liked for
threadJoinsto not have its own bottom element, as all threads being must-joined is equivalent to unreachability, which should be represented by the bottom element of the DeadcodeLifter.However, MCP explicitly creates
S.D.bot ()abstract elements when an analysis doesraise Deadcode, which means any analysis that raises deadcode has to have it's own bottom element.analyzer/src/analyses/mCP.ml
Lines 110 to 114 in 582608c
Getting rid of this would allow us to do some more simplications to the domain of the locals in
threadJoinsand potentially elsewhere.