CBMC
Loading...
Searching...
No Matches
alignment_checks.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Alignment Checks
4
5Author:
6
7\*******************************************************************/
8
11
12#include "alignment_checks.h"
13
14#include <util/config.h>
15#include <util/namespace.h>
17#include <util/std_types.h>
19
20#include <ostream>
21
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 {
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
67 it_mem = it_next - 1;
68 break;
69 }
70
71 if(it_mem != it_next && !it_next->get_is_padding())
72 {
74 {
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}
void print_struct_alignment_problems(const symbol_table_baset &symbol_table, std::ostream &out)
Alignment Checks.
configt config
Definition config.cpp:25
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Arrays with given size.
Definition std_types.h:807
const typet & subtype() const
Definition type.h:187
struct configt::ansi_ct ansi_c
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The type of an expression, extends irept.
Definition type.h:29
const typet & find_type(const irep_idt &name) const
Definition type.h:120
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.
Pointer Logic.
BigInt mp_integer
Definition smt_terms.h:17
Pre-defined types.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
Author: Diffblue Ltd.