Why doesn't Polyspace(R2012b) report all overflows?
2 次查看(过去 30 天)
显示 更早的评论
Simple code in my file running in multitasking verification mode with ep_task and interrupt_task as entry points.
The problem is that on variable c there is no overflow reported.
static signed char a;
static signed char b;
static signed char c;
/************************************ Periodic and interrupt functions ************************************/
void one_interrupt(void)
{
a=127;
}
void t_10ms(void)
{
a++;
b++;
c++;
}
void t_50ms(void)
{
a=0;
}
/************************************** Entry point functions ********************************************/
void ep_task()
{
volatile int t;
while(1)
{
t_10ms();
t_10ms();
t_10ms();
t_10ms();
t_10ms();
t_50ms();
}
}
void interrupt_task(void)
{
while(1)
{
one_interrupt();
}
}
/*********************************** Main function used as initialization **********************************/
void main(void)
{
a = 0;
b = 0;
c = 0;
}
0 个评论
回答(1 个)
Alexandre De Barros
2015-12-26
Hi!
There is no overflow on c because there is another overflow on the variable b just before that stops the execution of t_10ms.
The first iterations in t_10ms for b and c are ok (and so these variables are incremented) but there is eventually an overflow on b. And because of this overflow, for Polyspace the execution of t_10m stops on the b++ statement. The overflow on c++ is then never reached, hence only the safe increments for c are given.
If you invert the b++ and c++ statements, you will see that this time b++ is green.
Alex
另请参阅
类别
在 Help Center 和 File Exchange 中查找有关 Code Prover Verification 的更多信息
Community Treasure Hunt
Find the treasures in MATLAB Central and discover how the community can help you!
Start Hunting!