From e1e2fb0df32c15a804ab64a525d5f62c68deef57 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Tue, 4 May 2021 17:45:21 +0200 Subject: [PATCH] [tests] add test case for very large integers --- tests/syntax/very_large_integers.c | 73 ++++++++++++++++++++++++++++++ 1 file changed, 73 insertions(+) create mode 100644 tests/syntax/very_large_integers.c diff --git a/tests/syntax/very_large_integers.c b/tests/syntax/very_large_integers.c new file mode 100644 index 00000000000..8c6bac17a68 --- /dev/null +++ b/tests/syntax/very_large_integers.c @@ -0,0 +1,73 @@ +/* run.config + EXIT: 1 + STDOPT: #"-cpp-extra-args=-DBITFIELD" + STDOPT: #"-cpp-extra-args=-DARRAY_DECL" + STDOPT: #"-cpp-extra-args=-DCASE_RANGE" + STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR" + STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR2" + STDOPT: #"-cpp-extra-args=-DRANGE_DESIGNATOR" + STDOPT: #"-cpp-extra-args=-DATTRIBUTE_CONSTANT" + STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva" + STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA" +*/ +volatile int nondet; + +#ifdef BITFIELD +struct st { + int bf:(999999999999999999+9999999999999999999); +}; +#endif + +#ifdef ARRAY_DECL +int arr[9999999999999999999U+18000000000000000000U]; +char arr1[99999999999999999999U]; +#endif +#ifdef CASE_RANGE +unsigned long nondetul; +void case_range() { + switch (nondetul) + case 0 ... 9999999999999999999U:; +} +#endif + +#ifdef INIT_DESIGNATOR +int arr2[9999999999999999999U] = { [9999999999999999999U] = 42 }; +#endif + +#ifdef INIT_DESIGNATOR2 +int arr3[1] = { [9999999999999999999U] = 42 }; +#endif + +#ifdef RANGE_DESIGNATOR +int arr4[1] = { [-9999999999999999999U ... 9999999999999999999U] = 42 }; +#endif + +#ifdef ATTRIBUTE_CONSTANT +struct acst { + int a __attribute__((aligned(0x80000000000000000))); +}; +#endif + +typedef struct { + char a; + int b __attribute__((aligned(0x8000000000000000))); + double c __attribute__((aligned(0x8000000000000000+0x8000000000000000))); +} stt ; + +//@ logic integer too_large_integer = 9999999999999999999; + +int main() { +#ifdef EVA_UNROLL + //@ loop unroll (-9999999999999999999); // IntLimit + while (nondet); + //@ loop unroll too_large_integer; // ExpLimit + while (nondet); + //@ slevel 9999999999999999999; + while (nondet); +#endif +#ifdef UNROLL_PRAGMA + //@ loop pragma UNROLL 99999999999999999999; +#endif + while (nondet); + return 0; +} -- GitLab