CBMC
literal_expr.h File Reference
#include <util/std_expr.h>
#include "literal.h"
+ Include dependency graph for literal_expr.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  literal_exprt
 

Functions

template<>
bool can_cast_expr< literal_exprt > (const exprt &base)
 
void validate_expr (const literal_exprt &literal)
 
const literal_exprtto_literal_expr (const exprt &expr)
 Cast a generic exprt to a literal_exprt. More...
 
literal_exprtto_literal_expr (exprt &expr)
 Cast a generic exprt to a literal_exprt. More...
 

Function Documentation

◆ can_cast_expr< literal_exprt >()

template<>
bool can_cast_expr< literal_exprt > ( const exprt base)
inline

Definition at line 40 of file literal_expr.h.

◆ to_literal_expr() [1/2]

const literal_exprt& to_literal_expr ( const exprt expr)
inline

Cast a generic exprt to a literal_exprt.

This is an unchecked conversion. expr must be known to be literal_exprt.

Parameters
exprSource expression
Returns
Object of type literal_exprt

Definition at line 56 of file literal_expr.h.

◆ to_literal_expr() [2/2]

literal_exprt& to_literal_expr ( exprt expr)
inline

Cast a generic exprt to a literal_exprt.

This is an unchecked conversion. expr must be known to be literal_exprt.

Parameters
exprSource expression
Returns
Object of type literal_exprt

Definition at line 66 of file literal_expr.h.

◆ validate_expr()

void validate_expr ( const literal_exprt literal)
inline

Definition at line 45 of file literal_expr.h.