cprover
validate_expressions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Validate expressions
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
9 #include "validate_expressions.h"
10 #include "validate_helpers.h"
11 
12 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS
13 #include <iostream>
14 #endif
15 
16 #include "expr.h"
17 #include "namespace.h"
18 #include "pointer_expr.h"
19 #include "ssa_expr.h"
20 #include "std_expr.h"
21 #include "validate.h"
22 
23 #define CALL_ON_EXPR(expr_type) \
24  C<exprt, expr_type>()(expr, std::forward<Args>(args)...)
25 
26 template <template <typename, typename> class C, typename... Args>
27 void call_on_expr(const exprt &expr, Args &&... args)
28 {
29  if(expr.id() == ID_equal)
30  {
32  }
33  else if(expr.id() == ID_plus)
34  {
36  }
37  else if(is_ssa_expr(expr))
38  {
40  }
41  else if(expr.id() == ID_member)
42  {
44  }
45  else if(expr.id() == ID_dereference)
46  {
48  }
49  else
50  {
51 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS
52  std::cerr << "Unimplemented well-formedness check for expression with id: "
53  << expr.id_string() std::endl;
54 #endif
55 
57  }
58 }
59 
68 void check_expr(const exprt &expr, const validation_modet vm)
69 {
70  call_on_expr<call_checkt>(expr, vm);
71 }
72 
82  const exprt &expr,
83  const namespacet &ns,
84  const validation_modet vm)
85 {
86  call_on_expr<call_validatet>(expr, ns, vm);
87 }
88 
98  const exprt &expr,
99  const namespacet &ns,
100  const validation_modet vm)
101 {
102  call_on_expr<call_validate_fullt>(expr, ns, vm);
103 }
call_on_expr
void call_on_expr(const exprt &expr, Args &&... args)
Definition: validate_expressions.cpp:27
CALL_ON_EXPR
#define CALL_ON_EXPR(expr_type)
Definition: validate_expressions.cpp:23
check_expr
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...
Definition: validate_expressions.cpp:68
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:256
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:831
exprt
Base class for all expressions.
Definition: expr.h:54
namespace.h
equal_exprt
Equality.
Definition: std_expr.h:1140
expr.h
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
pointer_expr.h
API to expression classes for Pointers.
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::id
const irep_idt & id() const
Definition: irep.h:407
validate_expr
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...
Definition: validate_expressions.cpp:81
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2528
ssa_expr.h
validate_helpers.h
validate.h
validate_full_expr
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...
Definition: validate_expressions.cpp:97
validate_expressions.h
std_expr.h
API to expression classes.