Skip to content

Commit

Permalink
Use BoolDomain instead of SetDomain
Browse files Browse the repository at this point in the history
  • Loading branch information
karoliineh committed Sep 16, 2023
1 parent daa61b4 commit b64b65f
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 7 deletions.
2 changes: 1 addition & 1 deletion src/analyses/region.ml
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ struct
match st with
| `Lifted reg ->
begin match Reg.eval_exp exp with
| Some (_,v,_) -> (try not (RegionDomain.RS.is_empty (RegMap.find v reg)) with Not_found -> false)
| Some (_,v,_) -> RegMap.find v reg
| _ -> false
end
| `Top -> false
Expand Down
11 changes: 5 additions & 6 deletions src/cdomains/regionDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,7 @@ open GoblintCil
open GobConfig
open MusteqDomain

module B = Lattice.UnitConf (struct let name = "" end)
module RS = SetDomain.Make (B)
module RS = BoolDomain.MayBool

module RegMap =
struct
Expand Down Expand Up @@ -51,8 +50,8 @@ struct
(* This is the main logic for dealing with the bullet and finding it an
* owner... *)
let add_set (s:set) llist (m:RegMap.t): t =
if not (RS.is_empty s)
then RegMap.add_list_set llist (RS.singleton ()) m
if s
then RegMap.add_list_set llist true m
else m

let assign (lval: lval) (rval: exp) reg: t =
Expand All @@ -74,7 +73,7 @@ struct
| false, true , false ->
add_set (RS.join (RegMap.find x reg) (RegMap.find y reg)) [x;y] reg
| true , _ , true ->
add_set (RS.empty ()) [] reg
add_set false [] reg
| true , _ , false ->
add_set (RegMap.find y reg) [y] reg
end
Expand All @@ -90,7 +89,7 @@ struct

let assign_bullet lval m: t =
match eval_exp (Lval lval) with
| Some (_,x,_) -> RegMap.add x (RS.singleton ()) m
| Some (_,x,_) -> RegMap.add x true m
| _ -> m

let related_globals (deref_vfd: eval_t) : elt list =
Expand Down

0 comments on commit b64b65f

Please sign in to comment.