[Variadic] A set of tests for the support of ghost parameters

src/plugins/variadic/tests/declared/empty-vpar-with-ghost.c

+/*@ behavior bhv:
+  @ requires c>0;
+  @ requires a<=42;
+*/
+void f(const int a, int, int c,...) /*@ ghost(int x) */;
+
+int main(){
+  f(1, 2, 3) /*@ ghost(4) */;
+  return 0;
+}

src/plugins/variadic/tests/declared/no-va-with-ghost.c

+int f(int a, int b, int c) /*@ ghost(int x) */;
+
+int main(){
+  return f(1, 2, 3) /*@ ghost(4) */;
+}

src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle

+[variadic] tests/declared/empty-vpar-with-ghost.c:1: 
+  Declaration of variadic function f.
+[variadic] tests/declared/empty-vpar-with-ghost.c:8: 
+  Generic translation of call to variadic function.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[kernel] tests/declared/empty-vpar-with-ghost.c:8: Warning: 
+  No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __retres ∈ {0}
+/* Generated by Frama-C */
+/*@ assigns \nothing;
+    
+    behavior bhv:
+      requires c > 0;
+      requires a ≤ 42; */
+void f(int const a, int, int c, void * const *__va_params)/*@ ghost (int x) */;
+
+int main(void)
+{
+  int __retres;
+  {
+    void *__va_args[1] = {(void *)0};
+    f(1,2,3,(void * const *)(__va_args))/*@ ghost (4) */;
+  }
+  __retres = 0;
+  return __retres;
+}
+
+

src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle

+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[kernel:annot:missing-spec] tests/declared/no-va-with-ghost.c:4: Warning: 
+  Neither code nor specification for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  
+/* Generated by Frama-C */
+/*@ assigns \result;
+    assigns \result \from a, b, c; */
+int f(int a, int b, int c)/*@ ghost (int x) */;
+
+int main(void)
+{
+  int tmp;
+  tmp = f(1,2,3)/*@ ghost (4) */;
+  return tmp;
+}
+
+

src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle

+[variadic] tests/declared/rvalues-with-ghost.c:1: 
+  Declaration of variadic function f.
+[variadic] tests/declared/rvalues-with-ghost.c:5: 
+  Generic translation of call to variadic function.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[kernel:annot:missing-spec] tests/declared/rvalues-with-ghost.c:5: Warning: 
+  Neither code nor specification for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  x ∈ {0}
+  i ∈ [--..--]
+  __va_arg0 ∈ {5}
+  __va_arg1 ∈ {20}
+  __va_arg2 ∈ {{ &x }}
+  __va_args[0] ∈ {{ (void *)&__va_arg0 }}
+           [1] ∈ {{ (void *)&__va_arg1 }}
+           [2] ∈ {{ (void *)&__va_arg2 }}
+/* Generated by Frama-C */
+/*@ assigns \result;
+    assigns \result \from a; */
+int f(int a, void * const *__va_params)/*@ ghost (int x) */;
+
+int main(void)
+{
+  int x = 0;
+  int __va_arg0 = 2 + 3;
+  int __va_arg1 = 4 * 5;
+  int *__va_arg2 = & x;
+  void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
+  int i = f(1,(void * const *)(__va_args))/*@ ghost (x + 3) */;
+  return i;
+}
+
+

src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle

+[variadic] tests/declared/simple-with-ghost.c:1: 
+  Declaration of variadic function f.
+[variadic] tests/declared/simple-with-ghost.c:9: 
+  Generic translation of call to variadic function.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[kernel] tests/declared/simple-with-ghost.c:9: Warning: 
+  No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  
+/* Generated by Frama-C */
+/*@ assigns \result;
+    assigns \result \from a, c;
+    
+    behavior bhv:
+      requires c > 0;
+      requires a ≤ 42;
+      ensures \result > 0;
+ */
+int f(int const a, int, int c, void * const *__va_params)/*@ ghost (int x) */;
+
+int main(void)
+{
+  int tmp;
+  {
+    int __va_arg0 = 4;
+    int __va_arg1 = 5;
+    int __va_arg2 = 6;
+    void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
+    tmp = f(1,2,3,(void * const *)(__va_args))/*@ ghost (7) */;
+  }
+  return tmp;
+}
+
+

src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle

+[variadic] tests/declared/typedefed_function-with-ghost.c:2: 
+  Declaration of variadic function f.
+[variadic] tests/declared/typedefed_function-with-ghost.c:5: 
+  Generic translation of call to variadic function.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[kernel:annot:missing-spec] tests/declared/typedefed_function-with-ghost.c:5: Warning: 
+  Neither code nor specification for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __retres ∈ {0}
+/* Generated by Frama-C */
+typedef void T(int , void * const *__va_params)/*@ ghost (int ) */;
+/*@ assigns \nothing; */
+extern T f;
+
+int main(void)
+{
+  int __retres;
+  {
+    int __va_arg0 = 2;
+    int __va_arg1 = 0;
+    void *__va_args[2] = {& __va_arg0, & __va_arg1};
+    f(1,(void * const *)(__va_args))/*@ ghost (3) */;
+  }
+  __retres = 0;
+  return __retres;
+}
+
+

src/plugins/variadic/tests/declared/rvalues-with-ghost.c

+int f(int a,...) /*@ ghost(int x) */;
+
+int main(){
+  int x = 0;
+  int i = f(1, 2+3, 4*5, &x) /*@ ghost(x+3) */;
+  return i;
+}

src/plugins/variadic/tests/declared/simple-with-ghost.c

+/*@ behavior bhv:
+  @ requires c>0;
+  @ requires a<=42;
+  @ ensures \result > 0;
+*/
+int f(const int a, int, int c,...) /*@ ghost (int x) */;
+
+int main(){
+  return f(1, 2, 3, 4, 5, 6) /*@ ghost(7) */;
+}

src/plugins/variadic/tests/declared/typedefed_function-with-ghost.c

+typedef void T(int, ...) /*@ ghost (int) */ ;
+extern T f;
+
+int main () {
+  f(1, 2, 0) /*@ ghost(3) */;
+  return 0;
+}