CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
invariant_utils.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Invariant helper utilities
4
5Author: 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
16class irept;
17
23std::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
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
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