CBMC
invariant_utils.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Invariant helper utilities
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_INVARIANT_TYPES_H
10 #define CPROVER_UTIL_INVARIANT_TYPES_H
11 
12 #include "invariant.h"
13 
14 #include <string>
15 
16 class irept;
17 
23 std::string pretty_print_invariant_with_irep(
24  const irept &problem_node,
25  const std::string &description);
26 
30 #define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
31  INVARIANT_STRUCTURED( \
32  CONDITION, \
33  invariant_failedt, \
34  pretty_print_invariant_with_irep((IREP), (DESCRIPTION)))
35 
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))
47 
48 #endif
invariant.h
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:359
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.
Definition: invariant_utils.cpp:16