1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
/*******************************************************************\
Module: Unit test for max_malloc_size
Author: Thomas Kiley
\*******************************************************************/
#include <util/config.h>
#include <testing-utils/use_catch.h>
TEST_CASE("max_malloc_size", "[core][util][config][max_malloc_size]")
{
cbmc_invariants_should_throwt throw_invariants;
configt config_backup = config;
SECTION("Too many bits for pointer ID")
{
config.ansi_c.pointer_width = 4;
config.bv_encoding.object_bits = 4;
REQUIRE_THROWS_AS(config.max_malloc_size(), invariant_failedt);
config.bv_encoding.object_bits = 5;
REQUIRE_THROWS_AS(config.max_malloc_size(), invariant_failedt);
}
SECTION("Not enough bits for pointer ID")
{
config.ansi_c.pointer_width = 4;
config.bv_encoding.object_bits = 0;
REQUIRE_THROWS_AS(config.max_malloc_size(), invariant_failedt);
}
SECTION("Not enough bits in the pointer")
{
config.ansi_c.pointer_width = 0;
config.bv_encoding.object_bits = 0;
REQUIRE_THROWS_AS(config.max_malloc_size(), invariant_failedt);
}
SECTION("Valid allocation size configurations")
{
// The one bit offset can be used to store 0, or -1, so we can allocate
// a single bit
config.ansi_c.pointer_width = 4;
config.bv_encoding.object_bits = 3;
REQUIRE(config.max_malloc_size() == 1);
// Here we use 4 bits for the object ID, leaving 3 for the offset
config.ansi_c.pointer_width = 8;
config.bv_encoding.object_bits = 4;
REQUIRE(config.max_malloc_size() == 8);
config.ansi_c.pointer_width = 128;
config.bv_encoding.object_bits = 64;
REQUIRE(config.max_malloc_size() == 9223372036854775808ull /*2^63*/);
config.bv_encoding.object_bits = 63;
REQUIRE(
config.max_malloc_size() == string2integer("18446744073709551616"
/*2^64*/));
}
std::swap(config_backup, config);
}
|
