Add regression tests for havoc-ing of function arguments
This commit is contained in:
parent
2c909868d1
commit
15e34b6905
|
@ -0,0 +1,12 @@
|
|||
#include <assert.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
void func(int *p);
|
||||
|
||||
void main()
|
||||
{
|
||||
int *p;
|
||||
p = NULL;
|
||||
|
||||
func(p);
|
||||
}
|
|
@ -0,0 +1,7 @@
|
|||
CORE
|
||||
main.c
|
||||
--generate-function-body func --generate-function-body-options havoc,params:p --pointer-check
|
||||
^SIGNAL=0$
|
||||
^EXIT=0$
|
||||
--
|
||||
^warning: ignoring
|
|
@ -0,0 +1,14 @@
|
|||
#include <assert.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
void func(int *p);
|
||||
|
||||
void main()
|
||||
{
|
||||
int i;
|
||||
i = 0;
|
||||
|
||||
func(&i);
|
||||
|
||||
assert(i == 0);
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
--generate-function-body func --generate-function-body-options havoc,params:p
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
\[main.assertion.1\] line \d+ assertion i == 0: FAILURE
|
||||
--
|
||||
^warning: ignoring
|
|
@ -0,0 +1,33 @@
|
|||
#include <assert.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
typedef struct st1
|
||||
{
|
||||
struct st2 *to_st2;
|
||||
int data;
|
||||
} st1_t;
|
||||
|
||||
typedef struct st2
|
||||
{
|
||||
struct st1 *to_st1;
|
||||
int data;
|
||||
} st2_t;
|
||||
|
||||
st1_t dummy1;
|
||||
st2_t dummy2;
|
||||
|
||||
void func(st1_t *p);
|
||||
|
||||
void main()
|
||||
{
|
||||
st1_t st;
|
||||
|
||||
func(&st);
|
||||
|
||||
assert(st.to_st2 != NULL);
|
||||
assert(st.to_st2->to_st1 != NULL);
|
||||
assert(st.to_st2->to_st1->to_st2 == NULL);
|
||||
|
||||
assert(st.to_st2 != &dummy2);
|
||||
assert(st.to_st2->to_st1 != &dummy1);
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
--generate-function-body func --generate-function-body-options 'havoc,params:p' --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
VERIFICATION SUCCESSFUL
|
||||
--
|
||||
^warning: ignoring
|
|
@ -0,0 +1,19 @@
|
|||
#include <assert.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
typedef struct st
|
||||
{
|
||||
int data;
|
||||
} st_t;
|
||||
|
||||
void func(st_t *p);
|
||||
|
||||
void main()
|
||||
{
|
||||
st_t st;
|
||||
st.data = 0;
|
||||
|
||||
func(&st);
|
||||
|
||||
assert(st.data == 0);
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
--generate-function-body func --generate-function-body-options havoc,params:p
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
\[main.assertion.1\] line \d+ assertion st.data == 0: FAILURE
|
||||
--
|
||||
^warning: ignoring
|
|
@ -0,0 +1,31 @@
|
|||
#include <assert.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
typedef struct st
|
||||
{
|
||||
struct st *next;
|
||||
struct st *prev;
|
||||
int data;
|
||||
} st_t;
|
||||
|
||||
st_t dummy;
|
||||
|
||||
void func(st_t *p);
|
||||
|
||||
void main()
|
||||
{
|
||||
st_t st;
|
||||
|
||||
func(&st);
|
||||
|
||||
assert(st.prev != NULL);
|
||||
assert(st.prev != &dummy);
|
||||
|
||||
assert(st.next != NULL);
|
||||
assert(st.next != &dummy);
|
||||
|
||||
assert(st.prev->prev == NULL);
|
||||
assert(st.prev->next == NULL);
|
||||
assert(st.next->prev == NULL);
|
||||
assert(st.next->next == NULL);
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
--generate-function-body func --generate-function-body-options havoc,params:p --min-null-tree-depth 10 --max-nondet-tree-depth 2 --pointer-check
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
VERIFICATION SUCCESSFUL
|
||||
--
|
||||
^warning: ignoring
|
|
@ -0,0 +1,26 @@
|
|||
#include <assert.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
typedef struct st
|
||||
{
|
||||
struct st *next;
|
||||
int data;
|
||||
} st_t;
|
||||
|
||||
st_t dummy;
|
||||
|
||||
void func(st_t *p);
|
||||
|
||||
void main()
|
||||
{
|
||||
st_t st;
|
||||
|
||||
func(&st);
|
||||
|
||||
assert(st.next != NULL);
|
||||
assert(st.next->next != NULL);
|
||||
assert(st.next->next->next == NULL);
|
||||
|
||||
assert(st.next != &dummy);
|
||||
assert(st.next->next != &dummy);
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
--generate-function-body func --generate-function-body-options havoc,params:p --min-null-tree-depth 10 --max-nondet-tree-depth 3
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
VERIFICATION SUCCESSFUL
|
||||
--
|
||||
^warning: ignoring
|
Loading…
Reference in New Issue