Merge branch 'bugfix/julien/instrument-variadic' into 'stable/potassium'

fix bug when combining -e-acsl-instrument and -variadic-no-translation (fix issue #88)

See merge request frama-c/e-acsl!292

src/plugins/e-acsl/dup_functions.ml

@@ -227,6 +227,18 @@ type position = Before_gmp | Gmp | After_gmp | Memory_model | Code
 class dup_functions_visitor prj = object (self)
   inherit Visitor.frama_c_copy prj
 
+  val unduplicable_functions =
+    let white_list =
+      [ "__builtin_va_arg";
+        "__builtin_va_end";
+        "__builtin_va_start";
+        "__builtin_va_copy" ]
+    in
+    List.fold_left
+      (fun acc s -> Datatype.String.Set.add s acc)
+      Datatype.String.Set.empty
+      white_list
+
   val fct_tbl = Cil_datatype.Varinfo.Hashtbl.create 7
   val mutable before_memory_model = Before_gmp
   val mutable new_definitions: global list = []
@@ -288,25 +300,27 @@ class dup_functions_visitor prj = object (self)
   | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
       when (* duplicate a function iff: *)
         not (Cil_datatype.Varinfo.Hashtbl.mem fct_tbl vi)
-         (* it is not already duplicated *)
+        (* it is not already duplicated *)
+        && not (Datatype.String.Set.mem vi.vname unduplicable_functions)
+        (* it is duplicable *)
         && self#is_unvariadic_function vi (* it is not a variadic function *)
-         && not (Misc.is_library_loc loc) (* it is not in the E-ACSL's RTL *)
-         && not (Cil.is_builtin vi) (* it is not a Frama-C built-in *)
-         &&
-         (let kf =
-            try Globals.Functions.get vi with Not_found -> assert false
-          in
-          not (Functions.instrument kf)
+        && not (Misc.is_library_loc loc) (* it is not in the E-ACSL's RTL *)
+        && not (Cil.is_builtin vi) (* it is not a Frama-C built-in *)
+        &&
+        (let kf =
+           try Globals.Functions.get vi with Not_found -> assert false
+         in
+         not (Functions.instrument kf)
          (* either explicitely listed as to be not instrumented *)
          ||
          (* or: *)
-          (not (Cil.is_empty_funspec
-                    (Annotations.funspec ~populate:false
-                       (Extlib.the self#current_kf)))
+         (not (Cil.is_empty_funspec
+                 (Annotations.funspec ~populate:false
+                    (Extlib.the self#current_kf)))
           (* it has a function contract *)
           && Functions.check kf
           (* its annotations must be monitored *)))
-         ->
+      ->
     self#next ();
     let name = Functions.RTL.mk_gen_name vi.vname in
     let new_vi = 

src/plugins/e-acsl/tests/special/e-acsl-instrument.c

 /* run.config
-   COMMENT: test option -e-acsl-instrument
+   COMMENT: test option -e-acsl-instrument; cannot run Eva on this example
    LOG: gen_@PTEST_NAME@.c
-   OPT: -machdep gcc_x86_64 -e-acsl-instrument="@@all,-uninstrument1,-uninstrument2" -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva-verbose 0 -eva
+   OPT: -variadic-no-translation -machdep gcc_x86_64 -e-acsl-instrument="@@all,-uninstrument1,-uninstrument2" -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c -kernel-verbose 0
 */
 
+#include <stdarg.h>
+
 int uninstrument1(int *p) {
   *p = 0;
   return 0;
@@ -12,7 +14,7 @@ int uninstrument1(int *p) {
 /*@ requires \valid(p); */
 int uninstrument2(int *p) {
   { int *q = p;
-    *p = 0; 
+    *p = 0;
     goto L;
   }
  L:
@@ -27,13 +29,23 @@ int instrument1(int *p) {
 /*@ requires \valid(p); */
 int instrument2(int *p) {
   { int *q = p;
-    *p = 0; 
+    *p = 0;
     goto L;
   }
  L:
   return 0;
 }
 
+/* test combination of -e-acsl-instrument and -variadic-no-translation;
+   see gitlab's issue #88 */
+int vol(int n, ...) {
+  va_list vl;
+  va_start(vl, n);
+  int r = va_arg(vl, int);
+  va_end(vl);
+  return 1;
+}
+
 int main(void) {
   int x;
   int y = 0;
@@ -43,4 +55,5 @@ int main(void) {
   uninstrument2(&x);
   /*@ assert \initialized(&x); */
   /*@ assert \initialized(&y); */
+  return vol(6, 1);
 }

src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle

 [e-acsl] beginning translation.
+[kernel:annot:missing-spec] :0: Warning: 
+  Neither code nor specification for function __builtin_va_arg, generating default assigns from the prototype
+[kernel:annot:missing-spec] :0: Warning: 
+  Neither code nor specification for function __builtin_va_end, generating default assigns from the prototype
+[kernel:annot:missing-spec] :0: Warning: 
+  Neither code nor specification for function __builtin_va_start, generating default assigns from the prototype
+[e-acsl] tests/special/e-acsl-instrument.c:58: Warning: 
+  ignoring effect of variadic function vol
 [e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c

 /* Generated by Frama-C */
+#include "stdarg.h"
 #include "stdio.h"
 #include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
+/* compiler builtin: 
+   void __builtin_va_arg(__builtin_va_list, unsigned long, void *);   */
+/* compiler builtin: 
+   void __builtin_va_end(__builtin_va_list);   */
+/* compiler builtin: 
+   void __builtin_va_start(__builtin_va_list);   */
 int __gen_e_acsl_uninstrument1(int *p);
 
 int uninstrument1(int *p)
@@ -61,10 +68,23 @@ int instrument2(int *p)
   return __retres;
 }
 
-int main(void)
+int vol(int n , ...)
 {
   int __retres;
+  va_list vl;
+  int tmp;
+  __builtin_va_start(vl,n);
+  tmp = __builtin_va_arg (vl, int);
+  int r = tmp;
+  __builtin_va_end(vl);
+  __retres = 1;
+  return __retres;
+}
+
+int main(void)
+{
   int x;
+  int tmp;
   __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __e_acsl_store_block((void *)(& x),(size_t)4);
   int y = 0;
@@ -80,7 +100,7 @@ int main(void)
     __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& x),
                                                     sizeof(int));
     __e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
-                    (char *)"main",(char *)"\\initialized(&x)",44);
+                    (char *)"main",(char *)"\\initialized(&x)",56);
   }
   /*@ assert \initialized(&y); */
   {
@@ -88,13 +108,13 @@ int main(void)
     __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& y),
                                                       sizeof(int));
     __e_acsl_assert(__gen_e_acsl_initialized_2,(char *)"Assertion",
-                    (char *)"main",(char *)"\\initialized(&y)",45);
+                    (char *)"main",(char *)"\\initialized(&y)",57);
   }
-  __retres = 0;
+  tmp = vol(6,1);
   __e_acsl_delete_block((void *)(& y));
   __e_acsl_delete_block((void *)(& x));
   __e_acsl_memory_clean();
-  return __retres;
+  return tmp;
 }
 
 /*@ requires \valid(p); */
@@ -107,7 +127,7 @@ int __gen_e_acsl_instrument2(int *p)
     __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
                                         (void *)(& p));
     __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",
-                    (char *)"instrument2",(char *)"\\valid(p)",27);
+                    (char *)"instrument2",(char *)"\\valid(p)",29);
   }
   __retres = instrument2(p);
   __e_acsl_delete_block((void *)(& p));
@@ -123,7 +143,7 @@ int __gen_e_acsl_uninstrument2(int *p)
     __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
                                         (void *)(& p));
     __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",
-                    (char *)"uninstrument2",(char *)"\\valid(p)",12);
+                    (char *)"uninstrument2",(char *)"\\valid(p)",14);
   }
   __e_acsl_sound_verdict = 0;
   __retres = uninstrument2(p);