cprover
cbmc_invariants_should_throwt Struct Reference

Helper to enable invariant throwing as above bounded to an object lifetime: More...

#include <invariant.h>

Public Member Functions

 cbmc_invariants_should_throwt ()
 
 ~cbmc_invariants_should_throwt ()
 

Public Attributes

bool old_state
 

Detailed Description

Helper to enable invariant throwing as above bounded to an object lifetime:

Definition at line 75 of file invariant.h.

Constructor & Destructor Documentation

◆ cbmc_invariants_should_throwt()

cbmc_invariants_should_throwt::cbmc_invariants_should_throwt ( )
inline

Definition at line 78 of file invariant.h.

◆ ~cbmc_invariants_should_throwt()

cbmc_invariants_should_throwt::~cbmc_invariants_should_throwt ( )
inline

Definition at line 83 of file invariant.h.

Member Data Documentation

◆ old_state

bool cbmc_invariants_should_throwt::old_state

Definition at line 77 of file invariant.h.


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