Skip to content

Commit c64448b

Browse files
Martin Brainmartin
Martin Brain
authored and
martin
committed
Implement ai_simplify for the constant domain.
1 parent 409d6ef commit c64448b

File tree

2 files changed

+27
-0
lines changed

2 files changed

+27
-0
lines changed

src/analyses/constant_propagator.cpp

+23
Original file line numberDiff line numberDiff line change
@@ -333,6 +333,29 @@ void constant_propagator_domaint::assign(
333333

334334
/*******************************************************************\
335335
336+
Function: constant_propagator_domaint::ai_simplify
337+
338+
Inputs: The condition to simplify and its namespace.
339+
340+
Outputs: The simplified condition.
341+
342+
Purpose: Simplify the condition given context-sensitive knowledge
343+
from the abstract state.
344+
345+
\*******************************************************************/
346+
347+
bool constant_propagator_domaint::ai_simplify(
348+
exprt &condition,
349+
const namespacet &ns) const
350+
{
351+
bool b=values.replace_const.replace(condition);
352+
b&=simplify(condition, ns);
353+
354+
return b;
355+
}
356+
357+
/*******************************************************************\
358+
336359
Function: constant_propagator_domaint::is_array_constant
337360
338361
Inputs:

src/analyses/constant_propagator.h

+4
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,10 @@ class constant_propagator_domaint:public ai_domain_baset
3030
void make_entry() final { values.set_to_top(); }
3131
bool merge(const constant_propagator_domaint &, locationt, locationt);
3232

33+
virtual bool ai_simplify(
34+
exprt &condition,
35+
const namespacet &ns) const override;
36+
3337
struct valuest
3438
{
3539
public:

0 commit comments

Comments
 (0)