From 4e7a568bb57337d41dda893044ed84b66e62752f Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 14 Sep 2017 13:55:17 +0100
Subject: Fix bug in topological sorting

---
 src/rewriter.ml      | 2 +-
 src/spec_analysis.ml | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

(limited to 'src')

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 =
-- 
cgit v1.2.3