CBMC
invariant_utils.h File Reference
#include "invariant.h"
#include <string>
+ Include dependency graph for invariant_utils.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
 Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IREP, DESCRIPTION)) More...
 
#define PRECONDITION_WITH_IREP(CONDITION, DESCRIPTION, IREP)    INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
 See INVARIANT_WITH_IREP More...
 
#define POSTCONDITION_WITH_IREP(CONDITION, DESCRIPTION, IREP)    INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
 
#define CHECK_RETURN_WITH_IREP(CONDITION, DESCRIPTION, IREP)    INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
 
#define UNREACHABLE_WITH_IREP(CONDITION, DESCRIPTION, IREP)    INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
 
#define DATA_INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)    INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
 

Functions

std::string pretty_print_invariant_with_irep (const irept &problem_node, const std::string &description)
 Produces a plain string error description from an irep and some explanatory text. More...
 

Macro Definition Documentation

◆ CHECK_RETURN_WITH_IREP

#define CHECK_RETURN_WITH_IREP (   CONDITION,
  DESCRIPTION,
  IREP 
)     INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

Definition at line 41 of file invariant_utils.h.

◆ DATA_INVARIANT_WITH_IREP

#define DATA_INVARIANT_WITH_IREP (   CONDITION,
  DESCRIPTION,
  IREP 
)     INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

Definition at line 45 of file invariant_utils.h.

◆ INVARIANT_WITH_IREP

#define INVARIANT_WITH_IREP (   CONDITION,
  DESCRIPTION,
  IREP 
)
Value:
CONDITION, \
pretty_print_invariant_with_irep((IREP), (DESCRIPTION)))
A logic error, augmented with a distinguished field to hold a backtrace.
Definition: c_errors.h:28
std::string pretty_print_invariant_with_irep(const irept &problem_node, const std::string &description)
Produces a plain string error description from an irep and some explanatory text.
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:407

Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IREP, DESCRIPTION))

Definition at line 30 of file invariant_utils.h.

◆ POSTCONDITION_WITH_IREP

#define POSTCONDITION_WITH_IREP (   CONDITION,
  DESCRIPTION,
  IREP 
)     INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

Definition at line 39 of file invariant_utils.h.

◆ PRECONDITION_WITH_IREP

#define PRECONDITION_WITH_IREP (   CONDITION,
  DESCRIPTION,
  IREP 
)     INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

See INVARIANT_WITH_IREP

Definition at line 37 of file invariant_utils.h.

◆ UNREACHABLE_WITH_IREP

#define UNREACHABLE_WITH_IREP (   CONDITION,
  DESCRIPTION,
  IREP 
)     INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))

Definition at line 43 of file invariant_utils.h.

Function Documentation

◆ pretty_print_invariant_with_irep()

std::string pretty_print_invariant_with_irep ( const irept problem_node,
const std::string &  description 
)

Produces a plain string error description from an irep and some explanatory text.

If problem_node is nil, returns description.

Parameters
problem_nodeirep to pretty-print
descriptiondescriptive text to prepend
Returns
error message

Definition at line 16 of file invariant_utils.cpp.