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
17
class
java_string_literal_exprt
:
public
exprt
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
<>
33
inline
bool
can_cast_expr<java_string_literal_exprt>
(
const
exprt
&base)
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
jbmc
src
java_bytecode
java_string_literal_expr.h
Generated by
1.8.17