diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c
index ee5d632ef771e23467dfb6e520001caf93795f36..f07cda26a8b3a278cc708ff099b341b56ab2971a 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c
@@ -116,21 +116,7 @@ char *__gen_e_acsl_strdup(char const *s);
__inline static void fail_ncomp(int cond, char *fmt, int l, int r)
{
if (cond) {
- {
- int __va_arg0 = l;
- __e_acsl_store_block((void *)(& __va_arg0),(size_t)4);
- __e_acsl_full_init((void *)(& __va_arg0));
- int __va_arg1 = r;
- __e_acsl_store_block((void *)(& __va_arg1),(size_t)4);
- __e_acsl_full_init((void *)(& __va_arg1));
- void *__va_args[2] = {& __va_arg0, & __va_arg1};
- __e_acsl_store_block((void *)(__va_args),(size_t)16);
- __e_acsl_full_init((void *)(& __va_args));
- fprintf(stderr,(char const *)fmt,(void * const *)(__va_args));
- __e_acsl_delete_block((void *)(__va_args));
- __e_acsl_delete_block((void *)(& __va_arg1));
- __e_acsl_delete_block((void *)(& __va_arg0));
- }
+ fprintf(stderr,(char const *)fmt,l,r); /* fprintf_fallback_1 */
__gen_e_acsl_abort();
}
return;
diff --git a/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
index 5b3e8c0a4dd45b2df63d9d154c0eb737cbccb519..3964a37c4107508e018d69cb6119d25a96bbcbe6 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
@@ -11,11 +11,11 @@
[variadic] tests/erroneous/exec.c:7: Warning:
Failed to find a sentinel (NULL pointer) in the argument list.
[variadic] tests/erroneous/exec.c:7:
- Generic translation of call to variadic function.
+ Fallback translation of call execlp to a call to the specialized version execlp_fallback_1.
[variadic] tests/erroneous/exec.c:9: Warning:
Not enough arguments: expected 5, given 4.
[variadic] tests/erroneous/exec.c:9:
- Generic translation of call to variadic function.
+ Fallback translation of call execle to a call to the specialized version execle_fallback_1.
[variadic] tests/erroneous/exec.c:11: Warning:
Incorrect type for argument 5. The argument will be cast from int to char * const *.
[variadic] tests/erroneous/exec.c:11:
diff --git a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
index c4e0b6755536fe283e3d06bf066e2af31afa11cf..648e90041fe3c2953176a9b9b26a7cb63d420214 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
@@ -18,4 +18,4 @@
[variadic] tests/erroneous/printf.c:8: Warning:
Flag ' ' and conversion specififer e are not compatibles.
[variadic] tests/erroneous/printf.c:8:
- Generic translation of call to variadic function.
+ Fallback translation of call printf to a call to the specialized version printf_fallback_1.
diff --git a/src/plugins/variadic/tests/known/oracle/exec.res.oracle b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
index 3f46be4f8ff5f3509d6a207b7ae35f78f2c1e39a..d3df0e6caaecd4de576cc56e389dabf8762146eb 100644
--- a/src/plugins/variadic/tests/known/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
@@ -19,14 +19,19 @@
[variadic] tests/known/exec.c:15: Warning:
Failed to find a sentinel (NULL pointer) in the argument list.
[variadic] tests/known/exec.c:15:
- Generic translation of call to variadic function.
+ Fallback translation of call execlp to a call to the specialized version execlp_fallback_1.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function execve
[eva] using specification for function execv
[eva] using specification for function execvp
-[eva] using specification for function execlp
+[kernel:annot:missing-spec] tests/known/exec.c:15: Warning:
+ Neither code nor specification for function execlp_fallback_1, generating default assigns from the prototype
+[eva] using specification for function execlp_fallback_1
+[eva:invalid-assigns] tests/known/exec.c:15:
+ Completely invalid destination for assigns clause *(param1 + (0 ..)).
+ Ignoring.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -36,6 +41,17 @@
__retres ∈ {0}
/* Generated by Frama-C */
#include "unistd.h"
+/*@ assigns \result, *(param1 + (0 ..));
+ assigns \result
+ \from *(path + (0 ..)), *(arg + (0 ..)), *(param0 + (0 ..)),
+ *(param1 + (0 ..));
+ assigns *(param1 + (0 ..))
+ \from *(path + (0 ..)), *(arg + (0 ..)), *(param0 + (0 ..)),
+ *(param1 + (0 ..));
+ */
+int execlp_fallback_1(char const *path, char const *arg, char const *param0,
+ char *param1);
+
int main(void)
{
int __retres;
@@ -63,12 +79,7 @@ int main(void)
void *tmp_16 = (void *)0;
execve("ls",argv_12,(char * const *)(env));
}
- {
- char const *__va_arg0 = "--reverse";
- char *__va_arg1 = sentinel;
- void *__va_args[2] = {& __va_arg0, & __va_arg1};
- execlp("ls","ls",(void * const *)(__va_args));
- }
+ execlp("ls","ls","--reverse",sentinel); /* execlp_fallback_1 */
__retres = 0;
return __retres;
}
diff --git a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
index a561da371e26fa37c9312f6d6748499e08871a3c..4c3cf265c241707952e9f7525ea4fa17e225d14e 100644
--- a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
@@ -18,7 +18,7 @@
Given arguments:
fcntl(int, int, int, int)
[variadic] tests/known/fcntl.c:16:
- Generic translation of call to variadic function.
+ Fallback translation of call fcntl to a call to the specialized version fcntl_fallback_1.
[variadic] tests/known/fcntl.c:20:
Translating call to the specialized version fcntl(int, int).
[variadic] tests/known/fcntl.c:24:
@@ -32,18 +32,23 @@
Given arguments:
fcntl(int, int, double)
[variadic] tests/known/fcntl.c:28:
- Generic translation of call to variadic function.
+ Fallback translation of call fcntl to a call to the specialized version fcntl_fallback_2.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function __va_fcntl_void
[eva] using specification for function __va_fcntl_int
[eva] using specification for function __va_fcntl_flock
-[eva] using specification for function fcntl
+[kernel:annot:missing-spec] tests/known/fcntl.c:16: Warning:
+ Neither code nor specification for function fcntl_fallback_1, generating default assigns from the prototype
+[eva] using specification for function fcntl_fallback_1
[eva:alarm] tests/known/fcntl.c:20: Warning:
function __va_fcntl_void: precondition 'cmd_has_void_arg' got status invalid.
[eva:alarm] tests/known/fcntl.c:24: Warning:
function __va_fcntl_flock: precondition 'cmd_as_flock_arg' got status invalid.
+[kernel:annot:missing-spec] tests/known/fcntl.c:28: Warning:
+ Neither code nor specification for function fcntl_fallback_2, generating default assigns from the prototype
+[eva] using specification for function fcntl_fallback_2
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -53,6 +58,14 @@
__retres ∈ {0}
/* Generated by Frama-C */
#include "fcntl.h"
+/*@ assigns \result;
+ assigns \result \from fd, cmd, param0, param1; */
+int fcntl_fallback_1(int fd, int cmd, int param0, int param1);
+
+/*@ assigns \result;
+ assigns \result \from fd, cmd, param0; */
+int fcntl_fallback_2(int fd, int cmd, double param0);
+
int main(void)
{
int __retres;
@@ -62,21 +75,10 @@ int main(void)
fcntl(0,2,flags); /* __va_fcntl_int */
fcntl(0,5,& fl); /* __va_fcntl_flock */
switch (choice) {
- case 1:
- {
- int __va_arg0 = flags;
- int __va_arg1 = 5;
- void *__va_args[2] = {& __va_arg0, & __va_arg1};
- fcntl(0,2,(void * const *)(__va_args));
- }
+ case 1: fcntl(0,2,flags,5); /* fcntl_fallback_1 */
case 2: fcntl(0,2); /* __va_fcntl_void */
case 3: fcntl(0,2,& fl); /* __va_fcntl_flock */
- case 4:
- {
- double __va_arg0_9 = 0.5;
- void *__va_args_11[1] = {& __va_arg0_9};
- fcntl(0,2,(void * const *)(__va_args_11));
- }
+ case 4: fcntl(0,2,0.5); /* fcntl_fallback_2 */
}
__retres = 0;
return __retres;
diff --git a/src/plugins/variadic/tests/known/oracle/open.res.oracle b/src/plugins/variadic/tests/known/oracle/open.res.oracle
index 6873ba53a36872a23e484504ef6c8c6e98bde8cf..6561ada302004f8db755da9b92c58da579a9221c 100644
--- a/src/plugins/variadic/tests/known/oracle/open.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open.res.oracle
@@ -17,13 +17,15 @@
Given arguments:
open(char const *, int, int, int, char const *, int)
[variadic] tests/known/open.c:9:
- Generic translation of call to variadic function.
+ Fallback translation of call open to a call to the specialized version open_fallback_1.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function __va_open_mode_t
[eva] using specification for function __va_open_void
-[eva] using specification for function open
+[kernel:annot:missing-spec] tests/known/open.c:9: Warning:
+ Neither code nor specification for function open_fallback_1, generating default assigns from the prototype
+[eva] using specification for function open_fallback_1
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -32,18 +34,18 @@
file ∈ {{ "file" }}
fd1 ∈ [-1..1023]
fd2 ∈ [-1..1023]
- fd3 ∈ [-1..1023]
- __va_arg0 ∈ {0}
- __va_arg1 ∈ {3}
- __va_arg2 ∈ {{ "arg4" }}
- __va_arg3 ∈ {5}
- __va_args[0] ∈ {{ (void *)&__va_arg0 }}
- [1] ∈ {{ (void *)&__va_arg1 }}
- [2] ∈ {{ (void *)&__va_arg2 }}
- [3] ∈ {{ (void *)&__va_arg3 }}
+ fd3 ∈ [--..--]
__retres ∈ {0}
/* Generated by Frama-C */
#include "fcntl.h"
+/*@ assigns \result;
+ assigns \result
+ \from *(filename + (0 ..)), *(param2 + (0 ..)), flags, param0, param1,
+ param3;
+ */
+int open_fallback_1(char const *filename, int flags, int param0, int param1,
+ char const *param2, int param3);
+
int main(void)
{
int __retres;
@@ -52,12 +54,7 @@ int main(void)
char *file = (char *)"file";
int fd1 = __va_open_mode_t((char const *)file,flag,(mode_t)mode);
int fd2 = __va_open_void((char const *)file,flag);
- int __va_arg0 = mode;
- int __va_arg1 = 3;
- char const *__va_arg2 = "arg4";
- int __va_arg3 = 5;
- void *__va_args[4] = {& __va_arg0, & __va_arg1, & __va_arg2, & __va_arg3};
- int fd3 = open((char const *)file,flag,(void * const *)(__va_args));
+ int fd3 = open_fallback_1((char const *)file,flag,mode,3,"arg4",5);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
index 4bf24c1ad904f1cbd8eced6a8d494075f6d89418..f79b30145e845ed17e8e53550b054fa33c4f4d75 100644
--- a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
@@ -11,11 +11,13 @@
Given arguments:
open(char const *, int, char const *)
[variadic] tests/known/open_wrong.c:13:
- Generic translation of call to variadic function.
+ Fallback translation of call open to a call to the specialized version open_fallback_1.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva] using specification for function open
+[kernel:annot:missing-spec] tests/known/open_wrong.c:13: Warning:
+ Neither code nor specification for function open_fallback_1, generating default assigns from the prototype
+[eva] using specification for function open_fallback_1
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -24,16 +26,17 @@
__retres ∈ {0}
/* Generated by Frama-C */
#include "fcntl.h"
+/*@ assigns \result;
+ assigns \result \from *(filename + (0 ..)), *(param0 + (0 ..)), flags;
+ */
+int open_fallback_1(char const *filename, int flags, char const *param0);
+
int main(void)
{
int __retres;
char *file = (char *)"file";
int flag = 0;
- {
- char const *__va_arg0 = "";
- void *__va_args[1] = {& __va_arg0};
- open((char const *)file,flag,(void * const *)(__va_args));
- }
+ open((char const *)file,flag,""); /* open_fallback_1 */
__retres = 0;
return __retres;
}
diff --git a/src/plugins/variadic/tests/known/oracle/openat.res.oracle b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
index 8cf6482eaf7aecabc3dd52d8fd7d081f5ce7f552..18436d2d088c41e73b3979840d7d05a2ba6160e2 100644
--- a/src/plugins/variadic/tests/known/oracle/openat.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
@@ -17,12 +17,14 @@
Given arguments:
openat(int, char const *, int, double)
[variadic] tests/known/openat.c:10:
- Generic translation of call to variadic function.
+ Fallback translation of call openat to a call to the specialized version openat_fallback_1.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function __va_openat_mode_t
-[eva] using specification for function openat
+[kernel:annot:missing-spec] tests/known/openat.c:10: Warning:
+ Neither code nor specification for function openat_fallback_1, generating default assigns from the prototype
+[eva] using specification for function openat_fallback_1
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -33,6 +35,12 @@
__retres ∈ {0}
/* Generated by Frama-C */
#include "fcntl.h"
+/*@ assigns \result;
+ assigns \result \from *(filename + (0 ..)), dirfd, flags, param0;
+ */
+int openat_fallback_1(int dirfd, char const *filename, int flags,
+ double param0);
+
int main(void)
{
int __retres;
@@ -42,11 +50,7 @@ int main(void)
char *file = (char *)"file";
openat(0,(char const *)file,flag,mode1); /* __va_openat_mode_t */
openat(0,(char const *)file,flag,(mode_t)mode2); /* __va_openat_mode_t */
- {
- double __va_arg0 = 3.0;
- void *__va_args[1] = {& __va_arg0};
- openat(0,(char const *)file,flag,(void * const *)(__va_args));
- }
+ openat(0,(char const *)file,flag,3.0); /* openat_fallback_1 */
__retres = 0;
return __retres;
}
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 6a3b0b88b1d319fa010db5e21bd79015aaf7b9fd..c18613a1f186d64f915f9db8fa71177a824dcda7 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -81,7 +81,7 @@
[variadic] tests/known/printf.c:71: Warning:
Flag ' ' and conversion specififer x are not compatibles.
[variadic] tests/known/printf.c:71:
- Generic translation of call to variadic function.
+ Fallback translation of call printf to a call to the specialized version printf_fallback_1.
[variadic] tests/known/printf.c:74:
Translating call to printf to a call to the specialized version printf_va_27.
[variadic] tests/known/printf.c:75:
@@ -116,8 +116,11 @@
[eva] using specification for function printf_va_25
[eva] using specification for function printf_va_26
[kernel:annot:missing-spec] tests/known/printf.c:71: Warning:
- Neither code nor specification for function printf, generating default assigns from the prototype
-[eva] using specification for function printf
+ Neither code nor specification for function printf_fallback_1, generating default assigns from the prototype
+[eva] using specification for function printf_fallback_1
+[eva:invalid-assigns] tests/known/printf.c:71:
+ Completely invalid destination for assigns clause *(param1 + (0 ..)).
+ Ignoring.
[eva] using specification for function printf_va_27
[eva] using specification for function printf_va_28
[eva] done for function main
@@ -562,6 +565,15 @@ int printf_va_25(char const * restrict format, void *param0);
int printf_va_26(char const * restrict format, int param0, int param1,
int param2, unsigned int param3);
+/*@ assigns \result, *(param1 + (0 ..));
+ assigns \result
+ \from *(format + (0 ..)), *(param1 + (0 ..)), param0, param2;
+ assigns *(param1 + (0 ..))
+ \from *(format + (0 ..)), *(param1 + (0 ..)), param0, param2;
+ */
+int printf_fallback_1(char const * restrict format, unsigned int param0,
+ char *param1, int param2);
+
/*@ requires valid_read_nstring(param1, param0);
requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -644,14 +656,7 @@ int main(void)
printf("%c\n",(int)c); /* printf_va_24 */
printf("%p ",(void *)string); /* printf_va_25 */
printf("%d %*.*u\n",1,- (-1),2,ui); /* printf_va_26 */
- {
- unsigned int __va_arg0 = ui;
- char *__va_arg1 = string;
- int __va_arg2 = 42;
- void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
- printf("Hello %- 0+#20.10lx %% %s world %d !",
- (void * const *)(__va_args));
- }
+ printf("Hello %- 0+#20.10lx %% %s world %d !",ui,string,42); /* printf_fallback_1 */
char hashes[4] = {(char)'#', (char)'#', (char)'#', (char)'#'};
printf("%.*s",4,hashes); /* printf_va_27 */
printf("%.4s",hashes); /* printf_va_28 */
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index 02785d8ff3d6251f2f7f1ccd575e7861d9c50f33..c20bf567f1b4ab728d25c4bd5367fed1dd807dc2 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -23,14 +23,14 @@
[variadic] tests/known/printf_wrong_arity.c:9: Warning:
Not enough arguments: expected 3, given 2.
[variadic] tests/known/printf_wrong_arity.c:9:
- Generic translation of call to variadic function.
+ Fallback translation of call printf to a call to the specialized version printf_va_2_fallback_1.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function printf_va_1
[kernel:annot:missing-spec] tests/known/printf_wrong_arity.c:9: Warning:
- Neither code nor specification for function printf, generating default assigns from the prototype
-[eva] using specification for function printf
+ Neither code nor specification for function printf_va_2_fallback_1, generating default assigns from the prototype
+[eva] using specification for function printf_va_2_fallback_1
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -72,6 +72,10 @@ int printf_va_1(char const * restrict format, int param0);
*/
int printf_va_2(char const * restrict format, int param0, int param1);
+/*@ assigns \result;
+ assigns \result \from *(format + (0 ..)), param0; */
+int printf_va_2_fallback_1(char const * restrict format, int param0);
+
int main(void)
{
int __retres;
@@ -79,11 +83,7 @@ int main(void)
int tmp = 2;
printf("%d",1); /* printf_va_1 */
}
- {
- int __va_arg0 = 1;
- void *__va_args[1] = {& __va_arg0};
- printf("%d %d",(void * const *)(__va_args));
- }
+ printf("%d %d",1); /* printf_va_2_fallback_1 */
__retres = 0;
return __retres;
}
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
index d1eefe22d5db925f19fa564f707af18bab3f19e7..5195bdb7c25d106369eabb0dd894031e07d69bd5 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
@@ -18,27 +18,27 @@
Call to function fprintf with non-static format argument:
no specification will be generated.
[variadic] tests/known/stdio_print.c:9:
- Generic translation of call to variadic function.
+ Fallback translation of call fprintf to a call to the specialized version fprintf_fallback_1.
[variadic] tests/known/stdio_print.c:10: Warning:
Call to function printf with non-static format argument:
no specification will be generated.
[variadic] tests/known/stdio_print.c:10:
- Generic translation of call to variadic function.
+ Fallback translation of call printf to a call to the specialized version printf_fallback_1.
[variadic] tests/known/stdio_print.c:11: Warning:
Call to function snprintf with non-static format argument:
no specification will be generated.
[variadic] tests/known/stdio_print.c:11:
- Generic translation of call to variadic function.
+ Fallback translation of call snprintf to a call to the specialized version snprintf_fallback_1.
[variadic] tests/known/stdio_print.c:12: Warning:
Call to function sprintf with non-static format argument:
no specification will be generated.
[variadic] tests/known/stdio_print.c:12:
- Generic translation of call to variadic function.
+ Fallback translation of call sprintf to a call to the specialized version sprintf_fallback_1.
[variadic] tests/known/stdio_print.c:13: Warning:
Call to function dprintf with non-static format argument:
no specification will be generated.
[variadic] tests/known/stdio_print.c:13:
- Generic translation of call to variadic function.
+ Fallback translation of call dprintf to a call to the specialized version dprintf_fallback_1.
[variadic] tests/known/stdio_print.c:15:
Translating call to fprintf to a call to the specialized version fprintf_va_1.
[variadic] tests/known/stdio_print.c:16:
@@ -58,7 +58,7 @@
[eva] tests/known/stdio_print.c:9:
assertion 'Eva,initialization' got final status invalid.
[kernel:annot:missing-spec] tests/known/stdio_print.c:9: Warning:
- Neither code nor specification for function fprintf, generating default assigns from the prototype
+ Neither code nor specification for function fprintf_fallback_1, generating default assigns from the prototype
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
NON TERMINATING FUNCTION
@@ -67,6 +67,28 @@
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
+/*@ assigns \result, *stream;
+ assigns \result
+ \from *stream, *(format + (0 ..)), *(param1 + (0 ..)), param0, param2;
+ assigns *stream
+ \from *stream, *(format + (0 ..)), *(param1 + (0 ..)), param0, param2;
+ */
+int fprintf_fallback_1(FILE * restrict stream, char const * restrict format,
+ int param0, char const *param1, int param2);
+
+int printf_fallback_1(char const * restrict format, int param0,
+ char const *param1, int param2);
+
+int snprintf_fallback_1(char * restrict s, size_t n,
+ char const * restrict format, int param0,
+ char const *param1, int param2);
+
+int sprintf_fallback_1(char * restrict s, char const * restrict format,
+ int param0, char const *param1, int param2);
+
+int dprintf_fallback_1(int fd, char const * restrict format, int param0,
+ char const *param1, char const *param2);
+
/*@ requires valid_read_string(param1);
requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
@@ -148,42 +170,12 @@ int main(void)
char *format;
char *str;
size_t size;
- {
- int __va_arg0 = 1;
- char const *__va_arg1 = "2";
- int __va_arg2 = 3;
- void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
- /*@ assert Eva: initialization: \initialized(&format); */
- fprintf(stream,(char const *)format,(void * const *)(__va_args));
- }
- {
- int __va_arg0_10 = 1;
- char const *__va_arg1_12 = "2";
- int __va_arg2_14 = 3;
- void *__va_args_16[3] = {& __va_arg0_10, & __va_arg1_12, & __va_arg2_14};
- printf((char const *)format,(void * const *)(__va_args_16));
- }
- {
- int __va_arg0_18 = 1;
- char const *__va_arg1_20 = "2";
- int __va_arg2_22 = 3;
- void *__va_args_24[3] = {& __va_arg0_18, & __va_arg1_20, & __va_arg2_22};
- snprintf(str,size,(char const *)format,(void * const *)(__va_args_24));
- }
- {
- int __va_arg0_26 = 1;
- char const *__va_arg1_28 = "2";
- int __va_arg2_30 = 3;
- void *__va_args_32[3] = {& __va_arg0_26, & __va_arg1_28, & __va_arg2_30};
- sprintf(str,(char const *)format,(void * const *)(__va_args_32));
- }
- {
- int __va_arg0_34 = 1;
- char const *__va_arg1_36 = "3";
- char const *__va_arg2_38 = "4";
- void *__va_args_40[3] = {& __va_arg0_34, & __va_arg1_36, & __va_arg2_38};
- dprintf(1,(char const *)format,(void * const *)(__va_args_40));
- }
+ /*@ assert Eva: initialization: \initialized(&format); */
+ fprintf(stream,(char const *)format,1,"2",3); /* fprintf_fallback_1 */
+ printf((char const *)format,1,"2",3); /* printf_fallback_1 */
+ snprintf(str,size,(char const *)format,1,"2",3); /* snprintf_fallback_1 */
+ sprintf(str,(char const *)format,1,"2",3); /* sprintf_fallback_1 */
+ dprintf(1,(char const *)format,1,"3","4"); /* dprintf_fallback_1 */
fprintf(stream,"%d %s %d",1,(char *)"2",3); /* fprintf_va_1 */
printf("%d %s %d",1,(char *)"2",3); /* printf_va_1 */
snprintf(str,size,"%d %s %d",1,(char *)"2",3); /* snprintf_va_1 */
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
index 673cafd33f94eae29f7fae8d958841effcdd4a08..d1405ef465a47f1c679095e6dd6885a90ed63b87 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
@@ -18,17 +18,17 @@
Call to function fscanf with non-static format argument:
no specification will be generated.
[variadic] tests/known/stdio_scan.c:10:
- Generic translation of call to variadic function.
+ Fallback translation of call fscanf to a call to the specialized version fscanf_fallback_1.
[variadic] tests/known/stdio_scan.c:11: Warning:
Call to function scanf with non-static format argument:
no specification will be generated.
[variadic] tests/known/stdio_scan.c:11:
- Generic translation of call to variadic function.
+ Fallback translation of call scanf to a call to the specialized version scanf_fallback_1.
[variadic] tests/known/stdio_scan.c:12: Warning:
Call to function sscanf with non-static format argument:
no specification will be generated.
[variadic] tests/known/stdio_scan.c:12:
- Generic translation of call to variadic function.
+ Fallback translation of call sscanf to a call to the specialized version sscanf_fallback_1.
[variadic] tests/known/stdio_scan.c:14:
Translating call to fscanf to a call to the specialized version fscanf_va_1.
[variadic] tests/known/stdio_scan.c:15:
@@ -43,6 +43,8 @@
[eva] done for function main
[eva] tests/known/stdio_scan.c:10:
assertion 'Eva,initialization' got final status invalid.
+[kernel:annot:missing-spec] tests/known/stdio_scan.c:10: Warning:
+ Neither code nor specification for function fscanf_fallback_1, generating default assigns from the prototype
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
NON TERMINATING FUNCTION
@@ -51,6 +53,27 @@
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
+/*@ assigns \result, *stream, *param0, *(param1 + (0 ..)), *param2;
+ assigns \result
+ \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+ assigns *stream
+ \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+ assigns *param0
+ \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+ assigns *(param1 + (0 ..))
+ \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+ assigns *param2
+ \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+ */
+int fscanf_fallback_1(FILE * restrict stream, char const * restrict format,
+ int *param0, char *param1, int *param2);
+
+int scanf_fallback_1(char const * restrict format, int *param0, char *param1,
+ int *param2);
+
+int sscanf_fallback_1(char const * restrict s, char const * restrict format,
+ int *param0, char *param1, int *param2);
+
/*@ requires \valid(param0);
requires \valid(param2);
requires valid_read_string(format);
@@ -133,29 +156,10 @@ int main(void)
int i;
int j;
char *s;
- {
- int *__va_arg0 = & i;
- /*@ assert Eva: initialization: \initialized(&s); */
- char *__va_arg1 = s;
- int *__va_arg2 = & j;
- void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
- fscanf(stream,(char const *)format,(void * const *)(__va_args));
- }
- {
- int *__va_arg0_12 = & i;
- char *__va_arg1_14 = s;
- int *__va_arg2_16 = & j;
- void *__va_args_18[3] = {& __va_arg0_12, & __va_arg1_14, & __va_arg2_16};
- scanf((char const *)format,(void * const *)(__va_args_18));
- }
- {
- int *__va_arg0_20 = & i;
- char *__va_arg1_22 = s;
- int *__va_arg2_24 = & j;
- void *__va_args_26[3] = {& __va_arg0_20, & __va_arg1_22, & __va_arg2_24};
- sscanf((char const *)str,(char const *)format,
- (void * const *)(__va_args_26));
- }
+ /*@ assert Eva: initialization: \initialized(&s); */
+ fscanf(stream,(char const *)format,& i,s,& j); /* fscanf_fallback_1 */
+ scanf((char const *)format,& i,s,& j); /* scanf_fallback_1 */
+ sscanf((char const *)str,(char const *)format,& i,s,& j); /* sscanf_fallback_1 */
fscanf(stream,"%d %s %d",& i,s,& j); /* fscanf_va_1 */
scanf("%d %s %d",& i,s,& j); /* scanf_va_1 */
sscanf((char const *)str,"%d %s %d",& i,s,& j); /* sscanf_va_1 */