CBMC
Loading...
Searching...
No Matches
Public Member Functions | Protected Attributes | List of all members
havoc_utils_can_forward_propagatet Class Reference

A class containing utility functions for havocing expressions. More...

#include <havoc_utils.h>

+ Inheritance diagram for havoc_utils_can_forward_propagatet:
+ Collaboration diagram for havoc_utils_can_forward_propagatet:

Public Member Functions

 havoc_utils_can_forward_propagatet (const assignst &mod, const namespacet &ns)
 
bool is_constant (const exprt &expr) const override
 This function determines what expressions are to be propagated as "constants".
 
- Public Member Functions inherited from can_forward_propagatet
 can_forward_propagatet (const namespacet &ns)
 
bool operator() (const exprt &e) const
 returns true iff the expression can be considered constant
 

Protected Attributes

const assignst & assigns
 
- Protected Attributes inherited from can_forward_propagatet
const namespacet & ns
 

Additional Inherited Members

- Protected Member Functions inherited from can_forward_propagatet
virtual bool is_constant_address_of (const exprt &) const
 this function determines which reference-typed expressions are constant
 

Detailed Description

A class containing utility functions for havocing expressions.

Definition at line 27 of file havoc_utils.h.

Constructor & Destructor Documentation

◆ havoc_utils_can_forward_propagatet()

havoc_utils_can_forward_propagatet::havoc_utils_can_forward_propagatet ( const assignst &  mod,
const namespacet &  ns 
)
inlineexplicit

Definition at line 30 of file havoc_utils.h.

Member Function Documentation

◆ is_constant()

bool havoc_utils_can_forward_propagatet::is_constant ( const exprt &  expr) const
inlineoverridevirtual

This function determines what expressions are to be propagated as "constants".

Reimplemented from can_forward_propagatet.

Definition at line 37 of file havoc_utils.h.

Member Data Documentation

◆ assigns

const assignst& havoc_utils_can_forward_propagatet::assigns
protected

Definition at line 49 of file havoc_utils.h.

The documentation for this class was generated from the following file: