cprover
Loading...
Searching...
No Matches
goto_symex_is_constant.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution Constant Propagation
4
5Author: Michael Tautschig, tautschn@amazon.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H
13#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H
14
15#include <util/expr.h>
16#include <util/expr_util.h>
17
19{
20protected:
21 bool is_constant(const exprt &expr) const override
22 {
23 if(expr.id() == ID_mult)
24 {
25 bool found_non_constant = false;
26
27 // propagate stuff with sizeof in it
28 forall_operands(it, expr)
29 {
30 if(it->find(ID_C_c_sizeof_type).is_not_nil())
31 return true;
32 else if(!is_constant(*it))
33 found_non_constant = true;
34 }
35
36 return !found_non_constant;
37 }
38 else if(expr.id() == ID_with)
39 {
40 // this is bad
41 /*
42 forall_operands(it, expr)
43 if(!is_constant(expr.op0()))
44 return false;
45
46 return true;
47 */
48 return false;
49 }
50
51 return is_constantt::is_constant(expr);
52 }
53};
54
55#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H
Base class for all expressions.
Definition: expr.h:54
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
const irep_idt & id() const
Definition: irep.h:396
Determine whether an expression is constant.
Definition: expr_util.h:89
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:226
#define forall_operands(it, expr)
Definition: expr.h:18
Deprecated expression utility functions.