summaryrefslogtreecommitdiff
path: root/src/rewrites.mli
diff options
context:
space:
mode:
authorAlasdair2019-04-27 00:20:37 +0100
committerAlasdair2019-04-27 00:40:56 +0100
commit0c99f19b012205f1be1d4ae18b722ecbdd80e3d4 (patch)
tree55f796f9bdf270064bfe87bdf275b93ffcdc1fb2 /src/rewrites.mli
parentbf240119e43cb4e3b5f5746b5ef21f19a8fac2d2 (diff)
parent094c8e254abde44d45097aca7a36203704fe2ef4 (diff)
Merge branch 'sail2' into smt_experiments
Diffstat (limited to 'src/rewrites.mli')
-rw-r--r--src/rewrites.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/rewrites.mli b/src/rewrites.mli
index 330f10b4..e30a4206 100644
--- a/src/rewrites.mli
+++ b/src/rewrites.mli
@@ -63,6 +63,9 @@ val opt_dmono_continue : bool ref
(* Generate a fresh id with the given prefix *)
val fresh_id : string -> l -> id
+(* Move loop termination measures into loop AST nodes *)
+val move_loop_measures : 'a defs -> 'a defs
+
(* Re-write undefined to functions created by -undefined_gen flag *)
val rewrite_undefined : bool -> Env.t -> tannot defs -> tannot defs