[region] region_of_ptr_term v.0.1 (incorrect)

src/plugins/region/Region.ml

@@ -50,6 +50,40 @@ let field (map:map) (region:region) (field:fieldinfo) : region =
 
 let index (_:map) (_:region) (_:typ) : region = (* TODO *) raise Not_found
 
+let region_of_ptr_term (map:map) (ptr:term) : region =
+  match ptr.term_node with
+  (* same constructs as exp *)
+  | TConst _ | TLval _| TSizeOf _| TSizeOfE _ | TSizeOfStr _ | TAlignOf _
+  | TAlignOfE _ | TUnOp _ | TBinOp _ | TCast _ ->
+    begin match Memory.exp map.map @@ Logic_to_c.term_to_exp ptr with
+      | None -> raise Not_found
+      | Some node -> Memory.region map.map node
+    end
+  | TAddrOf term_lval ->
+    Memory.region map.map @@ Memory.lval map.map @@ Logic_to_c.term_lval_to_lval term_lval
+  | TStartOf term_lval ->
+    Memory.region map.map @@ Memory.lval map.map @@ Logic_to_c.term_lval_to_lval term_lval
+  (* additional constructs *)
+  | Tapp _            -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Tapp")
+  | Tlambda _         -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Tlambda")
+  | TDataCons _       -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: TDataCons")
+  | Tif _             -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Tif")
+  | Tat _             -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Tat")
+  (* logic_label * term  *)
+  | Tbase_addr _      -> (* TODO *) raise Not_found
+  | Toffset _         -> (* TODO *) raise Not_found
+  | Tblock_length _   -> (* TODO *) raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Tblock_length")
+  | Tnull             -> (* TODO *) raise Not_found
+  | TUpdate _         -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: TUpdate")
+  | Ttypeof _         -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Ttypeof")
+  | Ttype _           -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Ttype")
+  | Tempty_set        -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Tempty_set")
+  | Tunion _          -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Tunion")
+  | Tinter _          -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Tinter")
+  | Tcomprehension _  -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Tcomprehension")
+  | Trange _          -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Trange")
+  | Tlet _            -> raise (Invalid_argument "Region:Region.ml:region_of_ptr_term: Tlet")
+
 
 let points_to (map:map) (region:region) : region option =
   Option.map (Memory.region map.map) @@ Memory.cpointed map.map region.Memory.node

src/plugins/region/Region.mli

@@ -38,6 +38,8 @@ val cvar : map -> varinfo -> region
 val field : map -> region -> fieldinfo -> region
 val index : map -> region -> typ -> region
 
+val region_of_ptr_term : map -> term -> region
+
 (* API POINTERS *)
 val points_to : map -> region -> region option
 val pointed_by : map -> region -> region list