@@ -19,6 +19,7 @@ Author: Peter Schrammel
19
19
#include < util/arith_tools.h>
20
20
#include < util/base_type.h>
21
21
#include < util/cprover_prefix.h>
22
+ #include < util/expr_util.h>
22
23
#include < util/find_symbols.h>
23
24
#include < util/ieee_float.h>
24
25
#include < util/simplify_expr.h>
@@ -288,48 +289,31 @@ bool constant_propagator_domaint::ai_simplify(
288
289
289
290
bool constant_propagator_domaint::valuest::is_constant (const exprt &expr) const
290
291
{
291
- if (expr.id ()==ID_side_effect &&
292
- to_side_effect_expr (expr).get_statement ()==ID_nondet)
293
- return false ;
294
-
295
- if (expr.id ()==ID_side_effect &&
296
- to_side_effect_expr (expr).get_statement ()==ID_allocate)
297
- return false ;
298
-
299
- if (expr.id ()==ID_symbol)
300
- if (!replace_const.replaces_symbol (to_symbol_expr (expr).get_identifier ()))
301
- return false ;
302
-
303
- if (expr.id ()==ID_index)
304
- return false ;
305
-
306
- if (expr.id ()==ID_address_of)
307
- return is_constant_address_of (to_address_of_expr (expr).object ());
308
-
309
- forall_operands (it, expr)
310
- if (!is_constant (*it))
311
- return false ;
312
-
313
- return true ;
314
- }
315
-
316
- bool constant_propagator_domaint::valuest::is_constant_address_of (
317
- const exprt &expr) const
318
- {
319
- if (expr.id ()==ID_index)
320
- return is_constant_address_of (to_index_expr (expr).array ()) &&
321
- is_constant (to_index_expr (expr).index ());
292
+ class constant_propagator_is_constantt : public is_constantt
293
+ {
294
+ public:
295
+ explicit constant_propagator_is_constantt (
296
+ const replace_symbolt &replace_const)
297
+ : replace_const(replace_const)
298
+ {
299
+ }
322
300
323
- if (expr.id ()==ID_member)
324
- return is_constant_address_of (to_member_expr (expr).struct_op ());
301
+ protected:
302
+ bool is_constant (const exprt &expr) const override
303
+ {
304
+ if (expr.id () == ID_symbol)
305
+ {
306
+ return replace_const.replaces_symbol (
307
+ to_symbol_expr (expr).get_identifier ());
308
+ }
325
309
326
- if (expr. id ()==ID_dereference)
327
- return is_constant ( to_dereference_expr (expr). pointer ());
310
+ return is_constantt::is_constant (expr);
311
+ }
328
312
329
- if (expr. id ()==ID_string_constant)
330
- return true ;
313
+ const replace_symbolt &replace_const;
314
+ } ;
331
315
332
- return true ;
316
+ return constant_propagator_is_constantt (replace_const)(expr) ;
333
317
}
334
318
335
319
// / Do not call this when iterating over replace_const.expr_map!
0 commit comments