... | ... | @@ -229,3 +229,88 @@ x = TERM.readInt(); |
|
|
|
|
|
[![](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/raw/master/code/website/nested-loops-main-no-merge.svg)](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/code/website/nested-loops-main-no-merge-highres.svg)
|
|
|
[![](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/raw/master/code/website/nested-loops-main.svg)](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/code/website/nested-loops-main-highres.svg)
|
|
|
|
|
|
|
|
|
## A function with many evaluation paths
|
|
|
|
|
|
```c
|
|
|
int max = 3;
|
|
|
|
|
|
|
|
|
int main()
|
|
|
{
|
|
|
|
|
|
y = 1;
|
|
|
z = TERM.readInt();
|
|
|
x = z;
|
|
|
while( 0 <= x && x <= max )
|
|
|
{
|
|
|
if( y <= 0 )
|
|
|
{
|
|
|
LED1.switchOn();
|
|
|
LED2.switchOff();
|
|
|
}
|
|
|
else
|
|
|
{
|
|
|
LED2.switchOn();
|
|
|
LED1.switchOff();
|
|
|
}
|
|
|
|
|
|
y = y * -1;
|
|
|
x = x + 1;
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
z = TERM.readInt();
|
|
|
x = z;
|
|
|
while( 0 <= x && x <= max )
|
|
|
{
|
|
|
if( y <= 0 )
|
|
|
{
|
|
|
LED1.switchOn();
|
|
|
LED2.switchOff();
|
|
|
}
|
|
|
else
|
|
|
{
|
|
|
LED2.switchOn();
|
|
|
LED1.switchOff();
|
|
|
}
|
|
|
|
|
|
y = y * -1;
|
|
|
x = x + 1;
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
z = TERM.readInt();
|
|
|
x = z;
|
|
|
while( 0 <= x && x <= max )
|
|
|
{
|
|
|
if( y <= 0 )
|
|
|
{
|
|
|
LED1.switchOn();
|
|
|
LED2.switchOff();
|
|
|
}
|
|
|
else
|
|
|
{
|
|
|
LED2.switchOn();
|
|
|
LED1.switchOff();
|
|
|
}
|
|
|
|
|
|
y = y * -1;
|
|
|
x = x + 1;
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
return 0;
|
|
|
|
|
|
}
|
|
|
```
|
|
|
|
|
|
[![](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/raw/master/code/website/many-fragments-main-no-merge.svg)](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/code/website/many-fragments-main-no-merge-highres.svg)
|
|
|
[![](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/raw/master/code/website/many-fragments-main.svg)](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/code/website/many-fragments-main-highres.svg) |