java_string_literal_expr.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Java Bytecode
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
 
#ifndef CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERAL_EXPR_H
#define CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERAL_EXPR_H
 
#include <util/expr_cast.h>
 
class java_string_literal_exprt : public exprt
{
public:
  explicit java_string_literal_exprt(const irep_idt &literal)
    : exprt(ID_java_string_literal)
  {
    set(ID_value, literal);
  }
  explicit java_string_literal_exprt(const irep_idt &literal) {…}
 
  irep_idt value() const
  {
    return get(ID_value);
  }
  irep_idt value() const {…}
};
class java_string_literal_exprt : public exprt {…};
 
template <>
inline bool can_cast_expr<java_string_literal_exprt>(const exprt &base)
{
  return base.id() == ID_java_string_literal;
}
inline bool can_cast_expr<java_string_literal_exprt>(const exprt &base) {…}
 
#endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERAL_EXPR_H