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))
There are a large number of kinds of tree structured or tree-like data in CPROVER.
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.