diff options
Diffstat (limited to 'src/LlbcAst.ml')
-rw-r--r-- | src/LlbcAst.ml | 36 |
1 files changed, 22 insertions, 14 deletions
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml index d35cd5d8..ccc870dc 100644 --- a/src/LlbcAst.ml +++ b/src/LlbcAst.ml @@ -1,10 +1,10 @@ -open Identifiers open Names open Types open Values open Expressions - +open Identifiers module FunDeclId = IdGen () +module GlobalDeclId = IdGen () type var = { index : VarId.id; (** Unique variable identifier *) @@ -36,6 +36,9 @@ type assumed_fun_id = type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id [@@deriving show, ord] +type global_assignment = { dst : VarId.id; global : GlobalDeclId.id } +[@@deriving show] + type assertion = { cond : operand; expected : bool } [@@deriving show] type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group @@ -77,20 +80,16 @@ class ['self] iter_statement_base = object (_self : 'self) inherit [_] VisitorsRuntime.iter - method visit_place : 'env -> place -> unit = fun _ _ -> () + method visit_global_assignment : 'env -> global_assignment -> unit = + fun _ _ -> () + 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_operand : 'env -> operand -> unit = fun _ _ -> () - method visit_call : 'env -> call -> unit = fun _ _ -> () - method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> () - method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> () end @@ -99,16 +98,15 @@ class ['self] map_statement_base = object (_self : 'self) inherit [_] VisitorsRuntime.map - method visit_place : 'env -> place -> place = fun _ x -> x + method visit_global_assignment + : 'env -> global_assignment -> global_assignment = + fun _ x -> x + 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_operand : 'env -> operand -> operand = fun _ x -> x - method visit_call : 'env -> call -> call = fun _ x -> x method visit_integer_type : 'env -> integer_type -> integer_type = @@ -120,6 +118,7 @@ class ['self] map_statement_base = type statement = | Assign of place * rvalue + | AssignGlobal of global_assignment | FakeRead of place | SetDiscriminant of place * VariantId.id | Drop of place @@ -178,5 +177,14 @@ type fun_decl = { name : fun_name; signature : fun_sig; body : fun_body option; + is_global_decl_body : bool; +} +[@@deriving show] + +type global_decl = { + def_id : GlobalDeclId.id; + body_id : FunDeclId.id; + name : global_name; + ty : ety; } [@@deriving show] |