test: Add bunch of abstract unit aggregate tests.

test/abstract/unit-aggr-call-a.cpp

+/* 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 );
+}

test/abstract/unit-aggr-call-b.cpp

+/* 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 */
+}

test/abstract/unit-aggr-load-a.cpp

+/* 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];
+}

test/abstract/unit-aggr-load-b.cpp

+/* 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];
+}

test/abstract/unit-aggr-load-c.cpp

+/* 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 */
+}

test/abstract/unit-aggr-store-a.cpp

+/* 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;
+}

test/abstract/unit-aggr-store-b.cpp

+/* 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;
+}
+

test/abstract/unit-aggr-store-c.cpp

+/* 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;
+}