9 #ifndef CPROVER_UTIL_INVARIANT_TYPES_H 10 #define CPROVER_UTIL_INVARIANT_TYPES_H 23 const irept &problem_node,
24 const std::string &description);
29 #define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ 30 INVARIANT_STRUCTURED( \ 33 pretty_print_invariant_with_irep((IREP), (DESCRIPTION))) 36 #define PRECONDITION_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ 37 INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP)) 38 #define POSTCONDITION_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ 39 INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP)) 40 #define CHECK_RETURN_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ 41 INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP)) 42 #define UNREACHABLE_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ 43 INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP)) 44 #define DATA_INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP) \ 45 INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (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.
Base class for tree-like data structures with sharing.