Merge branch 'fix/variadic/unspecified-sequences-calls' into 'master'

[Variadic] Fix the references to calls in unspecified sequences

Closes #327

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

src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle

+[variadic] sum_with_unspecified_sequence.c:8: 
+  Declaration of variadic function sum.
+[eva] Analyzing a complete application starting at sum
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:alarm] sum_with_unspecified_sequence.c:14: Warning: 
+  out of bounds read. assert \valid_read(list);
+[eva:alarm] sum_with_unspecified_sequence.c:14: Warning: 
+  out of bounds read. assert \valid_read((int *)*list);
+[eva] sum_with_unspecified_sequence.c:14: 
+  Assigning imprecise value to tmp_unroll_5.
+  The imprecision originates from Well
+[eva:alarm] sum_with_unspecified_sequence.c:14: Warning: 
+  signed overflow.
+  assert -2147483648 ≤ ret + tmp_unroll_5;
+  (tmp_unroll_5 from vararg)
+[eva:alarm] sum_with_unspecified_sequence.c:14: Warning: 
+  signed overflow.
+  assert ret + tmp_unroll_5 ≤ 2147483647;
+  (tmp_unroll_5 from vararg)
+[eva] sum_with_unspecified_sequence.c:14: 
+  Assigning imprecise value to ret.
+  The imprecision originates from Well
+[eva:alarm] sum_with_unspecified_sequence.c:14: Warning: 
+  out of bounds read. assert \valid_read(list);
+[eva:alarm] sum_with_unspecified_sequence.c:14: Warning: 
+  out of bounds read. assert \valid_read((int *)*list);
+[eva] sum_with_unspecified_sequence.c:14: 
+  Assigning imprecise value to tmp.
+  The imprecision originates from Well
+[eva:alarm] sum_with_unspecified_sequence.c:14: Warning: 
+  signed overflow. assert -2147483648 ≤ ret + tmp;
+                   (tmp from vararg)
+[eva:alarm] sum_with_unspecified_sequence.c:14: Warning: 
+  signed overflow. assert ret + tmp ≤ 2147483647;
+                   (tmp from vararg)
+[eva] sum_with_unspecified_sequence.c:17: 
+  Assigning imprecise value to \result<sum>.
+  The imprecision originates from Well
+[eva] done for function sum
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function sum:
+  ret ∈
+     {{ garbled mix of &{S_0_S___va_params; S_1_S___va_params}
+      (origin: Well) }}
+  i ∈ {0; 1; 2}
+  list ∈ {{ NULL ; &S___va_params{[0], [1], [2]} }}
+/* Generated by Frama-C */
+#include "stdarg.h"
+int sum(int n, void * const *__va_params)
+{
+  int i;
+  va_list list;
+  int ret = 0;
+  list = __va_params;
+  i = 0;
+  if (! (i < n)) goto unrolling_2_loop;
+  {
+    int tmp_unroll_5;
+    /*@ assert Eva: mem_access: \valid_read(list); */
+    /*@ assert Eva: mem_access: \valid_read((int *)*list); */
+    tmp_unroll_5 = *((int *)*list);
+    list ++;
+    /*@ assert Eva: signed_overflow: -2147483648 ≤ ret + tmp_unroll_5; */
+    /*@ assert Eva: signed_overflow: ret + tmp_unroll_5 ≤ 2147483647; */
+    ret += tmp_unroll_5;
+  }
+  i ++;
+  unrolling_3_loop: ;
+  /*@ loop pragma UNROLL "done", 1; */
+  while (i < n) {
+    {
+      int tmp;
+      /*@ assert Eva: mem_access: \valid_read(list); */
+      /*@ assert Eva: mem_access: \valid_read((int *)*list); */
+      tmp = *((int *)*list);
+      list ++;
+      /*@ assert Eva: signed_overflow: -2147483648 ≤ ret + tmp; */
+      /*@ assert Eva: signed_overflow: ret + tmp ≤ 2147483647; */
+      ret += tmp;
+    }
+    i ++;
+  }
+  unrolling_2_loop: ;
+  return ret;
+}
+
+

src/plugins/variadic/tests/defined/sum_with_unspecified_sequence.c

+/* run.config
+STDOPT: +"-main sum -ulevel 1"
+*/
+
+
+#include <stdarg.h>
+
+int sum(int n, ...){
+  int ret = 0;
+  int i;
+  va_list list;
+  va_start(list, n);
+  for(i=0; i<n; i++){
+    ret += va_arg(list, int);
+  }
+  va_end(list);
+  return ret;
+}

src/plugins/variadic/translate.ml

@@ -57,6 +57,22 @@ let translate_variadics (file : file) =
   in
   Cil.visitCilFile v file;
 
+  (* Utility function that tells if there is a call inside a statement *)
+  let contains_call stmt =
+    let result = ref false in
+    let vis = object
+      inherit Cil.nopCilVisitor
+      method! vinst = function
+        | Call _ -> result := true; Cil.SkipChildren
+        | _ -> Cil.DoChildren
+      method! vexpr _ = Cil.SkipChildren
+      method! vtype _ = Cil.SkipChildren
+    end
+    in
+    ignore (Cil.visitCilStmt vis stmt);
+    !result
+  in
+
   (* The translating visitor *)
   let v = object (self)
     inherit Cil.nopCilVisitor
@@ -123,6 +139,19 @@ let translate_variadics (file : file) =
           | _ -> s
         in
         Cil.DoChildrenPost keep_block_if_needed
+      | UnspecifiedSequence _ ->
+        let update_seq_if_needed s =
+          match s.skind with
+          | UnspecifiedSequence seq ->
+            let update (stmt,modified,writes,reads,calls) =
+              let contains_call' stmt_ref = contains_call !stmt_ref in
+              (stmt,modified,writes,reads,List.filter contains_call' calls)
+            in
+            s.skind <- UnspecifiedSequence (List.map update seq);
+            s
+          | _ -> s
+        in
+        Cil.DoChildrenPost update_seq_if_needed
       | _ -> Cil.DoChildren
 
     (* Replace variadic calls *)