cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
exprt
Base class for all expressions.
Definition
expr.h:57
exprt::exprt
exprt()
Definition
expr.h:62
irept::get
const irep_idt & get(const irep_idt &name) const
Definition
irep.cpp:44
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition
irep.h:412
irept::id
const irep_idt & id() const
Definition
irep.h:388
java_string_literal_exprt::value
irep_idt value() const
Definition
java_string_literal_expr.h:26
java_string_literal_exprt::java_string_literal_exprt
java_string_literal_exprt(const irep_idt &literal)
Definition
java_string_literal_expr.h:20
expr_cast.h
Templated functions to cast to specific exprt-derived classes.
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
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
jbmc
src
java_bytecode
java_string_literal_expr.h
Generated by
1.17.0