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 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
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:408
const irep_idt & id() const
Definition: irep.h:384
java_string_literal_exprt(const irep_idt &literal)
Templated functions to cast to specific exprt-derived classes.
bool can_cast_expr< java_string_literal_exprt >(const exprt &base)