77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
m_remapper.nextLoopIteration();
uint32_t firstInductionIterationHeaderIndex = m_remapper.remapBBId( header );
m_builder.setCurrentBB( firstInductionIterationHeaderIndex );
if( ms_TraceMode )
cout << " == Havocing modified addresses for loop " << header.index() << endl;
m_cfg->forEachAddressModifiedByLoop( header.index(), [&]( auto&& type, auto&& addr )
{
HavocAddress( m_builder, firstInductionIterationHeaderIndex, type, addr );
} );
if( ms_TraceMode )
cout << " == Unrolling first induction case for loop " << header.index() << endl;
buildZ3Expressions( header, &parentWorkQueue );
// Emit the rest of the induction case.
|
>
|
|
|
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
m_remapper.nextLoopIteration();
uint32_t firstInductionIterationHeaderIndex = m_remapper.remapBBId( header );
m_builder.setCurrentBB( firstInductionIterationHeaderIndex );
if( ms_TraceMode )
cout << " == Havocing modified addresses for loop " << header.index() << endl;
// TODO_STACKBASED: refactor the whole "address modified by loop" stuff
/*m_cfg->forEachAddressModifiedByLoop( header.index(), [&]( auto&& type, auto&& addr )
{
HavocAddress( m_builder, firstInductionIterationHeaderIndex, type, addr );
} );*/
if( ms_TraceMode )
cout << " == Unrolling first induction case for loop " << header.index() << endl;
buildZ3Expressions( header, &parentWorkQueue );
// Emit the rest of the induction case.
|