From c6b7b94ababf101ff87ba6bf8adc549f5c26730f Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 12 Jun 2020 16:17:47 +0200
Subject: [PATCH] [tests] performance tests for parsing concatenated strings

---
 tests/syntax/oracle/string_concat.res.oracle  | 27 +++++++++++++++++++
 tests/syntax/oracle/wstring_concat.res.oracle | 27 +++++++++++++++++++
 tests/syntax/string_concat.c                  | 17 ++++++++++++
 tests/syntax/wstring_concat.c                 | 17 ++++++++++++
 4 files changed, 88 insertions(+)
 create mode 100644 tests/syntax/oracle/string_concat.res.oracle
 create mode 100644 tests/syntax/oracle/wstring_concat.res.oracle
 create mode 100644 tests/syntax/string_concat.c
 create mode 100644 tests/syntax/wstring_concat.c

diff --git a/tests/syntax/oracle/string_concat.res.oracle b/tests/syntax/oracle/string_concat.res.oracle
new file mode 100644
index 00000000000..53ba826eece
--- /dev/null
+++ b/tests/syntax/oracle/string_concat.res.oracle
@@ -0,0 +1,27 @@
+[kernel] Parsing tests/syntax/string_concat.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  test[0..65535] ∈ {97}
+      [65536] ∈ {0}
+[eva] using specification for function printf_va_1
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __retres ∈ {0}
+  S___fc_stdout[0..1] ∈ [--..--]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 4 statements reached (out of 4): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Preconditions     2 valid     0 unknown     0 invalid      2 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
diff --git a/tests/syntax/oracle/wstring_concat.res.oracle b/tests/syntax/oracle/wstring_concat.res.oracle
new file mode 100644
index 00000000000..c83c532eda2
--- /dev/null
+++ b/tests/syntax/oracle/wstring_concat.res.oracle
@@ -0,0 +1,27 @@
+[kernel] Parsing tests/syntax/wstring_concat.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  test[0..65535] ∈ {97}
+      [65536] ∈ {0}
+[eva] using specification for function printf_va_1
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __retres ∈ {0}
+  S___fc_stdout[0..1] ∈ [--..--]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 4 statements reached (out of 4): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Preconditions     2 valid     0 unknown     0 invalid      2 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
diff --git a/tests/syntax/string_concat.c b/tests/syntax/string_concat.c
new file mode 100644
index 00000000000..9669f9687ef
--- /dev/null
+++ b/tests/syntax/string_concat.c
@@ -0,0 +1,17 @@
+/* run.config*
+TIMEOUT: 45s
+OPT: -eva
+*/
+
+#include <string.h>
+#include <stdio.h>
+
+#define d(a) a a
+#define dd(a) d(d(a))
+#define ddd(a) dd(dd(a))
+#define dddd(a) ddd(ddd(a))
+#define ddddd(a) dddd(dddd(a))
+
+const char test[] = ddddd("a");
+
+int main() { printf("length: %zu\n",strlen(test)); }
diff --git a/tests/syntax/wstring_concat.c b/tests/syntax/wstring_concat.c
new file mode 100644
index 00000000000..86d7d3ff4ea
--- /dev/null
+++ b/tests/syntax/wstring_concat.c
@@ -0,0 +1,17 @@
+/* run.config*
+TIMEOUT: 45s
+OPT: -eva
+*/
+
+#include <wchar.h>
+#include <stdio.h>
+
+#define d(a) a a
+#define dd(a) d(d(a))
+#define ddd(a) dd(dd(a))
+#define dddd(a) ddd(ddd(a))
+#define ddddd(a) dddd(dddd(a))
+
+const wchar_t test[] = ddddd(L"a");
+
+int main() { printf("length: %zu\n",wcslen(test)); }
-- 
GitLab