java_expr.h File Reference

Java-specific exprt subclasses. More...

#include <util/std_expr.h>

Include dependency graph for java_expr.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	java_instanceof_exprt

Functions
template<>
bool	can_cast_expr< java_instanceof_exprt > (const exprt &base)
void	validate_expr (const java_instanceof_exprt &value)
const java_instanceof_exprt &	to_java_instanceof_expr (const exprt &expr)
	Cast an exprt to a java_instanceof_exprt. More...
java_instanceof_exprt &	to_java_instanceof_expr (exprt &expr)
	Cast an exprt to a java_instanceof_exprt. More...

Detailed Description

Java-specific exprt subclasses.

Definition in file java_expr.h.

Function Documentation

can_cast_expr< java_instanceof_exprt >()

template<>

bool can_cast_expr< java_instanceof_exprt > ( const exprt &  base )

inline

Definition at line 70 of file java_expr.h.

to_java_instanceof_expr() [1/2]

const java_instanceof_exprt& to_java_instanceof_expr ( const exprt &  expr )

inline

Cast an exprt to a java_instanceof_exprt.

expr must be known to be java_instanceof_exprt.

Parameters

expr	Source expression

Returns

Object of type java_instanceof_exprt

Definition at line 86 of file java_expr.h.

to_java_instanceof_expr() [2/2]

java_instanceof_exprt& to_java_instanceof_expr ( exprt &  expr )

inline

Cast an exprt to a java_instanceof_exprt.

expr must be known to be java_instanceof_exprt.

Parameters

expr	Source expression

Returns

Object of type java_instanceof_exprt

Definition at line 94 of file java_expr.h.

validate_expr()

void validate_expr ( const java_instanceof_exprt &  value )

inline

Definition at line 75 of file java_expr.h.