10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
bool Func::checkLoop( const cir::BasicBlock& header, queue< const BasicBlock* >& parentWorkQueue )
{
ProfileZoneScoped;
if( ms_TraceMode )
cout << " == Checking loop " << header.index() << endl;
AssertionHandlerGuard ahg( m_builder );
m_remapper.beginLoopUnrolling( header.index() );
bool completed = false;
uint32_t k = 0;
|
>
>
|
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
bool Func::checkLoop( const cir::BasicBlock& header, queue< const BasicBlock* >& parentWorkQueue )
{
ProfileZoneScoped;
if( ms_TraceMode )
cout << " == Checking loop " << header.index() << endl;
auto origAssHandler = m_builder.assertionHandler();
AssertionHandlerGuard ahg( m_builder );
m_remapper.beginLoopUnrolling( header.index() );
bool completed = false;
uint32_t k = 0;
|
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
// For the final loop instance, if we aren't at the last value of k before giving up,
// we want to resolve the assertions without emitting diagnostics:
// if they fail it means we need to increase k and try again.
// Otherwise, we want to use the regular assertion handler that will emit error
// messages for all failed assertions.
if( k == maxK )
{
m_builder.setAssertionHandler( [&]( auto&& expr, auto&& exprToCheck, LocationId locationId )
{
return checkAssertion( expr, exprToCheck, locationId );
} );
}
|
<
|
<
<
<
<
|
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
// For the final loop instance, if we aren't at the last value of k before giving up,
// we want to resolve the assertions without emitting diagnostics:
// if they fail it means we need to increase k and try again.
// Otherwise, we want to use the regular assertion handler that will emit error
// messages for all failed assertions.
if( k == maxK )
m_builder.setAssertionHandler( origAssHandler );
else
{
m_builder.setAssertionHandler( [&]( const z3::expr& expr, const z3::expr& exprToCheck, LocationId locationId )
{
if( ms_TraceMode )
return true;
|