Commit e7670577 authored by Adéla Štěpková's avatar Adéla Štěpková
Browse files

if no assert is found, just reverse what is there and do not add new main or error()

parent 1643a552

src/passes/startFromFailedAssert.cpp

+7 −7
Original line number Diff line number Diff line
@@ -175,11 +175,11 @@ void processAssertsInFunction(ModuleBundle& mod, Function* origF, FunctionBundle 
void addNewMain(ModuleBundle& mod, Function* badMain)

{

    mod.newMain = mod.functionsBuilder.getMain();

    auto* mainBB = BasicBlock::Create(mod.origModule.getContext(), "", mod.newMain);



    if (badMain) {

        auto* mainBB = BasicBlock::Create(mod.origModule.getContext(), "", mod.newMain);

        IRBuilder<> builder(mainBB);



    if (badMain) {

        if (badMain->arg_empty()) {

            builder.CreateCall(badMain);

        }
@@ -189,13 +189,13 @@ void addNewMain(ModuleBundle& mod, Function* badMain) 
            auto* nondet = builder.CreateCall(nondetGenerator);

            builder.CreateCall(badMain, {nondet});

        }

    }

    // if no bad main exists, that means no asserts were found

    // -> we can just create an empty main



        auto* zero = ConstantInt::get(Type::getInt32Ty(mod.revModule.getContext()), 0);

        builder.CreateRet(zero);

    }

    // if no bad main exists, that means no asserts were found

    // -> just leave the main that already exists in the module

}



void startFromFailedAssert(ModuleBundle& mod)

{