CBMC
Loading...
Searching...
No Matches
c_storage_spec.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "c_storage_spec.h"
10
12
14{
15 if(type.id()==ID_merged_type ||
16 type.id()==ID_code)
17 {
18 for(const typet &subtype : to_type_with_subtypes(type).subtypes())
19 read(subtype);
20 }
21 else if(type.id()==ID_static)
22 is_static=true;
23 else if(type.id()==ID_thread_local)
24 is_thread_local=true;
25 else if(type.id()==ID_inline)
26 is_inline=true;
27 else if(type.id()==ID_extern)
28 is_extern=true;
29 else if(type.id()==ID_typedef)
30 is_typedef=true;
31 else if(type.id()==ID_register)
32 is_register=true;
33 else if(type.id()==ID_weak)
34 is_weak=true;
35 else if(type.id() == ID_used)
36 is_used = true;
37 else if(type.id()==ID_auto)
38 {
39 // ignore
40 }
41 else if(type.id()==ID_msc_declspec)
42 {
43 const exprt &as_expr=
44 static_cast<const exprt &>(static_cast<const irept &>(type));
45 for(const auto &op : as_expr.operands())
46 {
47 if(op.id() == ID_thread)
48 is_thread_local=true;
49 }
50 }
51 else if(
52 type.id() == ID_alias && type.has_subtype() &&
53 to_type_with_subtype(type).subtype().id() == ID_string_constant)
54 {
55 alias = to_string_constant(to_type_with_subtype(type).subtype()).value();
56 }
57 else if(
58 type.id() == ID_asm && !to_type_with_subtypes(type).subtypes().empty() &&
59 to_type_with_subtypes(type).subtypes()[0].id() == ID_string_constant)
60 {
61 asm_label =
62 to_string_constant(to_type_with_subtypes(type).subtypes()[0]).value();
63 }
64 else if(
65 type.id() == ID_section && type.has_subtype() &&
66 to_type_with_subtype(type).subtype().id() == ID_string_constant)
67 {
68 section = to_string_constant(to_type_with_subtype(type).subtype()).value();
69 }
70}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
void read(const typet &type)
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
const irep_idt & id() const
Definition irep.h:388
The type of an expression, extends irept.
Definition type.h:29
bool has_subtype() const
Definition type.h:64
int __CPROVER_ID java::java io InputStream read
Definition java.io.c:5
const string_constantt & to_string_constant(const exprt &expr)
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition type.h:252
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208