Regression tests for not instrumenting built-ins
This commit is contained in:
parent
e88df0bc29
commit
c3931974d7
|
@ -0,0 +1,17 @@
|
|||
int main()
|
||||
{
|
||||
char a[10];
|
||||
__CPROVER_input("a[3]", a[3]);
|
||||
|
||||
int len = strlen(a);
|
||||
|
||||
if(len==3)
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
else if(len==4)
|
||||
{
|
||||
return -1;
|
||||
}
|
||||
return 1;
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
CORE
|
||||
main.c
|
||||
--cover location --unwind 1
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^\*\* 4 of 7 covered
|
||||
--
|
||||
^warning: ignoring
|
||||
^\[.*<builtin-library-
|
|
@ -0,0 +1,19 @@
|
|||
struct mystruct {
|
||||
int x;
|
||||
char y;
|
||||
};
|
||||
|
||||
int main()
|
||||
{
|
||||
struct mystruct s;
|
||||
char c;
|
||||
__CPROVER_input("c", c);
|
||||
|
||||
memset(&s,c,sizeof(struct mystruct));
|
||||
|
||||
if(s.y=='A')
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
return 1;
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
CORE
|
||||
main.c
|
||||
--cover location --unwind 10
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^\*\* 4 of 4 covered
|
||||
--
|
||||
^warning: ignoring
|
||||
^\[.*<builtin-library-
|
|
@ -0,0 +1,14 @@
|
|||
#include <stdio.h>
|
||||
|
||||
int main()
|
||||
{
|
||||
const char *s="test";
|
||||
int ret=puts(s); //return value is nondet (internal to built-in, thus non-controllable)
|
||||
|
||||
if(ret<0)
|
||||
{
|
||||
return 1;
|
||||
}
|
||||
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
CORE
|
||||
main.c
|
||||
--cover location --unwind 10
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^\*\* 4 of 4 covered
|
||||
--
|
||||
^warning: ignoring
|
||||
^\[.*<builtin-library-
|
|
@ -0,0 +1,17 @@
|
|||
int main()
|
||||
{
|
||||
char a[10];
|
||||
__CPROVER_input("a[3]", a[3]);
|
||||
|
||||
int len = strlen(a);
|
||||
|
||||
if(len==3)
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
else if(len==4)
|
||||
{
|
||||
return -1;
|
||||
}
|
||||
return 1;
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
CORE
|
||||
main.c
|
||||
--cover branch --unwind 5
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^\*\* 5 of 5 covered
|
||||
--
|
||||
^warning: ignoring
|
||||
^\[.*<builtin-library-
|
|
@ -0,0 +1,17 @@
|
|||
int main()
|
||||
{
|
||||
char a[10];
|
||||
__CPROVER_input("a[3]", a[3]);
|
||||
|
||||
int len = strlen(a);
|
||||
|
||||
if(len==3)
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
else if(len==4)
|
||||
{
|
||||
return -1;
|
||||
}
|
||||
return 1;
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
CORE
|
||||
main.c
|
||||
--cover condition --unwind 5
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^\*\* 4 of 4 covered
|
||||
--
|
||||
^warning: ignoring
|
||||
^\[.*<builtin-library-
|
|
@ -0,0 +1,17 @@
|
|||
int main()
|
||||
{
|
||||
char a[10];
|
||||
__CPROVER_input("a[3]", a[3]);
|
||||
|
||||
int len = strlen(a);
|
||||
|
||||
if(len==3)
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
else if(len==4)
|
||||
{
|
||||
return -1;
|
||||
}
|
||||
return 1;
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
CORE
|
||||
main.c
|
||||
--cover decision --unwind 5
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^\*\* 4 of 4 covered
|
||||
--
|
||||
^warning: ignoring
|
||||
^\[.*<builtin-library-
|
|
@ -0,0 +1,17 @@
|
|||
int main()
|
||||
{
|
||||
char a[10];
|
||||
__CPROVER_input("a[3]", a[3]);
|
||||
|
||||
int len = strlen(a);
|
||||
|
||||
if(len==3)
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
else if(len==4)
|
||||
{
|
||||
return -1;
|
||||
}
|
||||
return 1;
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
CORE
|
||||
main.c
|
||||
--cover mcdc --unwind 5
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^\*\* 4 of 4 covered
|
||||
--
|
||||
^warning: ignoring
|
||||
^\[.*<builtin-library-
|
Loading…
Reference in New Issue