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 74 of file invariant.h.

Constructor & Destructor Documentation

cbmc_invariants_should_throwt()

cbmc_invariants_should_throwt::cbmc_invariants_should_throwt ( )

inline

Definition at line 77 of file invariant.h.

~cbmc_invariants_should_throwt()

cbmc_invariants_should_throwt::~cbmc_invariants_should_throwt ( )

inline

Definition at line 82 of file invariant.h.

Member Data Documentation

old_state

bool cbmc_invariants_should_throwt::old_state

Definition at line 76 of file invariant.h.

---

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

• /home/runner/work/cbmc-documentation/cbmc-documentation/src/util/invariant.h