Skip to content

Commit

Permalink
Recognize mem-safety props in any order
Browse files Browse the repository at this point in the history
  • Loading branch information
mrstanb committed Oct 2, 2023
1 parent da45e40 commit 1335123
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/witness/svcompSpec.ml
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,8 @@ let of_string s =
let global1 = Str.matched_group 1 s in
let global2 = Str.matched_group 2 s in
let global3 = Str.matched_group 3 s in
if global1 = "valid-free" && global2 = "valid-deref" && global3 = "valid-memtrack" then
let mem_safety_props = ["valid-free"; "valid-deref"; "valid-memtrack";] in
if (global1 <> global2 && global1 <> global3 && global2 <> global3) && List.for_all (fun x -> List.mem x mem_safety_props) [global1; global2; global3] then
MemorySafety
(* if global = "valid-free" then
ValidFree
Expand Down

0 comments on commit 1335123

Please sign in to comment.