summaryrefslogtreecommitdiff
path: root/src/spec_analysis.mli
diff options
context:
space:
mode:
authorBrian Campbell2021-02-25 14:41:03 +0000
committerBrian Campbell2021-02-25 14:41:03 +0000
commitbb0a81f2170d068f561c6380bff500d568a7ffd3 (patch)
tree361b00816e07abcb54cbbb06f2c471ae246d8a83 /src/spec_analysis.mli
parent548407add6831460b3392ccaf77b45e55161bbd6 (diff)
Add -infer_effects option
Diffstat (limited to 'src/spec_analysis.mli')
-rw-r--r--src/spec_analysis.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli
index b111f6f0..b77434e7 100644
--- a/src/spec_analysis.mli
+++ b/src/spec_analysis.mli
@@ -79,6 +79,8 @@ val is_within_machine64 : typ -> nexp_range list -> triple *)
val top_sort_defs : tannot ast -> tannot ast
+val infer_effects : string -> tannot ast -> tannot ast
+
(** Return the set of mutable variables assigned to in the given AST. *)
val assigned_vars : 'a exp -> IdSet.t
val assigned_vars_in_fexps : 'a fexp list -> IdSet.t