[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

[SRM] Stable update for Frama-C



Hi,

I’d like to propose the following change for Frama-C.

--- Changelog   (revision 11098)
+++ Changelog   (working copy)
@@ -12,6 +12,8 @@
 # '#?nnn'  : OLD-BTS entry #nnn
       #
 ###############################################################################

+-* Inout      [2010/12/22] Return statement dependencies were forgotten in
+             operational input computations.
 o! Kernel     [2010/12/21] Remove API function Messages.enable_collect:
              please let the kernel do the job.
 -  GUI        [2010/12/21] Implement feature #635: display messages in the
Index: src/inout/context.ml
===================================================================
--- src/inout/context.ml        (revision 11098)
+++ src/inout/context.ml        (working copy)
@@ -115,7 +115,8 @@
   let computeFirstPredecessor (s: stmt) data =
     match s.skind with
       | Switch (exp,_,_,_)
-      | If (exp,_,_,_) ->
+      | If (exp,_,_,_)
+      | Return (Some exp, _) ->
           let inputs = !From.find_deps_no_transitivity (Kstmt s) exp in
             {data with
                over_inputs =

Is it OK for squeeze?

Regards,

-- 
Mehdi Dogguy مهدي الدڤي
http://dogguy.org/


Reply to: