From 82520f64c2102ea94116f474f55d9742a96cb312 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 12 Jun 2024 16:34:31 +0200
Subject: [PATCH] [region] useless named lv-region
---
src/plugins/region/annot.ml | 16 ++++++----------
src/plugins/region/annot.mli | 1 -
src/plugins/region/logic.ml | 3 +--
3 files changed, 7 insertions(+), 13 deletions(-)
diff --git a/src/plugins/region/annot.ml b/src/plugins/region/annot.ml
index 746ebcffad8..519b79dd914 100644
--- a/src/plugins/region/annot.ml
+++ b/src/plugins/region/annot.ml
@@ -36,7 +36,6 @@ type path = {
and step =
| Var of varinfo
- | Region of string
| AddrOf of path
| Star of path
| Index of path
@@ -54,12 +53,11 @@ type region = {
(* -------------------------------------------------------------------------- *)
let atomic = function
- | Var _ | Region _ | AddrOf _ | Star _ | Index _ | Field _ -> true
+ | Var _ | AddrOf _ | Star _ | Index _ | Field _ -> true
| Shift _ | Cast _ -> false
let rec pp_step fmt = function
| Var x -> Varinfo.pretty fmt x
- | Region a -> Format.pp_print_string fmt a
| Field(p,f) -> pfield p f fmt
| Index a -> Format.fprintf fmt "%a[..]" pp_atom a
| Shift a -> Format.fprintf fmt "%a+(..)" pp_atom a
@@ -120,12 +118,10 @@ let getCompoundType env ~loc typ =
| TComp(comp,_) -> comp
| _ -> error env ~loc "Expected compound type for term"
-let parse_name (env:env) ~loc x =
- try
- match env.context.find_var x with
- | { lv_origin = Some v } -> { loc ; typ = v.vtype ; step = Var v }
- | _ -> error env ~loc "Variable '%s' is not a C-variable" x
- with Not_found -> { loc ; typ = TVoid [] ; step = Region x }
+let parse_variable (env:env) ~loc x =
+ match env.context.find_var x with
+ | { lv_origin = Some v } -> { loc ; typ = v.vtype ; step = Var v }
+ | _ -> error env ~loc "Variable '%s' is not a C-variable" x
let parse_field env ~loc comp f =
try List.find (fun fd -> fd.fname = f) (Option.value ~default:[] comp.cfields)
@@ -149,7 +145,7 @@ let parse_typ env ~loc t =
let rec parse_lpath (env:env) (e: lexpr) =
let loc = e.lexpr_loc in
match e.lexpr_node with
- | PLvar x -> parse_name env ~loc x
+ | PLvar x -> parse_variable env ~loc x
| PLunop( Ustar , p ) ->
let lv = parse_lpath env p in
if Cil.isPointerType lv.typ then
diff --git a/src/plugins/region/annot.mli b/src/plugins/region/annot.mli
index d820c8a741d..a2fd8bc531f 100644
--- a/src/plugins/region/annot.mli
+++ b/src/plugins/region/annot.mli
@@ -30,7 +30,6 @@ type path = {
and step =
| Var of varinfo
- | Region of string
| AddrOf of path
| Star of path
| Index of path
diff --git a/src/plugins/region/logic.ml b/src/plugins/region/logic.ml
index e46702c622e..6e68710a475 100644
--- a/src/plugins/region/logic.ml
+++ b/src/plugins/region/logic.ml
@@ -26,7 +26,6 @@ open Memory
let rec add_lval (m:map) (p:path): node =
match p.step with
| Var x -> add_root m x
- | Region a -> add_label m a
| Field(lv,fd) -> Memory.add_field m (add_lval m lv) fd
| Index lv -> Memory.add_index m (add_lval m lv) lv.typ
| Star e | Cast(_,e) -> add_pointer m e
@@ -41,7 +40,7 @@ and add_pointer (m:map) (p:path): Memory.node =
and add_exp (m:map) (p:path): Memory.node option =
match p.step with
- | (Var _ | Field _ | Index _ | Star _ | Cast _ | Region _) ->
+ | (Var _ | Field _ | Index _ | Star _ | Cast _) ->
let r = add_lval m p in
add_value m r p.typ
| AddrOf p -> Some (add_lval m p)
--
GitLab