Skip to content

Commit b88e678

Browse files
Martin Brainmartin
authored andcommitted
Improve the simplification of the constant domain.
1 parent 2c4fede commit b88e678

File tree

2 files changed

+21
-0
lines changed

2 files changed

+21
-0
lines changed

src/analyses/constant_propagator.cpp

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -334,6 +334,26 @@ void constant_propagator_domaint::assign(
334334

335335
/*******************************************************************\
336336
337+
Function: constant_propagator_domaint::assign
338+
339+
Inputs: The condition to simplify and its namespace.
340+
341+
Outputs: The simplified condition.
342+
343+
Purpose: Simplify the condition given context-sensitive knowledge from the domain.
344+
345+
\*******************************************************************/
346+
347+
exprt constant_propagator_domaint::domain_simplify (const exprt &condition,
348+
const namespacet &ns)
349+
{
350+
exprt e(condition);
351+
values.replace_const(e);
352+
return simplify_expr(e, ns);
353+
}
354+
355+
/*******************************************************************\
356+
337357
Function: constant_propagator_domaint::is_array_constant
338358
339359
Inputs:

src/analyses/constant_propagator.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ class constant_propagator_domaint:public ai_domain_baset
1919
virtual void transform(locationt, locationt, ai_baset &, const namespacet &);
2020
virtual void output(std::ostream &, const ai_baset &, const namespacet &) const;
2121
bool merge(const constant_propagator_domaint &, locationt, locationt);
22+
virtual exprt domain_simplify (const exprt &condition, const namespacet &ns);
2223

2324
struct valuest
2425
{

0 commit comments

Comments
 (0)