summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-01-24 17:44:22 +0000
committerAlasdair Armstrong2018-01-24 19:53:05 +0000
commit10e2be330c14aaddbd8ada6b6ce8a8a63c7d605e (patch)
treeac904feb95f86f0758b74804e632b4785b601acc /src/rewrites.ml
parentcd81acaf58db3edc4187e4cccc35f6aa76d6933d (diff)
Have some simple sail programs compiling to C
Diffstat (limited to 'src/rewrites.ml')
-rw-r--r--src/rewrites.ml13
1 files changed, 13 insertions, 0 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 4378c720..454fefd3 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3004,6 +3004,19 @@ let rewrite_defs_ocaml = [
(* ("separate_numbs", rewrite_defs_separate_numbs) *)
]
+let rewrite_defs_c = [
+ ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
+ ("pat_lits", rewrite_defs_pat_lits);
+ ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
+ ("tuple_assignments", rewrite_tuple_assignments);
+ ("simple_assignments", rewrite_simple_assignments);
+ ("remove_vector_concat", rewrite_defs_remove_vector_concat);
+ ("exp_lift_assign", rewrite_defs_exp_lift_assign);
+ ("constraint", rewrite_constraint);
+ ("trivial_sizeof", rewrite_trivial_sizeof);
+ ("sizeof", rewrite_sizeof);
+ ]
+
let rewrite_defs_interpreter = [
("no_effect_check", (fun defs -> opt_no_effects := true; defs));
("tuple_vector_assignments", rewrite_tuple_vector_assignments);