Skip to content

Commit ba7eb04

Browse files
committed
Tests: do not hard-code 64 bits/8 bytes as pointer width
This wouldn't be true for all platforms.
1 parent 0723271 commit ba7eb04

File tree

2 files changed

+18
-2
lines changed

2 files changed

+18
-2
lines changed

regression/cbmc/assigning_nullpointers_should_not_crash_symex/main.c

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,19 @@ struct linked_list
66
struct linked_list *next;
77
};
88

9+
#ifdef _WIN32
10+
# ifdef _M_X64
11+
# define POINTER_BYTES 8ul
12+
# else
13+
# define POINTER_BYTES 4ul
14+
# endif
15+
#else
16+
# define POINTER_BYTES __SIZEOF_POINTER__
17+
#endif
18+
919
int main(void)
1020
{
11-
size_t list_sz = 8ul;
21+
size_t list_sz = POINTER_BYTES;
1222
assert(list_sz == sizeof(struct linked_list));
1323
struct linked_list *list = malloc(list_sz);
1424
// this line makes symex crash for some reason

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,16 @@
66
#include <stdint.h>
77

88
extern size_t __CPROVER_max_malloc_size;
9-
int __builtin_clzll(unsigned long long);
109

10+
#if defined(_WIN32) && defined(_M_X64)
11+
int __builtin_clzll(unsigned long long);
1112
#define __nof_symex_objects \
1213
((size_t)(1ULL << __builtin_clzll(__CPROVER_max_malloc_size)))
14+
#else
15+
int __builtin_clzl(unsigned long);
16+
#define __nof_symex_objects \
17+
((size_t)(1UL << __builtin_clzl(__CPROVER_max_malloc_size)))
18+
#endif
1319

1420
typedef struct {
1521
size_t k;

0 commit comments

Comments
 (0)