CBMC
cpp_template_parameter.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_CPP_CPP_TEMPLATE_PARAMETER_H
11 #define CPROVER_CPP_CPP_TEMPLATE_PARAMETER_H
12 
13 #include <util/expr.h>
14 
15 // A data structure for expressions of the form
16 // <typename T, int x, ...>
17 // Not to be confused with template arguments!
18 
20 {
21 public:
22  template_parametert():exprt(ID_template_parameter)
23  {
24  }
25 
26  #if 0
27  bool get_is_type() const
28  {
29  return get_bool(ID_is_type);
30  }
31 
32  void set_is_type(bool value)
33  {
34  set(ID_is_type, value);
35  }
36 
37  irep_idt get_identifier() const
38  {
39  return get(ID_identifier);
40  }
41 
42  void set_identifier(const irep_idt &identifier)
43  {
44  return set(ID_identifier, identifier);
45  }
46  #endif
47 
49  {
50  return static_cast<exprt &>(add(ID_C_default_value));
51  }
52 
53  const exprt &default_argument() const
54  {
55  return static_cast<const exprt &>(find(ID_C_default_value));
56  }
57 
58  bool has_default_argument() const
59  {
60  return find(ID_C_default_value).is_not_nil();
61  }
62 };
63 
66 {
67 public:
68  explicit template_parameter_symbol_typet(const irep_idt &identifier)
69  : typet(ID_template_parameter_symbol_type)
70  {
71  set_identifier(identifier);
72  }
73 
74  void set_identifier(const irep_idt &identifier)
75  {
76  set(ID_identifier, identifier);
77  }
78 
79  const irep_idt &get_identifier() const
80  {
81  return get(ID_identifier);
82  }
83 };
84 
95 {
96  PRECONDITION(type.id() == ID_template_parameter_symbol_type);
97  return static_cast<const template_parameter_symbol_typet &>(type);
98 }
99 
103 {
104  PRECONDITION(type.id() == ID_template_parameter_symbol_type);
105  return static_cast<template_parameter_symbol_typet &>(type);
106 }
107 
108 #endif // CPROVER_CPP_CPP_TEMPLATE_PARAMETER_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
template_parametert
Definition: cpp_template_parameter.h:19
typet
The type of an expression, extends irept.
Definition: type.h:28
irept::find
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
template_parameter_symbol_typet
a template parameter symbol that is a type
Definition: cpp_template_parameter.h:65
exprt
Base class for all expressions.
Definition: expr.h:55
template_parametert::default_argument
const exprt & default_argument() const
Definition: cpp_template_parameter.h:53
irept::get
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
expr.h
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:380
template_parametert::template_parametert
template_parametert()
Definition: cpp_template_parameter.h:22
get_identifier
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
Definition: smt2_incremental_decision_procedure.cpp:328
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
to_template_parameter_symbol_type
const template_parameter_symbol_typet & to_template_parameter_symbol_type(const typet &type)
Cast a typet to a template_parameter_symbol_typet.
Definition: cpp_template_parameter.h:94
irept::id
const irep_idt & id() const
Definition: irep.h:396
template_parametert::has_default_argument
bool has_default_argument() const
Definition: cpp_template_parameter.h:58
irept::add
irept & add(const irep_idt &name)
Definition: irep.cpp:116
template_parametert::default_argument
exprt & default_argument()
Definition: cpp_template_parameter.h:48
template_parameter_symbol_typet::get_identifier
const irep_idt & get_identifier() const
Definition: cpp_template_parameter.h:79
template_parameter_symbol_typet::template_parameter_symbol_typet
template_parameter_symbol_typet(const irep_idt &identifier)
Definition: cpp_template_parameter.h:68
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
template_parameter_symbol_typet::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: cpp_template_parameter.h:74