summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CfimAst.ml51
-rw-r--r--src/Values.ml8
2 files changed, 54 insertions, 5 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 23c8f1aa..a4a128c3 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -82,6 +82,38 @@ type call = {
}
[@@deriving show]
+(** Ancestor for [typed_value] iter visitor *)
+class ['self] iter_statement_base =
+ object (_self : 'self)
+ inherit [_] VisitorsRuntime.iter
+
+ method visit_place : 'env -> place -> unit = fun _ _ -> ()
+
+ method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> ()
+
+ method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> ()
+
+ method visit_assertion : 'env -> assertion -> unit = fun _ _ -> ()
+
+ method visit_call : 'env -> call -> unit = fun _ _ -> ()
+ end
+
+(** Ancestor for [typed_value] map visitor *)
+class ['self] map_statement_base =
+ object (_self : 'self)
+ inherit [_] VisitorsRuntime.iter
+
+ method visit_place : 'env -> place -> place = fun _ x -> x
+
+ method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x
+
+ method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x
+
+ method visit_assertion : 'env -> assertion -> assertion = fun _ x -> x
+
+ method visit_call : 'env -> call -> call = fun _ x -> x
+ end
+
type statement =
| Assign of place * rvalue
| FakeRead of place
@@ -114,7 +146,24 @@ and switch_targets =
- the "otherwise" statement.
Also note that we precise the type of the integer (uint32, int64, etc.)
which we switch on. *)
-[@@deriving show]
+[@@deriving
+ show,
+ visitors
+ {
+ name = "iter_statement";
+ variety = "iter";
+ ancestors = [ "iter_statement_base" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ concrete = true;
+ },
+ visitors
+ {
+ name = "map_statement";
+ variety = "map";
+ ancestors = [ "map_statement_base" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ concrete = true;
+ }]
type fun_def = {
def_id : FunDefId.id;
diff --git a/src/Values.ml b/src/Values.ml
index ae9eb127..ac4145eb 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -77,7 +77,7 @@ type symbolic_proj_comp = {
regions *but* the ones which are listed in the projector.
*)
-(** Ancestor for iter visitor for [typed_value] *)
+(** Ancestor for [typed_value] iter visitor *)
class ['self] iter_typed_value_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.iter
@@ -92,7 +92,7 @@ class ['self] iter_typed_value_base =
method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
end
-(** Ancestor for map visitor for [typed_value] *)
+(** Ancestor for [typed_value] map visitor for *)
class ['self] map_typed_value_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.map
@@ -215,7 +215,7 @@ type aproj =
type region = RegionVarId.id Types.region [@@deriving show]
-(** Ancestor for iter visitor for [typed_avalue] *)
+(** Ancestor for [typed_avalue] iter visitor *)
class ['self] iter_typed_avalue_base =
object (_self : 'self)
inherit [_] iter_typed_value
@@ -231,7 +231,7 @@ class ['self] iter_typed_avalue_base =
fun _ _ -> ()
end
-(** Ancestor for MAP visitor for [typed_avalue] *)
+(** Ancestor for [typed_avalue] map visitor *)
class ['self] map_typed_avalue_base =
object (_self : 'self)
inherit [_] map_typed_value