summaryrefslogtreecommitdiff
path: root/src/CfimAst.ml
diff options
context:
space:
mode:
authorSon Ho2021-11-17 14:26:43 +0100
committerSon Ho2021-11-17 14:26:43 +0100
commit7c62043ab195ee9844d29ade76efdf839a2e98d0 (patch)
treeaa0aa45d5d11da055604fe7ec503a907bc47af82 /src/CfimAst.ml
parent25fe1a81758bcf25171beee849467b2fff673b20 (diff)
Use [@@ëerive of_json] on all the types
Diffstat (limited to 'src/CfimAst.ml')
-rw-r--r--src/CfimAst.ml10
1 files changed, 9 insertions, 1 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 1fd8ccd4..66e3fb0c 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -4,10 +4,12 @@ open Values
open Expressions
type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree
+[@@deriving of_yojson]
type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id
+[@@deriving of_yojson]
-type assertion = { cond : operand; expected : bool }
+type assertion = { cond : operand; expected : bool } [@@deriving of_yojson]
type fun_sig = {
region_params : region_var RegionVarId.vector;
@@ -16,6 +18,7 @@ type fun_sig = {
inputs : rty VarId.vector;
output : rty;
}
+[@@deriving of_yojson]
type call = {
func : fun_id;
@@ -24,6 +27,7 @@ type call = {
args : operand list;
dest : place;
}
+[@@deriving of_yojson]
type statement =
| Assign of place * rvalue
@@ -44,12 +48,14 @@ type statement =
(** Continue to (outer) loop. The loop identifier works
the same way as for [Break] *)
| Nop
+[@@deriving of_yojson]
type expression =
| Statement of statement
| Sequence of expression * expression
| Switch of operand * switch_targets
| Loop of expression
+[@@deriving of_yojson]
and switch_targets =
| If of expression * expression (** Gives the "if" and "else" blocks *)
@@ -59,6 +65,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 of_yojson]
type fun_def = {
def_id : FunDefId.id;
@@ -69,3 +76,4 @@ type fun_def = {
locals : var VarId.vector;
body : expression;
}
+[@@deriving of_yojson]