⚲
Project
General
Profile
Sign in
Home
Projects
Help
Search
:
BLAST
All Projects
Linux Driver Verification
»
BLAST
Overview
Activity
Roadmap
Issues
News
Wiki
Files
Repository
Download (628 Bytes)
Bug #330
» latt2.c
latt2.c lines shifted -
Vadim Mutilin
, 11/11/2010 08:00 PM
void
error
()
{
ERROR:
goto
ERROR
;
}
int
nondet
();
int
nondet2
();
int
call
();
int
some
();
int
useless
();
int
functions
();
int
to
();
int
make
();
int
other
();
int
branches
();
int
proceed
();
int
main
()
{
int
a
,
b
,
z
;
if
(
nondet
()){
a
=
10
;
b
=
1
;
}
else
{
if
(
nondet2
()){
a
=
1
;
b
=
10
;
}
else
{
a
=
1
;
b
=
1
;
call
();
//due to DFS traversal, this branch may be at z=10 before the other!
some
();
useless
();
functions
();
to
();
make
();
other
();
branches
();
proceed
();
}
}
z
=
10
;
// coverage error happens here
if
(
a
==
1
&&
b
==
1
)
error
();
// and leads to missing this error!
return
0
;
}
« Previous
1
2
3
4
…
12
Next »
(2-2/12)
Loading...