diff options
| author | Alasdair Armstrong | 2017-09-14 15:55:28 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-09-14 15:55:28 +0100 |
| commit | bf509b250cf676e96e11ace54648f30e43848754 (patch) | |
| tree | f0add29f0b908e41c26220ab5af26be1c3ed53ae /src/spec_analysis.ml | |
| parent | 59892ba3127112fd2c5c6b3cd93ab4f29502ebb2 (diff) | |
| parent | 4e7a568bb57337d41dda893044ed84b66e62752f (diff) | |
Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into experiments
Diffstat (limited to 'src/spec_analysis.ml')
| -rw-r--r-- | src/spec_analysis.ml | 1 |
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 = |