CodeProver: Non-terminating loop: condition var is read from HW in interrupt

simplified embedded C code:

void main()
{
...
do
{
    uint16 voltage = GetVoltage();
} while (voltage > 60);

// voltage is high enough to continue
...
}    
   
uint16 GetVoltage()
{
    return m_voltage;
}

interrupt void ReadAdc()
{
	if(ADC.ConversionDone = true)
	{
		m_voltage = ADC.Result;
	}
}

Code Prover error for "do":

Non-terminating loop

The loop is infinite or contains a run-time error.

Loop may be infinite.

Is that because Code Prover doesn't know what the ADC.Result returns (it could be 0 forever (which would be OK for this code), or a value bigger than 60)?

Or because of an incorrect interrupt configuration in Polyspace?

I tried adding ReadAdc() to -cyclic-tasks or -interrupts, but that didn't help.