diff --git a/tests/syntax/oracle/variadic_fresh_names.res.oracle b/tests/syntax/oracle/variadic_fresh_names.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1fb230dff45abd65517f9051ac02522c249c33fa
--- /dev/null
+++ b/tests/syntax/oracle/variadic_fresh_names.res.oracle
@@ -0,0 +1,39 @@
+[kernel] Parsing variadic_fresh_names.c (with preprocessing)
+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
+/*@ requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..))), param0;
+ */
+int fprintf_va_1(FILE * restrict stream, char const * restrict format,
+                 int param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..))), param0;
+ */
+int fprintf_va_2(FILE * restrict stream, char const * restrict format,
+                 int param0);
+
+void main(void)
+{
+  fprintf(__fc_stderr,"%d ",42); /* fprintf_va_2 */
+  return;
+}
+
+
diff --git a/tests/syntax/variadic_fresh_names.c b/tests/syntax/variadic_fresh_names.c
new file mode 100644
index 0000000000000000000000000000000000000000..46615262b2d8bdc38fdafb9b32a4b4b5a65296fa
--- /dev/null
+++ b/tests/syntax/variadic_fresh_names.c
@@ -0,0 +1,24 @@
+/* run.config
+PLUGIN: variadic
+STDOPT:
+*/
+#include "stdio.h"
+
+/*@ requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..))), param0;
+ */
+int fprintf_va_1(FILE * restrict stream, char const * restrict format,
+                 int param0);
+
+void main(void)
+{
+  fprintf(__fc_stderr,"%d ",42); /* fprintf_va_1 */
+  return;
+}