Non-convergence with while(1)

[kokke]

Hi @arthaud

I have problems getting analysis to converge on this function:

uint32_t CLKPWR_GetCLK (uint8_t ClkType)
{
    switch(ClkType)
    {
        case CLKPWR_CLKTYPE_CPU:
            return SystemCoreClock;

        case CLKPWR_CLKTYPE_PER:
            return PeripheralClock;

        case CLKPWR_CLKTYPE_EMC:
            return EMCClock;

        case CLKPWR_CLKTYPE_USB:
            return USBClock;

        default:
            while(1); //error loop
    }
}

SystemCoreClock, PeripheralClock, EMCClock and USBClock are all uint32_t-variables.

I run IKOS like this:
ikos --entry-points=CLKPWR_GetCLK whole_program.bc

It seems the problem is with the while(1);-loop, since analysis converges immediately if I replace with assert(0);.

[arthaud]

Thanks for reporting this.

It was due to an infinite loop in source_location(). This is now fixed.

[kokke]

Thanks for the vigilant support 👍