Goose  loop.cpp at [f7c8245cb2]

File bs/verify/loop.cpp artifact c318dca5f2 part of check-in f7c8245cb2

#include "verify.h"
#include "builtins/builtins.h"

namespace goose::verify
{
    bool Func::checkLoop( const llr::BasicBlock& bb, queue< const BasicBlock* >& parentWorkQueue )
    {
        if( ms_TraceMode )
            cout << "  == Checking loop " << bb.index() << endl;

        // Just try to unroll the loop a few times for now so we can check that
        // everything gets linker together properly
        m_remapper.beginLoopUnrolling( bb.index() );

        buildZ3Expressions( bb, &parentWorkQueue );

        m_remapper.nextLoopIteration();
        buildZ3Expressions( bb, &parentWorkQueue );

        m_remapper.nextLoopIteration();
        buildZ3Expressions( bb, &parentWorkQueue );

        m_remapper.endLoopUnrolling();

        if( ms_TraceMode )
            cout << "  == Finished checking loop " << bb.index() << endl;
        return true;
    }
}