fix bug #1716 about annotations in while(1)

src/plugins/e-acsl/doc/Changelog

@@ -15,7 +15,8 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
--* E-ACSL       [2014/03/17] Fix bug #1715 about -e-acsl-full-mmodel which
+-* E-ACSL       [2014/03/25] Fix bug #1716 with annotations in while(1).
+-* E-ACSL       [2014/03/25] Fix bug #1715 about -e-acsl-full-mmodel which
 	        generates incorrect code.
 -* E-ACSL       [2014/03/17] Fix bug #1700 about non-ISO empty struct.
 

src/plugins/e-acsl/pre_analysis.ml

@@ -599,7 +599,7 @@ end = struct
 	    List.iter (fun s -> Stmt.Hashtbl.replace tbl s (Some set)) returns)
 	  init_set
       end;
-      D.compute returns
+      D.compute stmts
     with Kernel_function.No_Definition | Kernel_function.No_Statement -> 
       ());
     Options.feedback ~dkey ~level:2 "function %a done."