CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_linkage_spec.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_CPP_CPP_LINKAGE_SPEC_H
13#define CPROVER_CPP_CPP_LINKAGE_SPEC_H
14
16{
17public:
21
22 typedef std::vector<class cpp_itemt> itemst;
23
24 const itemst &items() const
25 {
26 return (const itemst &)operands();
27 }
28
30 {
31 return (itemst &)operands();
32 }
33
35 {
36 return add(ID_linkage);
37 }
38
39 const irept &linkage() const
40 {
41 return find(ID_linkage);
42 }
43};
44
45#endif // CPROVER_CPP_CPP_LINKAGE_SPEC_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
const irept & linkage() const
std::vector< class cpp_itemt > itemst
const itemst & items() const
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 irept & find(const irep_idt &name) const
Definition irep.cpp:93
irept & add(const irep_idt &name)
Definition irep.cpp:103