From 5b2a4c723fab4007b6769a5fc0dcf1782398e2a7 Mon Sep 17 00:00:00 2001
From: Henrich Lauko <xlauko@mail.muni.cz>
Date: Thu, 10 Oct 2019 10:16:20 +0000
Subject: [PATCH] test: Add bunch of abstract unit aggregate tests.

---
 test/abstract/unit-aggr-call-a.cpp  | 17 +++++++++++++++++
 test/abstract/unit-aggr-call-b.cpp  | 22 ++++++++++++++++++++++
 test/abstract/unit-aggr-load-a.cpp  | 11 +++++++++++
 test/abstract/unit-aggr-load-b.cpp  | 12 ++++++++++++
 test/abstract/unit-aggr-load-c.cpp  | 13 +++++++++++++
 test/abstract/unit-aggr-store-a.cpp | 12 ++++++++++++
 test/abstract/unit-aggr-store-b.cpp | 14 ++++++++++++++
 test/abstract/unit-aggr-store-c.cpp | 12 ++++++++++++
 8 files changed, 113 insertions(+)
 create mode 100644 test/abstract/unit-aggr-call-a.cpp
 create mode 100644 test/abstract/unit-aggr-call-b.cpp
 create mode 100644 test/abstract/unit-aggr-load-a.cpp
 create mode 100644 test/abstract/unit-aggr-load-b.cpp
 create mode 100644 test/abstract/unit-aggr-load-c.cpp
 create mode 100644 test/abstract/unit-aggr-store-a.cpp
 create mode 100644 test/abstract/unit-aggr-store-b.cpp
 create mode 100644 test/abstract/unit-aggr-store-c.cpp

diff --git a/test/abstract/unit-aggr-call-a.cpp b/test/abstract/unit-aggr-call-a.cpp
new file mode 100644
index 000000000..67ba03fa7
--- /dev/null
+++ b/test/abstract/unit-aggr-call-a.cpp
@@ -0,0 +1,17 @@
+/* TAGS: star min */
+/* VERIFY_OPTS: --symbolic -o nofail:malloc */
+
+#include <rst/domains.h>
+
+#include <cassert>
+
+char * store_ten( char * aggr ) {
+    auto idx = __unit_val_i64();
+    aggr[idx] = 10;
+    return aggr;
+}
+
+int main() {
+    auto aggr = static_cast< char * >( __unit_aggregate() );
+    auto res = store_ten( aggr );
+}
diff --git a/test/abstract/unit-aggr-call-b.cpp b/test/abstract/unit-aggr-call-b.cpp
new file mode 100644
index 000000000..fe38a891d
--- /dev/null
+++ b/test/abstract/unit-aggr-call-b.cpp
@@ -0,0 +1,22 @@
+/* TAGS: star min */
+/* VERIFY_OPTS: --symbolic -o nofail:malloc */
+
+#include <rst/domains.h>
+
+#include <cassert>
+
+char * store_value( char * aggr ) {
+    auto val = __unit_val_i8();
+    aggr[5] = val;
+    return aggr;
+}
+
+int main() {
+    auto aggr = static_cast< char * >( __unit_aggregate() );
+    auto res = store_value( aggr );
+
+    char arr[ 10 ] = {};
+    auto concrete = store_value( arr );
+    assert( concrete[ 0 ] == 0 );
+    assert( arr[ 5 ] ); /* ERROR */
+}
diff --git a/test/abstract/unit-aggr-load-a.cpp b/test/abstract/unit-aggr-load-a.cpp
new file mode 100644
index 000000000..15a5b0886
--- /dev/null
+++ b/test/abstract/unit-aggr-load-a.cpp
@@ -0,0 +1,11 @@
+/* TAGS: star min */
+/* VERIFY_OPTS: --symbolic -o nofail:malloc */
+
+#include <rst/domains.h>
+
+#include <cassert>
+
+int main() {
+    auto aggr = static_cast< char * >( __unit_aggregate() );
+    auto c = aggr[6];
+}
diff --git a/test/abstract/unit-aggr-load-b.cpp b/test/abstract/unit-aggr-load-b.cpp
new file mode 100644
index 000000000..cc72565ae
--- /dev/null
+++ b/test/abstract/unit-aggr-load-b.cpp
@@ -0,0 +1,12 @@
+/* TAGS: star min */
+/* VERIFY_OPTS: --symbolic -o nofail:malloc */
+
+#include <rst/domains.h>
+
+#include <cassert>
+
+int main() {
+    auto aggr = static_cast< char * >( __unit_aggregate() );
+    auto idx = __unit_val_i64();
+    auto c = aggr[idx];
+}
diff --git a/test/abstract/unit-aggr-load-c.cpp b/test/abstract/unit-aggr-load-c.cpp
new file mode 100644
index 000000000..ff087f101
--- /dev/null
+++ b/test/abstract/unit-aggr-load-c.cpp
@@ -0,0 +1,13 @@
+/* TAGS: star min */
+/* VERIFY_OPTS: --symbolic -o nofail:malloc */
+
+#include <rst/domains.h>
+
+#include <cassert>
+
+int main() {
+    auto aggr = static_cast< char * >( __unit_aggregate() );
+    auto idx = __unit_val_i64();
+    auto c = aggr[idx];
+    assert( c ); /* ERROR */
+}
diff --git a/test/abstract/unit-aggr-store-a.cpp b/test/abstract/unit-aggr-store-a.cpp
new file mode 100644
index 000000000..785e6bc18
--- /dev/null
+++ b/test/abstract/unit-aggr-store-a.cpp
@@ -0,0 +1,12 @@
+/* TAGS: star min */
+/* VERIFY_OPTS: --symbolic -o nofail:malloc */
+
+#include <rst/domains.h>
+
+#include <cassert>
+
+int main() {
+    auto val = __unit_val_i8();
+    auto aggr = static_cast< char * >( __unit_aggregate() );
+    aggr[5] = val;
+}
diff --git a/test/abstract/unit-aggr-store-b.cpp b/test/abstract/unit-aggr-store-b.cpp
new file mode 100644
index 000000000..90b3271d0
--- /dev/null
+++ b/test/abstract/unit-aggr-store-b.cpp
@@ -0,0 +1,14 @@
+/* TAGS: star min */
+/* VERIFY_OPTS: --symbolic -o nofail:malloc */
+
+#include <rst/domains.h>
+
+#include <cassert>
+
+int main() {
+    auto val = __unit_val_i8();
+    auto idx = __unit_val_i64();
+    auto aggr = static_cast< char * >( __unit_aggregate() );
+    aggr[idx] = val;
+}
+
diff --git a/test/abstract/unit-aggr-store-c.cpp b/test/abstract/unit-aggr-store-c.cpp
new file mode 100644
index 000000000..bcb29f627
--- /dev/null
+++ b/test/abstract/unit-aggr-store-c.cpp
@@ -0,0 +1,12 @@
+/* TAGS: star min */
+/* VERIFY_OPTS: --symbolic -o nofail:malloc */
+
+#include <rst/domains.h>
+
+#include <cassert>
+
+int main() {
+    auto aggr = static_cast< char * >( __unit_aggregate() );
+    auto idx = __unit_val_i64();
+    aggr[idx] = 10;
+}
-- 
GitLab