CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
string_constant.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_UTIL_STRING_CONSTANT_H
10#define CPROVER_UTIL_STRING_CONSTANT_H
11
12#include "std_expr.h"
13
15{
16public:
17 explicit string_constantt(const irep_idt &);
18
19 void value(const irep_idt &);
20
21 const irep_idt &value() const
22 {
23 return get(ID_value);
24 }
25
27
28 const typet &char_type() const
29 {
30 return type().element_type();
31 }
32
33 const array_typet &type() const;
35};
36
37template <>
38inline bool can_cast_expr<string_constantt>(const exprt &base)
39{
40 return base.id() == ID_string_constant;
41}
42
43inline void validate_expr(const string_constantt &expr)
44{
45 validate_operands(expr, 0, "String constants must not have operands");
46}
47
48inline const string_constantt &to_string_constant(const exprt &expr)
49{
51 return static_cast<const string_constantt &>(expr);
52}
53
54inline const string_constantt &to_string_constant(const typet &type)
55{
56 return to_string_constant((const exprt &)type);
57}
58
60{
62 return static_cast<string_constantt &>(expr);
63}
64
66{
67 return to_string_constant((exprt &)type);
68}
69
70#endif // CPROVER_ANSI_C_STRING_CONSTANT_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Array constructor from list of elements.
Definition std_expr.h:1621
Arrays with given size.
Definition std_types.h:807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
An expression without operands.
Definition std_expr.h:22
const array_typet & type() const
const typet & char_type() const
const irep_idt & value() const
array_exprt to_array_expr() const
convert string into array constant
The type of an expression, extends irept.
Definition type.h:29
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition expr_cast.h:250
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
void validate_expr(const string_constantt &expr)
bool can_cast_expr< string_constantt >(const exprt &base)
const string_constantt & to_string_constant(const exprt &expr)