9 #ifndef CPROVER_UTIL_INVARIANT_TYPES_H
10 #define CPROVER_UTIL_INVARIANT_TYPES_H
24 const irept &problem_node,
25 const std::string &description);
30 #define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
31 INVARIANT_STRUCTURED( \
34 pretty_print_invariant_with_irep((IREP), (DESCRIPTION)))
37 #define PRECONDITION_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
38 INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
39 #define POSTCONDITION_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
40 INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
41 #define CHECK_RETURN_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
42 INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
43 #define UNREACHABLE_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
44 INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
45 #define DATA_INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
46 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.