CBMC
cpp_template_args.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CPP_CPP_TEMPLATE_ARGS_H
13 #define CPROVER_CPP_CPP_TEMPLATE_ARGS_H
14 
15 #include <util/expr.h>
16 #include <util/invariant.h>
17 
18 // A data structures for template arguments, i.e.,
19 // a sequence of types/expressions of the form <E1, T2, ...>.
20 // Not to be confused with the template parameters!
21 
23 {
24 public:
25  cpp_template_args_baset():irept(ID_template_args)
26  {
27  }
28 
30 
32  {
33  return (argumentst &)(add(ID_arguments).get_sub());
34  }
35 
36  const argumentst &arguments() const
37  {
38  return (const argumentst &)(find(ID_arguments).get_sub());
39  }
40 };
41 
42 // the non-yet typechecked variant
43 
45 {
46 };
47 
49  irept &irep)
50 {
51  PRECONDITION(irep.id() == ID_template_args);
52  return static_cast<cpp_template_args_non_tct &>(irep);
53 }
54 
56  const irept &irep)
57 {
58  PRECONDITION(irep.id() == ID_template_args);
59  return static_cast<const cpp_template_args_non_tct &>(irep);
60 }
61 
62 // the already typechecked variant
63 
65 {
66 public:
67  bool has_unassigned() const
68  {
69  const argumentst &_arguments=arguments();
70  for(argumentst::const_iterator
71  it=_arguments.begin();
72  it!=_arguments.end();
73  it++)
74  if(it->id()==ID_unassigned ||
75  it->type().id()==ID_unassigned)
76  return true;
77 
78  return false;
79  }
80 };
81 
83 {
84  PRECONDITION(irep.id() == ID_template_args);
85  return static_cast<cpp_template_args_tct &>(irep);
86 }
87 
89 {
90  PRECONDITION(irep.id() == ID_template_args);
91  return static_cast<const cpp_template_args_tct &>(irep);
92 }
93 
94 #endif // CPROVER_CPP_CPP_TEMPLATE_ARGS_H
to_cpp_template_args_non_tc
cpp_template_args_non_tct & to_cpp_template_args_non_tc(irept &irep)
Definition: cpp_template_args.h:48
irept::find
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
invariant.h
cpp_template_args_baset
Definition: cpp_template_args.h:22
cpp_template_args_tct
Definition: cpp_template_args.h:64
expr.h
to_cpp_template_args_tc
cpp_template_args_tct & to_cpp_template_args_tc(irept &irep)
Definition: cpp_template_args.h:82
cpp_template_args_baset::arguments
argumentst & arguments()
Definition: cpp_template_args.h:31
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
irept::id
const irep_idt & id() const
Definition: irep.h:396
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:58
cpp_template_args_non_tct
Definition: cpp_template_args.h:44
irept::add
irept & add(const irep_idt &name)
Definition: irep.cpp:116
irept::get_sub
subt & get_sub()
Definition: irep.h:456
cpp_template_args_tct::has_unassigned
bool has_unassigned() const
Definition: cpp_template_args.h:67
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:359
cpp_template_args_baset::argumentst
exprt::operandst argumentst
Definition: cpp_template_args.h:29
cpp_template_args_baset::arguments
const argumentst & arguments() const
Definition: cpp_template_args.h:36
cpp_template_args_baset::cpp_template_args_baset
cpp_template_args_baset()
Definition: cpp_template_args.h:25