summaryrefslogtreecommitdiff
path: root/src/spec_analysis.ml
diff options
context:
space:
mode:
authorBrian Campbell2017-09-18 16:31:56 +0100
committerBrian Campbell2017-09-18 16:31:56 +0100
commit4d83d5cf11751b990055963797b5919bf7c22b0b (patch)
tree329c2cd838c467430146ceafd662f6a8a7091d40 /src/spec_analysis.ml
parentd7d7b781e91abbefca7e7a037c4109b3db89f958 (diff)
parent4e7a568bb57337d41dda893044ed84b66e62752f (diff)
Merge branch 'experiments' into mono-experiments
Diffstat (limited to 'src/spec_analysis.ml')
-rw-r--r--src/spec_analysis.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 5281ef27..d349037e 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -350,6 +350,7 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
b,used,set
| E_exit e -> fv_of_exp consider_var bound used set e
| E_assert(c,m) -> list_fv bound used set [c;m]
+ | E_return e -> fv_of_exp consider_var bound used set e
| _ -> bound,used,set
and fv_of_pes consider_var bound used set pes =