Why doesn't Polyspace(R2012b) report all overflows?
1 Ansicht (letzte 30 Tage)
Ältere Kommentare anzeigen
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 Kommentare
Antworten (1)
Alexandre De Barros
am 26 Dez. 2015
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
Siehe auch
Kategorien
Mehr zu Code Prover Verification finden Sie in Help Center und File Exchange
Produkte
Community Treasure Hunt
Find the treasures in MATLAB Central and discover how the community can help you!
Start Hunting!