cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
alignment_checks.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Alignment Checks
4
5
Author:
6
7
\*******************************************************************/
8
11
12
#include "
alignment_checks.h
"
13
14
#include <
util/config.h
>
15
#include <
util/namespace.h
>
16
#include <
util/pointer_offset_size.h
>
17
#include <
util/std_types.h
>
18
#include <
util/symbol_table_base.h
>
19
20
#include <ostream>
21
22
void
print_struct_alignment_problems
(
23
const
symbol_table_baset
&symbol_table,
24
std::ostream &out)
25
{
26
for
(
const
auto
&symbol_pair : symbol_table.
symbols
)
27
{
28
if
(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
29
{
30
const
struct_typet
&str =
to_struct_type
(symbol_pair.second.type);
31
const
struct_typet::componentst
&components = str.
components
();
32
33
bool
first_time_seen_in_struct =
true
;
34
35
for
(struct_typet::componentst::const_iterator it_mem = components.begin();
36
it_mem != components.end();
37
it_mem++)
38
{
39
mp_integer
cumulated_length = 0;
40
bool
first_time_seen_from =
true
;
41
42
// if the instruction cannot be aligned to the address,
43
// try the next one
44
45
if
(it_mem->get_is_padding())
46
// || alignment(it_mem->type())%config.ansi_c.alignment!=0)
47
continue
;
48
49
for
(struct_typet::componentst::const_iterator it_next = it_mem;
50
it_next != components.end();
51
it_next++)
52
{
53
const
typet
&it_type = it_next->type();
54
const
namespacet
ns(symbol_table);
55
auto
size =
pointer_offset_size
(it_type, ns);
56
57
if
(!size.has_value())
58
throw
"type of unknown size:\n"
+ it_type.
pretty
();
59
60
cumulated_length += *size;
61
// [it_mem;it_next] cannot be covered by an instruction
62
if
(cumulated_length >
config
.ansi_c.memory_operand_size)
63
{
64
// if interferences have been found, no need to check with
65
// starting from an already covered member
66
if
(!first_time_seen_from)
67
it_mem = it_next - 1;
68
break
;
69
}
70
71
if
(it_mem != it_next && !it_next->get_is_padding())
72
{
73
if
(first_time_seen_in_struct)
74
{
75
first_time_seen_in_struct =
false
;
76
first_time_seen_from =
false
;
77
78
out <<
"\nWARNING: "
79
<<
"declaration of structure "
80
<< str.
find_type
(ID_tag).
pretty
() <<
" at "
81
<< symbol_pair.second.location <<
'\n'
;
82
}
83
84
out <<
"members "
<< it_mem->get_name() <<
" and "
85
<< it_next->get_name() <<
" might interfere\n"
;
86
}
87
}
88
}
89
}
90
else
if
(symbol_pair.second.type.id() == ID_array)
91
{
92
// is this structure likely to introduce data races?
93
#if 0
94
const
namespacet
ns(symbol_table);
95
const
array_typet
array=
to_array_type
(symbol_pair.second.type);
96
const
auto
size=
97
pointer_offset_size
(array.
subtype
(), ns);
98
99
if
(!size.has_value())
100
throw
"type of unknown size:\n"
+it_type.pretty();
101
102
if
(2*integer2long(*size)<=
config
.ansi_c.memory_operand_size)
103
{
104
out <<
"\nWARNING: "
105
<<
"declaration of an array at "
106
<< symbol_pair.second.location <<
107
<<
"\nmight be concurrently accessed\n"
;
108
}
109
#endif
110
}
111
}
112
}
print_struct_alignment_problems
void print_struct_alignment_problems(const symbol_table_baset &symbol_table, std::ostream &out)
Definition
alignment_checks.cpp:22
alignment_checks.h
Alignment Checks.
config
configt config
Definition
config.cpp:25
array_typet
Arrays with given size.
Definition
std_types.h:807
array_typet::subtype
const typet & subtype() const
Definition
type.h:187
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition
irep.cpp:482
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
struct_typet
Structure type, corresponds to C style structs.
Definition
std_types.h:231
struct_union_typet::components
const componentst & components() const
Definition
std_types.h:147
struct_union_typet::componentst
std::vector< componentt > componentst
Definition
std_types.h:140
symbol_table_baset
The symbol table base class interface.
Definition
symbol_table_base.h:23
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition
symbol_table_base.h:31
typet
The type of an expression, extends irept.
Definition
type.h:29
typet::find_type
const typet & find_type(const irep_idt &name) const
Definition
type.h:120
config.h
namespace.h
pointer_offset_size
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Definition
pointer_offset_size.cpp:91
pointer_offset_size.h
Pointer Logic.
mp_integer
BigInt mp_integer
Definition
smt_terms.h:17
std_types.h
Pre-defined types.
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition
std_types.h:308
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition
std_types.h:888
symbol_table_base.h
Author: Diffblue Ltd.
goto-instrument
alignment_checks.cpp
Generated by
1.17.0