Merge branch 'fix/eva/goto-skipping-variable-declaration' into 'master'

[Eva] Fixes a bug on goto statement skipping local variable declarations.

See merge request frama-c/frama-c!4245

src/plugins/eva/engine/iterator.ml

@@ -122,12 +122,6 @@ module Make_Dataflow
 
   let active_behaviors = Logic.create AnalysisParam.initial_state kf
 
-  (* Compute the locals that we must enter in scope when we start the analysis
-     of [block]. The other ones will be introduced on the fly, when we
-     encounter a [Local_init] instruction. *)
-  let block_toplevel_locals block =
-    List.filter (fun vi -> not vi.vdefined) block.blocals
-
   let initial_states =
     let state = AnalysisParam.initial_state
     and call_kinstr = AnalysisParam.call_kinstr
@@ -267,8 +261,15 @@ module Make_Dataflow
     : transfer_function =
     lift' (fun s -> Transfer.assign s (Kstmt stmt) dest exp)
 
+  (* All variables local to a block are introduced in domain states when
+     entering the block. Variables explicitly initialized at declaration time
+     (for which vi.vdefined is true) enter the scope too early, as they should
+     be introduced on the fly when encountering their [Local_init] instruction.
+     However, goto statements can skip their declaration/initialization, so it
+     is safer to always introduce all local variables (without initialize them)
+     when entering a block. *)
   let transfer_enter (block : block) : transfer_function =
-    let vars = block_toplevel_locals block in
+    let vars = block.blocals in
     if vars = [] then id else lift (Transfer.enter_scope kf vars)
 
   let transfer_leave (block : block) : transfer_function =
@@ -289,20 +290,12 @@ module Make_Dataflow
   let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
     match instr with
     | Local_init (vi, AssignInit exp, _loc) ->
-      let kind = Abstract_domain.Local kf in
       let transfer state =
-        let state = Domain.enter_scope kind [vi] state in
         Init.initialize_local_variable stmt vi exp state
       in
       lift' transfer
     | Local_init (vi, ConsInit (f, args, k), loc) ->
-      let kind = Abstract_domain.Local kf in
       let as_func dest callee args _loc (key, state) =
-        (* This variable enters the scope too early, as it should
-           be introduced after the call to [f] but before the assignment
-           to [v]. This is currently not possible, at least without
-           splitting Transfer.call in two. *)
-        let state = Domain.enter_scope kind [vi] state in
         transfer_call stmt dest callee args (key, state)
       in
       Cil.treat_constructor_as_func as_func vi f args k loc

tests/builtins/oracle/calloc.0.res.oracle

@@ -40,11 +40,11 @@
 [eva:final-states] Values at end of function main:
   __fc_heap_status ∈ [--..--]
   p1 ∈ [--..--]
-  p2 ∈ [--..--]
-  p3 ∈ [--..--]
-  p4 ∈ [--..--]
-  p5 ∈ [--..--]
-  p9001 ∈ {0}
+  p2 ∈ [--..--] or UNINITIALIZED
+  p3 ∈ [--..--] or UNINITIALIZED
+  p4 ∈ [--..--] or UNINITIALIZED
+  p5 ∈ [--..--] or UNINITIALIZED
+  p9001 ∈ {0} or UNINITIALIZED
   __retres ∈ {0; 1}
 [from] Computing for function main
 [from] Computing for function calloc <-main

tests/builtins/oracle/free.res.oracle

@@ -30,6 +30,9 @@
   q ∈ {{ &__malloc_main1_l10[0] }}
   r ∈ {{ &__malloc_main1_l8[0] ; &__malloc_main1_l10[0] }}
   tmp_1 ∈ {{ &__malloc_main1_l8[0] ; &__malloc_main1_l10[0] }}
+  u ∈ UNINITIALIZED
+  t ∈ UNINITIALIZED
+  s ∈ UNINITIALIZED
   S_0___fc_env[0..1] ∈ [--..--]
   S_1___fc_env[0..1] ∈ [--..--]
   __malloc_main1_l8[0] ∈ UNINITIALIZED

tests/builtins/oracle/realloc.res.oracle

@@ -26,6 +26,7 @@
   Frama_C_entropy_source ∈ [--..--]
   p ∈ {{ &__malloc_main1_l12 }}
   pp ∈ {{ &__malloc_main1_l12 }}
+  q ∈ UNINITIALIZED
   v ∈ [--..--]
   S_0___fc_env[0..1] ∈ [--..--]
   S_1___fc_env[0..1] ∈ [--..--]
@@ -144,6 +145,7 @@
   r ∈ {{ &__malloc_main3_l35[0] }}
   p ∈ {{ &__malloc_main3_l32[0] ; &__malloc_main3_l35[0] }}
   x ∈ {0; 1}
+  s ∈ UNINITIALIZED
   v ∈ [--..--]
   S_0___fc_env[0..1] ∈ [--..--]
   S_1___fc_env[0..1] ∈ [--..--]
@@ -241,6 +243,8 @@
   sizeq ∈ [0..10]
   p ∈ {{ &__malloc_main4_l55[0] }}
   q ∈ {{ &__malloc_main4_l56[0] }}
+  rp ∈ UNINITIALIZED
+  rq ∈ UNINITIALIZED
   v ∈ [--..--]
   S_0___fc_env[0..1] ∈ [--..--]
   S_1___fc_env[0..1] ∈ [--..--]
@@ -356,6 +360,7 @@
   p ∈ {{ &__malloc_main5_l76 }}
   c ∈ {0; 1}
   q ∈ {{ NULL ; &__malloc_main5_l76 }}
+  r ∈ UNINITIALIZED
   v ∈ [--..--]
   S_0___fc_env[0..1] ∈ [--..--]
   S_1___fc_env[0..1] ∈ [--..--]

tests/builtins/oracle/realloc_multiple.0.res.oracle

@@ -36,6 +36,7 @@
   r ∈ {{ &__malloc_main1_l12[0] }}
   p ∈ {{ &__malloc_main1_l9[0] ; &__malloc_main1_l12[0] }}
   x ∈ {0; 1}
+  s ∈ UNINITIALIZED
   v ∈ {1}
   S_0___fc_env[0..1] ∈ [--..--]
   S_1___fc_env[0..1] ∈ [--..--]
@@ -120,6 +121,7 @@
   r ∈ {{ &__malloc_main2_l33[0] }}
   p ∈ {{ NULL ; &__malloc_main2_l30[0] ; &__malloc_main2_l33[0] }}
   x ∈ {0; 1; 2}
+  s ∈ UNINITIALIZED
   v ∈ {2}
   S_0___fc_env[0..1] ∈ [--..--]
   S_1___fc_env[0..1] ∈ [--..--]

tests/builtins/oracle/realloc_multiple.1.res.oracle

@@ -44,6 +44,7 @@
   r ∈ {{ &__malloc_main1_l12[0] }}
   p ∈ {{ &__malloc_main1_l9[0] ; &__malloc_main1_l12[0] }}
   x ∈ {0; 1}
+  s ∈ UNINITIALIZED
   v ∈ {1}
   S_0___fc_env[0..1] ∈ [--..--]
   S_1___fc_env[0..1] ∈ [--..--]
@@ -165,6 +166,7 @@
   r ∈ {{ &__malloc_main2_l33[0] }}
   p ∈ {{ NULL ; &__malloc_main2_l30[0] ; &__malloc_main2_l33[0] }}
   x ∈ {0; 1; 2}
+  s ∈ UNINITIALIZED
   v ∈ {2}
   S_0___fc_env[0..1] ∈ [--..--]
   S_1___fc_env[0..1] ∈ [--..--]

tests/builtins/oracle_gauges/realloc.res.oracle

