diff options
| author | Alasdair Armstrong | 2019-06-04 17:36:22 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-06-04 17:36:22 +0100 |
| commit | 37c5fb51e9986917a791de73435e182549e21fca (patch) | |
| tree | f6bd9bd26d80e51cf197b9ea8a5c9d5c3c61ec8b /src | |
| parent | 239e13dc149af80f979ea95a3c9b42220481a0a1 (diff) | |
Make sure aarch64_small can generate Jib for SMT
Add a test case for this
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/anf.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/src/jib/anf.ml b/src/jib/anf.ml index 5165904d..dbbb10e0 100644 --- a/src/jib/anf.ml +++ b/src/jib/anf.ml @@ -670,7 +670,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = let aexp2 = anf exp2 in let aval1, wrap1 = to_aval aexp1 in let aval2, wrap2 = to_aval aexp2 in - wrap1 (wrap2 (mk_aexp (AE_app (mk_id "cons", [aval1; aval2], unit_typ)))) + wrap1 (wrap2 (mk_aexp (AE_app (mk_id "sail_cons", [aval1; aval2], unit_typ)))) | E_id id -> let lvar = Env.lookup_id id (env_of exp) in diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 7e062c5a..2066021e 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -1568,8 +1568,9 @@ let sort_ctype_defs cdefs = let compile_ast ctx (Defs defs) = let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit" in let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in + let cons_vs = Initial_check.extern_of_string (mk_id "sail_cons") "forall ('a : Type). ('a, list('a)) -> list('a)" in - let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in + let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs; cons_vs])) } in if !opt_memo_cache then (try |