cprover
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 #include "irep.h"
14 
15 #include <string>
16 
23  const irept &problem_node,
24  const std::string &description);
25 
29 #define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
30  INVARIANT_STRUCTURED( \
31  CONDITION, \
32  invariant_failedt, \
33  pretty_print_invariant_with_irep((IREP), (DESCRIPTION)))
34 
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))
46 
47 #endif
invariant.h
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
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:14
irep.h