CBMC
java_string_literal_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java Bytecode
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERAL_EXPR_H
13 #define CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERAL_EXPR_H
14 
15 #include <util/expr_cast.h>
16 
18 {
19 public:
20  explicit java_string_literal_exprt(const irep_idt &literal)
21  : exprt(ID_java_string_literal)
22  {
23  set(ID_value, literal);
24  }
25 
26  irep_idt value() const
27  {
28  return get(ID_value);
29  }
30 };
31 
32 template <>
34 {
35  return base.id() == ID_java_string_literal;
36 }
37 
38 #endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERAL_EXPR_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
can_cast_expr< java_string_literal_exprt >
bool can_cast_expr< java_string_literal_exprt >(const exprt &base)
Definition: java_string_literal_expr.h:33
exprt
Base class for all expressions.
Definition: expr.h:55
irept::get
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
java_string_literal_exprt::java_string_literal_exprt
java_string_literal_exprt(const irep_idt &literal)
Definition: java_string_literal_expr.h:20
irept::id
const irep_idt & id() const
Definition: irep.h:396
expr_cast.h
Templated functions to cast to specific exprt-derived classes.
java_string_literal_exprt
Definition: java_string_literal_expr.h:17
java_string_literal_exprt::value
irep_idt value() const
Definition: java_string_literal_expr.h:26