diff options
Diffstat (limited to '')
| -rw-r--r-- | src/CfimAst.ml | 10 | ||||
| -rw-r--r-- | src/Contexts.ml | 7 | ||||
| -rw-r--r-- | src/Expressions.ml | 4 |
3 files changed, 18 insertions, 3 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 85d4c56e..7be1a4bc 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -6,10 +6,12 @@ open Expressions module FunDefId = IdGen () type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree +[@@deriving show] type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id +[@@deriving show] -type assertion = { cond : operand; expected : bool } +type assertion = { cond : operand; expected : bool } [@@deriving show] type fun_sig = { region_params : region_var RegionVarId.vector; @@ -18,6 +20,7 @@ type fun_sig = { inputs : rty VarId.vector; output : rty; } +[@@deriving show] type call = { func : fun_id; @@ -26,6 +29,7 @@ type call = { args : operand list; dest : place; } +[@@deriving show] type statement = | Assign of place * rvalue @@ -46,12 +50,14 @@ type statement = (** Continue to (outer) loop. The loop identifier works the same way as for [Break] *) | Nop +[@@deriving show] type expression = | Statement of statement | Sequence of expression * expression | Switch of operand * switch_targets | Loop of expression +[@@deriving show] and switch_targets = | If of expression * expression (** Gives the "if" and "else" blocks *) @@ -61,6 +67,7 @@ and switch_targets = - the "otherwise" expression. Also note that we precise the type of the integer (uint32, int64, etc.) which we switch on. *) +[@@deriving show] type fun_def = { def_id : FunDefId.id; @@ -71,3 +78,4 @@ type fun_def = { locals : var VarId.vector; body : expression; } +[@@deriving show] diff --git a/src/Contexts.ml b/src/Contexts.ml index b18cfe22..f182add5 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -8,12 +8,14 @@ open CfimAst TODO: rename? Environment element or something? *) type env_value = Var of var * typed_value | Abs of abs | Frame +[@@deriving show] -type env = env_value list +type env = env_value list [@@deriving show] -type interpreter_mode = ConcreteMode | SymbolicMode +type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show] type config = { mode : interpreter_mode; check_invariants : bool } +[@@deriving show] type eval_ctx = { type_context : type_def TypeDefId.vector; @@ -23,6 +25,7 @@ type eval_ctx = { symbolic_counter : SymbolicValueId.generator; borrow_counter : BorrowId.generator; } +[@@deriving show] (** Evaluation context *) let fresh_symbolic_value_id (ctx : eval_ctx) : eval_ctx * SymbolicValueId.id = diff --git a/src/Expressions.ml b/src/Expressions.ml index 20431f18..38ee1ff6 100644 --- a/src/Expressions.ml +++ b/src/Expressions.ml @@ -66,16 +66,19 @@ type operand_constant_value = | ConstantValue of constant_value | ConstantAdt of TypeDefId.id | Unit +[@@deriving show] type operand = | Copy of place | Move of place | Constant of ety * operand_constant_value +[@@deriving show] type aggregate_kind = | AggregatedTuple | AggregatedAdt of TypeDefId.id * VariantId.id option * erased_region list * ety list +[@@deriving show] type rvalue = | Use of operand @@ -84,3 +87,4 @@ type rvalue = | BinaryOp of binop * operand * operand | Discriminant of place | Aggregate of aggregate_kind * operand list +[@@deriving show] |