Changes
Page history
infeasible omitted
authored
Feb 06, 2020
by
Markus Klinik
Show whitespace changes
Inline
Side-by-side
Home.md
View page @
b0011672
...
...
@@ -102,3 +102,42 @@ int main() {
[
](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/code/website/split-and-merge-main-no-merge-highres.svg)
[
](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/code/website/split-and-merge-main-highres.svg)
## A program with three execution paths
Infeasible paths are omitted by the symbolic execution.
```
c
int
main
()
{
x
=
TERM
.
readInt
();
if
(
x
<=
5
)
{
LED1
.
switchOn
();
LED1
.
switchOff
();
}
else
{
LED2
.
switchOn
();
LED2
.
switchOff
();
}
if
(
x
<=
10
)
{
LED1
.
switchOn
();
LED1
.
switchOff
();
}
else
{
LED2
.
switchOn
();
LED2
.
switchOff
();
}
return
0
;
}
```
[
](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/code/website/infeasible-omitted-main-no-merge-highres.svg)
[
](https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/code/website/infeasible-omitted-main-highres.svg)
