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 "ssa_expr.h"
19 #include "std_expr.h"
20 #include "validate.h"
21 
22 #define CALL_ON_EXPR(expr_type) \
23  C<exprt, expr_type>()(expr, std::forward<Args>(args)...)
24 
25 template <template <typename, typename> class C, typename... Args>
26 void call_on_expr(const exprt &expr, Args &&... args)
27 {
28  if(expr.id() == ID_equal)
29  {
31  }
32  else if(expr.id() == ID_plus)
33  {
35  }
36  else if(expr.get_bool(ID_C_SSA_symbol))
37  {
39  }
40  else if(expr.id() == ID_member)
41  {
43  }
44  else if(expr.id() == ID_dereference)
45  {
47  }
48  else
49  {
50 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS
51  std::cerr << "Unimplemented well-formedness check for expression with id: "
52  << expr.id_string() std::endl;
53 #endif
54 
56  }
57 }
58 
67 void check_expr(const exprt &expr, const validation_modet vm)
68 {
69  call_on_expr<call_checkt>(expr, vm);
70 }
71 
81  const exprt &expr,
82  const namespacet &ns,
83  const validation_modet vm)
84 {
85  call_on_expr<call_validatet>(expr, ns, vm);
86 }
87 
97  const exprt &expr,
98  const namespacet &ns,
99  const validation_modet vm)
100 {
101  call_on_expr<call_validate_fullt>(expr, ns, vm);
102 }
call_on_expr
void call_on_expr(const exprt &expr, Args &&... args)
Definition: validate_expressions.cpp:26
CALL_ON_EXPR
#define CALL_ON_EXPR(expr_type)
Definition: validate_expressions.cpp:22
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:67
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
exprt
Base class for all expressions.
Definition: expr.h:53
namespace.h
equal_exprt
Equality.
Definition: std_expr.h:1190
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
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:80
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
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:96
validate_expressions.h
std_expr.h
API to expression classes.