Skip to content

Commit abdf497

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 0bbfc31 commit abdf497

File tree

6 files changed

+55
-13
lines changed

6 files changed

+55
-13
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: 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_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;

‎regression/cbmc/gcc_builtin_sub_overflow/test.desc

Lines changed: 11 additions & 11 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
@@ -40,15 +40,15 @@ main.c
4040
\[check_unsigned_long_long.assertion.5\] line \d+ assertion result == 0ull: SUCCESS
4141
\[check_unsigned_long_long.assertion.6\] line \d+ assertion __builtin_usubll_overflow\(.* / 2ull, .*, &result\): SUCCESS
4242
\[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
43+
\[check_generic.assertion.1\] line 93 assertion __builtin_sub_overflow\(5, 10, &small_result\): SUCCESS
44+
\[check_generic.assertion.2\] line 94 assertion !__builtin_sub_overflow\(5, 10, &big_result\): SUCCESS
45+
\[check_generic.assertion.3\] line 95 assertion big_result == -5ll: SUCCESS
46+
\[check_generic.assertion.4\] line 96 assertion !__builtin_sub_overflow\(10, 5, &small_result\): SUCCESS
47+
\[check_generic.assertion.5\] line 97 assertion small_result == 5: SUCCESS
48+
\[check_generic.assertion.6\] line 98 assertion !__builtin_sub_overflow\(10, 5, &big_result\): SUCCESS
49+
\[check_generic.assertion.7\] line 99 assertion big_result == 5ll: SUCCESS
50+
\[check_generic.assertion.8\] line 100 assertion !__builtin_sub_overflow\(.*, .*, &big_result\): SUCCESS
51+
\[check_generic.assertion.9\] line 101 assertion big_result == 2ll \* .* \+ 1: SUCCESS
52+
\[check_generic.assertion.10\] line 102 assertion 0 && "reachability": FAILURE
5353
^EXIT=10$
5454
^SIGNAL=0$

0 commit comments

Comments
 (0)