From 5bf545f81182f8e36124309af57a58cd1678f704 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 6 Mar 2024 10:43:43 +0100
Subject: [PATCH] [tests] add test checking that variadic does generate fresh
names
---
.../oracle/variadic_fresh_names.res.oracle | 39 +++++++++++++++++++
tests/syntax/variadic_fresh_names.c | 24 ++++++++++++
2 files changed, 63 insertions(+)
create mode 100644 tests/syntax/oracle/variadic_fresh_names.res.oracle
create mode 100644 tests/syntax/variadic_fresh_names.c
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 00000000000..1fb230dff45
--- /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 00000000000..46615262b2d
--- /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;
+}
--
GitLab