CBMC: /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_expr.h File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Functions

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.

java_instanceof_exprt & to_java_instanceof_expr (exprt &expr)

Cast an exprt to a java_instanceof_exprt.

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.