Possible bugs found my Modelchecker

[GoogleCodeExporter]

I tried to verify that the baseflight firmware does not have any obvious bugs 
like division by zero, array access out of bound, ...

To do this I used CBMC to verify the loop function in mw.c. Until now CBMC 
found two possible bugs. I'm not sure if this are real bugs as the tool works 
with non-deterministic assumptions and cannot check if the values that trigger 
the bug are present during normal operation.

In the function annexCode line 125: array out of bound when tmp=500 in statement

rcCommand[axis] = lookupPitchRollRC[tmp2] + (tmp - tmp2 * 100) * 
(lookupPitchRollRC[tmp2 + 1] - lookupPitchRollRC[tmp2]) / 100;

Line 803: possible integer overflow in statement

cycleTime = (int32_t)(currentTime - previousTime);


The verification is not finished yet and more bugs may be found. I will report 
back any further results.

Regards,
Johannes

Original issue reported on code.google.com by [email protected] on 10 Oct 2013 at 11:41