diff options
| author | Thomas Bauereiss | 2017-09-14 13:55:17 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-09-14 13:55:17 +0100 |
| commit | 4e7a568bb57337d41dda893044ed84b66e62752f (patch) | |
| tree | 337e7c6f617086f3943b13000a97588bb35c7682 /src | |
| parent | cb90735550541fa6752aaad82ff809d84e6c5f88 (diff) | |
Fix bug in topological sorting
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewriter.ml | 2 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 1 |
2 files changed, 2 insertions, 1 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index 62ea6be7..fed8408d 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -3429,7 +3429,7 @@ let rewrite_defs_remove_e_assign = let recheck_defs defs = fst (check initial_env defs) let rewrite_defs_lem =[ - (* top_sort_defs; *) + top_sort_defs; rewrite_trivial_sizeof; rewrite_sizeof; rewrite_defs_remove_vector_concat; 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 = |