cprover
Loading...
Searching...
No Matches
validate_expressions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Validate expressions
4
5Author: Daniel Poetzl
6
7\*******************************************************************/
8
10#include "validate_helpers.h"
11
12#ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS
13#include <iostream>
14#endif
15
16#include "pointer_expr.h"
17#include "ssa_expr.h"
18
19#define CALL_ON_EXPR(expr_type) \
20 C<exprt, expr_type>()(expr, std::forward<Args>(args)...)
21
22template <template <typename, typename> class C, typename... Args>
23void call_on_expr(const exprt &expr, Args &&... args)
24{
25 if(expr.id() == ID_equal)
26 {
28 }
29 else if(expr.id() == ID_plus)
30 {
32 }
33 else if(is_ssa_expr(expr))
34 {
36 }
37 else if(expr.id() == ID_member)
38 {
40 }
41 else if(expr.id() == ID_dereference)
42 {
44 }
45 else
46 {
47#ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS
48 std::cerr << "Unimplemented well-formedness check for expression with id: "
49 << expr.id_string() std::endl;
50#endif
51
53 }
54}
55
64void check_expr(const exprt &expr, const validation_modet vm)
65{
67}
68
78 const exprt &expr,
79 const namespacet &ns,
80 const validation_modet vm)
81{
82 call_on_expr<call_validatet>(expr, ns, vm);
83}
84
94 const exprt &expr,
95 const namespacet &ns,
96 const validation_modet vm)
97{
99}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Operator to dereference a pointer.
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
const std::string & id_string() const
Definition irep.h:399
const irep_idt & id() const
Definition irep.h:396
Extract member of struct or union.
Definition std_expr.h:2667
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The plus expression Associativity is not specified.
Definition std_expr.h:914
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
API to expression classes for Pointers.
bool is_ssa_expr(const exprt &expr)
Definition ssa_expr.h:125
void check_expr(const exprt &expr, const validation_modet vm)
Check that the given expression is well-formed (shallow checks only, i.e., subexpressions and its typ...
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
void validate_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed, assuming that its subexpression and type have already...
void call_on_expr(const exprt &expr, Args &&... args)
#define CALL_ON_EXPR(expr_type)
validation_modet