diff --git a/test/abstract/unit-aggr-call-a.cpp b/test/abstract/unit-aggr-call-a.cpp new file mode 100644 index 0000000000000000000000000000000000000000..67ba03fa75b6a50bdab3360a3ee00ad1a3e6dd78 --- /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 0000000000000000000000000000000000000000..fe38a891d4a5f466ee370cc1ecc833559c1aea49 --- /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 0000000000000000000000000000000000000000..15a5b088636564adb1afac05b144836bc8ae22d7 --- /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 0000000000000000000000000000000000000000..cc72565ae5dc677505fee71a0f36d10d72fc0b54 --- /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 0000000000000000000000000000000000000000..ff087f101439c2b3a946359c118281e6328eb860 --- /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 0000000000000000000000000000000000000000..785e6bc186fdc6038682cd04a036eb5bf4e0c82b --- /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 0000000000000000000000000000000000000000..90b3271d05831e5805581d2c3f3fa2080850364f --- /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 0000000000000000000000000000000000000000..bcb29f627b067d2d4ce2b1e19e0d6f247a89a715 --- /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; +}