From aa8829f66b18344c41fe6cf1bf8fa974d7cdbd1a Mon Sep 17 00:00:00 2001
From: Pierre Nigron <pierre.nigron@cea.fr>
Date: Tue, 22 Aug 2023 14:14:38 +0200
Subject: [PATCH] Tests + Oracles
---
tests/syntax/init_call_ko.c | 15 ++++++++++++
tests/syntax/init_call_ok.c | 22 +++++++++++++++++
tests/syntax/oracle/init_call_ko.res.oracle | 18 ++++++++++++++
tests/syntax/oracle/init_call_ok.res.oracle | 27 +++++++++++++++++++++
4 files changed, 82 insertions(+)
create mode 100644 tests/syntax/init_call_ko.c
create mode 100644 tests/syntax/init_call_ok.c
create mode 100644 tests/syntax/oracle/init_call_ko.res.oracle
create mode 100644 tests/syntax/oracle/init_call_ok.res.oracle
diff --git a/tests/syntax/init_call_ko.c b/tests/syntax/init_call_ko.c
new file mode 100644
index 00000000000..644ad18bd76
--- /dev/null
+++ b/tests/syntax/init_call_ko.c
@@ -0,0 +1,15 @@
+/* run.config
+ EXIT: 1
+ STDOPT:
+*/
+char *b(char* c){ return c; }
+
+int main(void) {
+ char a[] = b("");
+ char m[] = 1;
+ char p[1] = 0;
+ extern char j[] = {0,1};
+ char f[];
+ static char n[];
+ return 0;
+}
diff --git a/tests/syntax/init_call_ok.c b/tests/syntax/init_call_ok.c
new file mode 100644
index 00000000000..c544f666d23
--- /dev/null
+++ b/tests/syntax/init_call_ok.c
@@ -0,0 +1,22 @@
+/* run.config
+ EXIT: 0
+ STDOPT:
+*/
+int h(void);
+
+char g[];
+char* z(void);
+
+int main(void) {
+ char c[] = {0,1};
+ char d[] = {h()};
+ char e[] = "abcd";
+ static char l[2];
+ static char i[] = {0,1};
+ extern char k[];
+ struct {
+ int A[sizeof(char[8])];
+ int i;
+ } A = { h(), 2, 3, 4, 5, 6, 7, 8, 9 };
+ return 0;
+}
diff --git a/tests/syntax/oracle/init_call_ko.res.oracle b/tests/syntax/oracle/init_call_ko.res.oracle
new file mode 100644
index 00000000000..8db6a89d8e2
--- /dev/null
+++ b/tests/syntax/oracle/init_call_ko.res.oracle
@@ -0,0 +1,18 @@
+[kernel] Parsing init_call_ko.c (with preprocessing)
+[kernel] init_call_ko.c:8: User Error:
+ Array initializer must be an initializer list or string literal
+[kernel:typing:int-conversion] init_call_ko.c:8: Warning:
+ Conversion from a pointer to an integer without an explicit cast
+[kernel] init_call_ko.c:9: User Error:
+ Array initializer must be an initializer list or string literal
+[kernel] init_call_ko.c:10: User Error:
+ Array initializer must be an initializer list or string literal
+[kernel] init_call_ko.c:11: User Error:
+ 'extern' variable cannot have an initializer
+[kernel] init_call_ko.c:12: User Error:
+ variable f with array type needs an explicit size or an initializer
+[kernel] init_call_ko.c:13: User Error:
+ variable n with array type needs an explicit size or an initializer
+[kernel] User Error: stopping on file "init_call_ko.c" that has errors. Add '-kernel-msg-key pp'
+ for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/init_call_ok.res.oracle b/tests/syntax/oracle/init_call_ok.res.oracle
new file mode 100644
index 00000000000..7022d5eea88
--- /dev/null
+++ b/tests/syntax/oracle/init_call_ok.res.oracle
@@ -0,0 +1,27 @@
+[kernel] Parsing init_call_ok.c (with preprocessing)
+/* Generated by Frama-C */
+struct __anonstruct_A_1 {
+ int A[sizeof(char [8])] ;
+ int i ;
+};
+int h(void);
+
+char g[];
+int main(void);
+
+int main(void)
+{
+ int __retres;
+ int tmp;
+ int tmp_0;
+ char c[2] = {(char)0, (char)1};
+ tmp = h();
+ char d[1] = {(char)tmp};
+ char e[5] = {(char)'a', (char)'b', (char)'c', (char)'d', (char)'\000'};
+ tmp_0 = h();
+ struct __anonstruct_A_1 A = {.A = {tmp_0, 2, 3, 4, 5, 6, 7, 8}, .i = 9};
+ __retres = 0;
+ return __retres;
+}
+
+
--
GitLab