Skip to content

Commit 6a99d3b

Browse files
tautschnigtautschnig
committed
__builtin_*_overflow tests can be run on any platform
We just need to provide the declarations in case the underlying compiler isn't GCC.
1 parent 2a38a0c commit 6a99d3b

File tree

6 files changed

+67
-15
lines changed

6 files changed

+67
-15
lines changed

‎regression/cbmc/gcc_builtin_add_overflow/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,20 @@
11
#include <assert.h>
22
#include <limits.h>
33

4+
#ifndef __GNUC__
5+
_Bool __builtin_add_overflow();
6+
_Bool __builtin_add_overflow_p();
7+
_Bool __builtin_sadd_overflow(int, int, int *);
8+
_Bool __builtin_saddl_overflow(long, long, long *);
9+
_Bool __builtin_saddll_overflow(long long, long long, long long *);
10+
_Bool __builtin_uadd_overflow(unsigned int, unsigned int, unsigned int *);
11+
_Bool __builtin_uaddl_overflow(unsigned long, unsigned long, unsigned long *);
12+
_Bool __builtin_uaddll_overflow(
13+
unsigned long long,
14+
unsigned long long,
15+
unsigned long long *);
16+
#endif
17+
418
void check_int(void)
519
{
620
int const one = 1;

‎regression/cbmc/gcc_builtin_add_overflow/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE gcc-only
1+
CORE
22
main.c
33

44
\[check_int.assertion.1\] line \d+ assertion !__builtin_sadd_overflow\(one, one, &result\): SUCCESS

‎regression/cbmc/gcc_builtin_mul_overflow/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,20 @@
22
#include <limits.h>
33
#include <stdint.h>
44

5+
#ifndef __GNUC__
6+
_Bool __builtin_mul_overflow();
7+
_Bool __builtin_mul_overflow_p();
8+
_Bool __builtin_smul_overflow(int, int, int *);
9+
_Bool __builtin_smull_overflow(long, long, long *);
10+
_Bool __builtin_smulll_overflow(long long, long long, long long *);
11+
_Bool __builtin_umul_overflow(unsigned int, unsigned int, unsigned int *);
12+
_Bool __builtin_umull_overflow(unsigned long, unsigned long, unsigned long *);
13+
_Bool __builtin_umulll_overflow(
14+
unsigned long long,
15+
unsigned long long,
16+
unsigned long long *);
17+
#endif
18+
519
#define A_VALUE_X_SO_THAT_X_TIMES_X_DOES_NOT_OVERFLOW(T) \
620
(((T)(1)) << (sizeof(T) * CHAR_BIT) / 2 - 1)
721

‎regression/cbmc/gcc_builtin_mul_overflow/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE gcc-only
1+
CORE
22
main.c
33

44
\[check_int.assertion.1\] line \d+ assertion !__builtin_smul_overflow\(1, 1, &result\): SUCCESS

‎regression/cbmc/gcc_builtin_sub_overflow/main.c

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,20 @@
11
#include <assert.h>
22
#include <limits.h>
33

4+
#ifndef __GNUC__
5+
_Bool __builtin_sub_overflow();
6+
_Bool __builtin_sub_overflow_p();
7+
_Bool __builtin_ssub_overflow(int, int, int *);
8+
_Bool __builtin_ssubl_overflow(long, long, long *);
9+
_Bool __builtin_ssubll_overflow(long long, long long, long long *);
10+
_Bool __builtin_usub_overflow(unsigned int, unsigned int, unsigned int *);
11+
_Bool __builtin_usubl_overflow(unsigned long, unsigned long, unsigned long *);
12+
_Bool __builtin_usubll_overflow(
13+
unsigned long long,
14+
unsigned long long,
15+
unsigned long long *);
16+
#endif
17+
418
void check_int(void)
519
{
620
int result;
@@ -30,7 +44,16 @@ void check_long_long(void)
3044
assert(result == 0ll);
3145
assert(__builtin_ssubll_overflow(LLONG_MIN, 1ll, &result));
3246
assert(!__builtin_ssubll_overflow(LLONG_MIN / 2ll, LLONG_MAX / 2ll, &result));
47+
#if !defined(_WIN32) || defined(_WIN64)
48+
// Visual Studio x86/32 bit has an 8-byte "long long" type with corresponding
49+
// LLONG_MAX and LLONG_MIN constants (9223372036854775807i64 and
50+
// -9223372036854775807i64 - 1, respectively), but compiles these to 32-bit
51+
// values. The result is that -LLONG_MAX wraps around to the 32-bit value of
52+
// -LLONG_MIN (-2147483648), with the consequence that result == LLONG_MIN
53+
// after the above subtraction. Therefore, disable this assertion on Visual
54+
// Studio x86/32 bit.
3355
assert(result - 1ll == LLONG_MIN);
56+
#endif
3457
assert(0 && "reachability");
3558
}
3659

‎regression/cbmc/gcc_builtin_sub_overflow/test.desc

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE gcc-only
1+
CORE
22
main.c
33

44
\[check_int.assertion.1\] line \d+ assertion !__builtin_ssub_overflow\(1, 1, &result\): SUCCESS
@@ -17,8 +17,7 @@ main.c
1717
\[check_long_long.assertion.2\] line \d+ assertion result == 0ll: SUCCESS
1818
\[check_long_long.assertion.3\] line \d+ assertion __builtin_ssubll_overflow\(.*, 1ll, &result\): SUCCESS
1919
\[check_long_long.assertion.4\] line \d+ assertion !__builtin_ssubll_overflow\(.* / 2ll, .* / 2ll, &result\): SUCCESS
20-
\[check_long_long.assertion.5\] line \d+ assertion result - 1ll == .*: SUCCESS
21-
\[check_long_long.assertion.6\] line \d+ assertion 0 && "reachability": FAILURE
20+
\[check_long_long.assertion.[56]\] line \d+ assertion 0 && "reachability": FAILURE
2221
\[check_unsigned.assertion.1\] line \d+ assertion !__builtin_usub_overflow\(1u, 1u, &result\): SUCCESS
2322
\[check_unsigned.assertion.2\] line \d+ assertion result == 0u: SUCCESS
2423
\[check_unsigned.assertion.3\] line \d+ assertion __builtin_usub_overflow\(0u, 1u, &result\): SUCCESS
@@ -40,15 +39,17 @@ main.c
4039
\[check_unsigned_long_long.assertion.5\] line \d+ assertion result == 0ull: SUCCESS
4140
\[check_unsigned_long_long.assertion.6\] line \d+ assertion __builtin_usubll_overflow\(.* / 2ull, .*, &result\): SUCCESS
4241
\[check_unsigned_long_long.assertion.7\] line \d+ assertion 0 && "reachability": FAILURE
43-
\[check_generic.assertion.1\] line 79 assertion __builtin_sub_overflow\(5, 10, &small_result\): SUCCESS
44-
\[check_generic.assertion.2\] line 80 assertion !__builtin_sub_overflow\(5, 10, &big_result\): SUCCESS
45-
\[check_generic.assertion.3\] line 81 assertion big_result == -5ll: SUCCESS
46-
\[check_generic.assertion.4\] line 82 assertion !__builtin_sub_overflow\(10, 5, &small_result\): SUCCESS
47-
\[check_generic.assertion.5\] line 83 assertion small_result == 5: SUCCESS
48-
\[check_generic.assertion.6\] line 84 assertion !__builtin_sub_overflow\(10, 5, &big_result\): SUCCESS
49-
\[check_generic.assertion.7\] line 85 assertion big_result == 5ll: SUCCESS
50-
\[check_generic.assertion.8\] line 86 assertion !__builtin_sub_overflow\(.*, .*, &big_result\): SUCCESS
51-
\[check_generic.assertion.9\] line 87 assertion big_result == 2ll \* .* \+ 1: SUCCESS
52-
\[check_generic.assertion.10\] line 88 assertion 0 && "reachability": FAILURE
42+
\[check_generic.assertion.1\] line 102 assertion __builtin_sub_overflow\(5, 10, &small_result\): SUCCESS
43+
\[check_generic.assertion.2\] line 103 assertion !__builtin_sub_overflow\(5, 10, &big_result\): SUCCESS
44+
\[check_generic.assertion.3\] line 104 assertion big_result == -5ll: SUCCESS
45+
\[check_generic.assertion.4\] line 105 assertion !__builtin_sub_overflow\(10, 5, &small_result\): SUCCESS
46+
\[check_generic.assertion.5\] line 106 assertion small_result == 5: SUCCESS
47+
\[check_generic.assertion.6\] line 107 assertion !__builtin_sub_overflow\(10, 5, &big_result\): SUCCESS
48+
\[check_generic.assertion.7\] line 108 assertion big_result == 5ll: SUCCESS
49+
\[check_generic.assertion.8\] line 109 assertion !__builtin_sub_overflow\(.*, .*, &big_result\): SUCCESS
50+
\[check_generic.assertion.9\] line 110 assertion big_result == 2ll \* .* \+ 1: SUCCESS
51+
\[check_generic.assertion.10\] line 111 assertion 0 && "reachability": FAILURE
5352
^EXIT=10$
5453
^SIGNAL=0$
54+
--
55+
\[check_long_long.assertion.5\] line \d+ assertion result - 1ll == .*: FAILURE

0 commit comments

Comments
 (0)