CBMC
loop_contract_configt Struct Reference

Loop contract configurations. More...

#include <loop_contract_config.h>

Public Member Functions

std::string to_string () const
 
bool operator== (const loop_contract_configt &rhs) const
 
bool operator!= (const loop_contract_configt &rhs) const
 

Public Attributes

bool apply_loop_contracts = false
 
bool unwind_transformed_loops = true
 
bool check_side_effect = true
 

Detailed Description

Loop contract configurations.

Definition at line 18 of file loop_contract_config.h.

Member Function Documentation

◆ operator!=()

bool loop_contract_configt::operator!= ( const loop_contract_configt rhs) const
inline

Definition at line 49 of file loop_contract_config.h.

◆ operator==()

bool loop_contract_configt::operator== ( const loop_contract_configt rhs) const
inline

Definition at line 42 of file loop_contract_config.h.

◆ to_string()

std::string loop_contract_configt::to_string ( ) const
inline

Definition at line 30 of file loop_contract_config.h.

Member Data Documentation

◆ apply_loop_contracts

bool loop_contract_configt::apply_loop_contracts = false

Definition at line 22 of file loop_contract_config.h.

◆ check_side_effect

bool loop_contract_configt::check_side_effect = true

Definition at line 28 of file loop_contract_config.h.

◆ unwind_transformed_loops

bool loop_contract_configt::unwind_transformed_loops = true

Definition at line 25 of file loop_contract_config.h.


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