Merge branch 'kostyantyn/bugfix/local-init-goto' into 'master'

Fix incorrect tracking of local variables when processing goto statements

See merge request !122

src/plugins/e-acsl/exit_points.ml

@@ -93,47 +93,54 @@ let store_vars stmt =
     Varinfo.Set.empty
     gotos
 
-let list_flatten_to_set =
-  List.fold_left
-    (List.fold_left (fun acc v -> Varinfo.Set.add v acc))
-    Varinfo.Set.empty
+let unify_sets =
+  List.fold_left (fun acc v -> Varinfo.Set.union v acc) Varinfo.Set.empty
 
 class jump_context = object (_)
   inherit Visitor.frama_c_inplace
 
-  val mutable locals = [[]]
+  val mutable locals = []
   (* Maintained list of local variables within the scope of a currently
      visited statement. Variables within a single scope are given by a
-     single list *)
+     single set *)
 
   val jumps = Stack.create ()
   (* Stack of entered switches and loops *)
 
   method !vblock blk =
-    locals <- [blk.blocals] @ locals;
+    (* Filter out variables which definitions appear later in the code *)
+    let vardefs = List.filter (fun vi -> not vi.vdefined) blk.blocals in
+    locals <- Varinfo.Set.of_list vardefs :: locals;
     Cil.DoChildrenPost
-    (fun blk -> locals <- List.tl locals; blk)
+      (fun blk -> locals <- List.tl locals; blk)
 
   method !vstmt stmt =
+    let add_labels stmt =
+      match stmt.labels with
+      | [] -> ()
+      | _ :: _ -> SLocals.add stmt (unify_sets locals)
+    in
     match stmt.skind with
     | Loop _ | Switch _ ->
-      SLocals.add stmt (list_flatten_to_set locals);
+      SLocals.add stmt (unify_sets locals);
       Stack.push stmt jumps;
       Cil.DoChildrenPost (fun st -> ignore(Stack.pop jumps); st)
     | Break _ | Continue _ ->
       Exits.add stmt (Stack.top jumps);
-      SLocals.add stmt (list_flatten_to_set locals);
+      SLocals.add stmt (unify_sets locals);
       Cil.DoChildren
     | Goto(sref, _)  ->
-      SLocals.add stmt (list_flatten_to_set locals);
+      SLocals.add stmt (unify_sets locals);
       Exits.add stmt !sref;
       LJumps.add !sref stmt;
       Cil.DoChildren
+    | Instr(Local_init (vi, _, _)) ->
+      locals <- (Varinfo.Set.add vi (List.hd locals)) :: List.tl locals;
+      add_labels stmt;
+      Cil.DoChildren
     | Instr _ | Return _ | If _ | Block _ | UnspecifiedSequence _
     | Throw _ | TryCatch _ | TryFinally _ | TryExcept _ ->
-      (match stmt.labels with
-      | [] -> ()
-      | _ :: _ -> SLocals.add stmt (list_flatten_to_set locals));
+      add_labels stmt;
       Cil.DoChildren
 end
 

src/plugins/e-acsl/tests/runtime/local_goto.c

+/* run.config
+   COMMENT: Check that deleting statements before goto jumps takes into
+   COMMENT: account variable declarations given via local inits
+*/
+#include <stdio.h>
+
+#define describe(lab) \
+  printf("t is %d, going to %s\n", t, #lab)
+
+int main(int argc, const char **argv) {
+  int t = 0;
+
+  {
+UP:
+    if (t == 2) {
+      describe(RET);
+      goto RET;
+    }
+  }
+
+AGAIN:
+  {
+    int a;
+    a = 1;
+    /*@assert \valid(&a); */
+
+    if (t == 2) {
+      describe(UP);
+      /* When jumping to UP label we need to make sure that the
+         program transformation does not insert a call deleting [b]. */
+      goto UP;
+    } else
+      t++;
+
+    int b = 15;
+    /*@assert \valid(&b); */
+    describe(AGAIN);
+    goto AGAIN;
+  }
+
+RET:
+  return 0;
+}

src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c

+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+char *__gen_e_acsl_literal_string;
+char *__gen_e_acsl_literal_string_3;
+char *__gen_e_acsl_literal_string_2;
+char *__gen_e_acsl_literal_string_4;
+void __e_acsl_globals_init(void)
+{
+  __gen_e_acsl_literal_string = "t is %d, going to %s\n";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+                       sizeof("t is %d, going to %s\n"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+  __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
+  __gen_e_acsl_literal_string_3 = "UP";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,sizeof("UP"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
+  __e_acsl_readonly((void *)__gen_e_acsl_literal_string_3);
+  __gen_e_acsl_literal_string_2 = "RET";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,sizeof("RET"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
+  __e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
+  __gen_e_acsl_literal_string_4 = "AGAIN";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,sizeof("AGAIN"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
+  __e_acsl_readonly((void *)__gen_e_acsl_literal_string_4);
+  return;
+}
+
+int main(int argc, char const **argv)
+{
+  int __retres;
+  __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
+  __e_acsl_globals_init();
+  int t = 0;
+  UP: ;
+  if (t == 2) {
+    __gen_e_acsl_printf_va_1(__gen_e_acsl_literal_string,t,
+                             (char *)__gen_e_acsl_literal_string_2);
+    goto RET;
+  }
+  AGAIN:
+    {
+      int a;
+      __e_acsl_store_block((void *)(& a),(size_t)4);
+      __e_acsl_full_init((void *)(& a));
+      a = 1;
+      /*@ assert \valid(&a); */
+      {
+        {
+          int __gen_e_acsl_valid;
+          __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int));
+          __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",
+                          (char *)"main",(char *)"\\valid(&a)",25);
+        }
+      }
+      if (t == 2) {
+        __gen_e_acsl_printf_va_2(__gen_e_acsl_literal_string,t,
+                                 (char *)__gen_e_acsl_literal_string_3);
+        __e_acsl_delete_block((void *)(& a));
+        goto UP;
+      }
+      else t ++;
+      int b = 15;
+      __e_acsl_store_block((void *)(& b),(size_t)4);
+      __e_acsl_full_init((void *)(& b));
+      /*@ assert \valid(&b); */
+      {
+        {
+          int __gen_e_acsl_valid_2;
+          __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int));
+          __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
+                          (char *)"main",(char *)"\\valid(&b)",36);
+        }
+      }
+      __gen_e_acsl_printf_va_3(__gen_e_acsl_literal_string,t,
+                               (char *)__gen_e_acsl_literal_string_4);
+      __e_acsl_delete_block((void *)(& a));
+      __e_acsl_delete_block((void *)(& b));
+      goto AGAIN;
+      __e_acsl_delete_block((void *)(& b));
+      __e_acsl_delete_block((void *)(& a));
+    }
+  RET: __retres = 0;
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle

+[variadic] warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.
+[e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `printf_va_1':
+                  the generated program may miss memory instrumentation
+                  if there are memory-related annotations.
+[e-acsl] warning: annotating undefined function `printf_va_2':
+                  the generated program may miss memory instrumentation
+                  if there are memory-related annotations.
+[e-acsl] warning: annotating undefined function `printf_va_3':
+                  the generated program may miss memory instrumentation
+                  if there are memory-related annotations.
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+tests/runtime/local_goto.c:37:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+tests/runtime/local_goto.c:28:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+tests/runtime/local_goto.c:16:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.