-627a628,964
+632a633,969
 > [eva] realloc.c:152: Call to builtin realloc
 > [eva:malloc] bases_to_realloc: {__realloc_w_main10_l152}
 > [eva:malloc] realloc.c:152: weak free on bases: {__realloc_w_main10_l152}
@@ -336,7 +336,7 @@
 >   __realloc_w_main10_l152[0] ∈ {4}
 >                          [1] ∈ UNINITIALIZED
 >   ==END OF DUMP==
-694a1032,1096
+699a1037,1101
 > [eva] realloc.c:167: Call to builtin reallocarray
 > [eva] realloc.c:167: Call to builtin reallocarray
 > [eva] computing for function Frama_C_interval <- main11 <- main.
@@ -402,7 +402,7 @@
 > [eva:malloc] bases_to_realloc: {}
 > [eva:malloc] realloc.c:171: strong free on bases: {}
 > [eva] realloc.c:172: Frama_C_show_each_p: {{ NULL ; &__realloc_w_main11_l171 }}
-762,763c1164,1166
+767,768c1169,1171
 <   p ∈ {{ NULL ; &__malloc_main11_l160 ; (int *)&__realloc_main11_l171 }}
 <   q ∈ {0} or UNINITIALIZED or ESCAPINGADDR
 ---

tests/float/oracle/alarms.0.res.oracle

@@ -29,7 +29,12 @@
   ull ∈ {0}
   rand ∈ [--..--]
   l ∈ [--..--]
+  vf ∈ UNINITIALIZED
   tmp ∈ UNINITIALIZED
+  vd ∈ UNINITIALIZED
+  i ∈ UNINITIALIZED
+  j ∈ UNINITIALIZED
+  mvd ∈ UNINITIALIZED
   l ∈ [--..--]
   ==END OF DUMP==
 [kernel:annot:missing-spec] alarms.i:21: Warning: 

tests/float/oracle/alarms.1.res.oracle

@@ -26,7 +26,12 @@
   ull ∈ {0}
   rand ∈ [--..--]
   l ∈ [--..--]
+  vf ∈ UNINITIALIZED
   tmp ∈ UNINITIALIZED
+  vd ∈ UNINITIALIZED
+  i ∈ UNINITIALIZED
+  j ∈ UNINITIALIZED
+  mvd ∈ UNINITIALIZED
   l ∈ [--..--]
   ==END OF DUMP==
 [kernel:annot:missing-spec] alarms.i:21: Warning: 

tests/float/oracle/alarms.2.res.oracle

@@ -23,7 +23,12 @@
   ull ∈ {0}
   rand ∈ [--..--]
   l ∈ [--..--]
+  vf ∈ UNINITIALIZED
   tmp ∈ UNINITIALIZED
+  vd ∈ UNINITIALIZED
+  i ∈ UNINITIALIZED
+  j ∈ UNINITIALIZED
+  mvd ∈ UNINITIALIZED
   l ∈ [--..--]
   ==END OF DUMP==
 [kernel:annot:missing-spec] alarms.i:21: Warning: 

tests/float/oracle/const3.0.res.oracle

@@ -14,6 +14,7 @@
   # cvalue:
   f1 ∈ {9.99994610111e-41}
   d0 ∈ {1e-40}
+  d1 ∈ UNINITIALIZED
   __retres ∈ UNINITIALIZED
   ==END OF DUMP==
 [eva] Recording results for main

tests/float/oracle/const3.1.res.oracle

@@ -16,6 +16,7 @@
   # cvalue:
   f1 ∈ [0x1.16c2000000000p-133 .. 0x1.16c3000000000p-133]
   d0 ∈ [0x1.16c262777579cp-133 .. 0x1.16c262777579dp-133]
+  d1 ∈ UNINITIALIZED
   __retres ∈ UNINITIALIZED
   ==END OF DUMP==
 [eva] Recording results for main

tests/float/oracle/const4.1.res.oracle

@@ -18,6 +18,7 @@
   # cvalue:
   f1 ∈ [3.39999995214e+38 .. 3.40000015497e+38]
   f2 ∈ {3.40282346639e+38}
