diff options
author | Son Ho | 2022-01-06 10:07:15 +0100 |
---|---|---|
committer | Son Ho | 2022-01-06 10:07:15 +0100 |
commit | 6f25cbb0dd202b53fe850560ddf566c75183af7d (patch) | |
tree | 3df3c63b33d6a794db066bf75d52b121f63afc4d | |
parent | 067be88c6c3fc61a55eeeaf8ccf59a9ce423e68d (diff) |
Generate iterators for statement
-rw-r--r-- | src/CfimAst.ml | 51 | ||||
-rw-r--r-- | src/Values.ml | 8 |
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 |