summaryrefslogtreecommitdiff
path: root/src/initial_check.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-05-14 15:46:10 +0100
committerAlasdair Armstrong2019-05-14 15:46:10 +0100
commit9d6734f717639f9babdec4441f8362bfeca10d66 (patch)
tree91080afb376c38328de7262352f7c3217bc22719 /src/initial_check.ml
parent63d7f669f3d292315e4a353115284358ba7d5627 (diff)
parentf6cc45f2788dc777d1fa35aa9a216de994992288 (diff)
Merge branch 'smt_experiments' into sail2
Diffstat (limited to 'src/initial_check.ml')
-rw-r--r--src/initial_check.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index ad52751b..522faab7 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -425,7 +425,8 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
E_internal_return(to_ast_exp ctx exp)
else
raise (Reporting.err_general l "Internal return construct found without -dmagic_hash")
- | _ -> raise (Reporting.err_unreachable l __POS__ "Unparsable construct in to_ast_exp")
+ | P.E_deref exp ->
+ E_app (Id_aux (Id "__deref", l), [to_ast_exp ctx exp])
), (l,()))
and to_ast_measure ctx (P.Measure_aux(m,l)) : unit internal_loop_measure =