+  d2 ∈ UNINITIALIZED
   __retres ∈ UNINITIALIZED
   ==END OF DUMP==
 [eva] Recording results for main

tests/float/oracle_equality/alarms.0.res.oracle

-137,139c137,138
+142,144c142,143
 <   u1{.l[bits 0 to 31]; .f; .d[bits 0 to 31]} ∈
 <     [-3.40282346639e+38 .. 3.40282346639e+38]
 <     {.l[bits 32 to 63]; .f[bits 32 to 63]; .d[bits 32 to 63]} ∈ [--..--]

tests/float/oracle_equality/alarms.1.res.oracle

-120,121c120,121
+125,126c125,126
 <   u1{.l[bits 0 to 31]; .f; .d[bits 0 to 31]} ∈ [-inf .. inf]
 <     {.l[bits 32 to 63]; .f[bits 32 to 63]; .d[bits 32 to 63]} ∈ [--..--]
 ---

tests/float/oracle_equality/const3.1.res.oracle

-25c25
+26c26
 <   d1 ∈ [0x1.16c2000000000p-133 .. 0x1.16c3000000000p-133]
 ---
 >   d1 ∈ {0x1.16c2000000000p-133}

tests/libc/oracle/poll.res.oracle

@@ -25,7 +25,7 @@
       .events ∈ {3}
       .revents ∈ [--..--]
   r ∈ {-1; 0; 1}
-  can_read ∈ {0; 1}
-  can_read_out_of_band ∈ {0; 2}
-  invalid_fd ∈ {0; 32}
+  can_read ∈ {0; 1} or UNINITIALIZED
+  can_read_out_of_band ∈ {0; 2} or UNINITIALIZED
+  invalid_fd ∈ {0; 32} or UNINITIALIZED
   __retres ∈ [0..127]

tests/libc/oracle/signal_h.res.oracle

@@ -289,7 +289,7 @@
   s ∈ [--..--]
   uninit ∈ UNINITIALIZED
   old ∈ [--..--] or UNINITIALIZED
-  kill_res ∈ {-1; 0}
+  kill_res ∈ {-1; 0} or UNINITIALIZED
   sa1 ∈
      {{ garbled mix of &{__fc_sigaction}
       (origin: Library function {signal_h.c:45}) }} or UNINITIALIZED

tests/libc/oracle/socket.0.res.oracle

@@ -257,10 +257,10 @@
   __fc_socket_counter ∈ [--..--]
   fd ∈ [-1..1023]
   addr ∈ [--..--] or UNINITIALIZED
-  addrlen ∈ {8}
-  client_fd ∈ [-1..1023]
+  addrlen ∈ {8} or UNINITIALIZED
+  client_fd ∈ [-1..1023] or UNINITIALIZED
   buf[0..63] ∈ [--..--] or UNINITIALIZED
-  r ∈ [-1..64]
+  r ∈ [-1..64] or UNINITIALIZED
   __retres ∈ {0; 1; 5; 20; 100; 200; 300; 400}
 [eva:final-states] Values at end of function main:
   __fc_fds[0..1023] ∈ [--..--]

tests/libc/oracle/socket.1.res.oracle

@@ -259,10 +259,10 @@
   __fc_socket_counter ∈ [--..--]
   fd ∈ [-1..1023]
   addr ∈ [--..--] or UNINITIALIZED
-  addrlen ∈ {8}
-  client_fd ∈ [-1..1023]
+  addrlen ∈ {8} or UNINITIALIZED
+  client_fd ∈ [-1..1023] or UNINITIALIZED
   buf[0..63] ∈ [--..--] or UNINITIALIZED
-  r ∈ [-1..64]
+  r ∈ [-1..64] or UNINITIALIZED
   __retres ∈ {0; 1; 5; 20; 100; 200; 300; 400}
 [eva:final-states] Values at end of function main:
   __fc_fds[0..1023] ∈ [--..--]