Skip to content

Commit 6cffb45

Browse files
author
Daniel Kroening
authored
Merge pull request #479 from lucasccordeiro/regression-full-slice
Added regression tests for checking the full-slice option
2 parents 99ee469 + e823d4b commit 6cffb45

File tree

42 files changed

+894
-0
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

42 files changed

+894
-0
lines changed

‎regression/goto-instrument/slice01/main.c

+70
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
#include <stdio.h>
2+
#include <stdlib.h>
3+
#include <assert.h>
4+
5+
typedef struct list
6+
{
7+
int key;
8+
struct list *next;
9+
} mlist;
10+
11+
mlist *head;
12+
13+
mlist* search_list(mlist *l, int k)
14+
{
15+
l = head;
16+
while(l!=NULL && l->key!=k)
17+
{
18+
l = l->next;
19+
}
20+
return l;
21+
}
22+
23+
int delete_list(mlist *l)
24+
{
25+
mlist *tmp;
26+
tmp = head;
27+
if (head != l)
28+
{
29+
while(tmp->next!=l)
30+
tmp = tmp->next;
31+
tmp->next = l->next;
32+
}
33+
else
34+
{
35+
head = l->next;
36+
}
37+
free(l);
38+
return 0;
39+
}
40+
41+
int insert_list(mlist *l, int k)
42+
{
43+
l = (mlist*)malloc(sizeof(mlist));
44+
if (head==NULL)
45+
{
46+
l->key = k;
47+
l->next = NULL;
48+
}
49+
else
50+
{
51+
l->key = k;
52+
l->next = head;
53+
}
54+
head = l;
55+
return 0;
56+
}
57+
58+
int main(void)
59+
{
60+
int i;
61+
mlist *mylist, *temp;
62+
insert_list(mylist,2);
63+
insert_list(mylist,5);
64+
insert_list(mylist,1);
65+
insert_list(mylist,3);
66+
mylist = head;
67+
temp = search_list(mylist,2);
68+
assert(temp->key == 2);
69+
delete_list(temp);
70+
}

‎regression/goto-instrument/slice01/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
main.c
3+
--unwind 2 --full-slice
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/goto-instrument/slice02/main.c

+73
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
#include <stdio.h>
2+
3+
#define TRUE (1)
4+
#define FALSE (0)
5+
#define SIZE (10)
6+
int topo=0;
7+
8+
void inc_topo(void){
9+
topo++;
10+
}
11+
12+
void dec_topo(void){
13+
topo--;
14+
}
15+
16+
int get_topo(void){
17+
return topo;
18+
}
19+
20+
int stack_empty(void){
21+
(topo==0) ? TRUE : FALSE;
22+
}
23+
24+
int push(int *stack, int x){
25+
if (topo==SIZE) {
26+
printf("stack overflow\n");
27+
return -1;
28+
} else {
29+
stack[get_topo()] = x;
30+
printf("push: stack[%d] = %d\n", get_topo(), stack[get_topo()]);
31+
inc_topo();
32+
}
33+
}
34+
35+
int pop(int *stack){
36+
if (get_topo()==0) {
37+
printf("stack underflow\n");
38+
return -1;
39+
} else {
40+
dec_topo();
41+
printf("pop: stack[%d] = %d\n", get_topo(), stack[get_topo()]);
42+
return stack[get_topo()];
43+
}
44+
}
45+
46+
int main(void) {
47+
int arr[SIZE];
48+
49+
push(arr,3);
50+
push(arr,4);
51+
push(arr,5);
52+
push(arr,1);
53+
push(arr,9);
54+
push(arr,10);
55+
push(arr,6);
56+
push(arr,12);
57+
push(arr,15);
58+
push(arr,8);
59+
push(arr,20);
60+
61+
pop(arr);
62+
pop(arr);
63+
pop(arr);
64+
pop(arr);
65+
pop(arr);
66+
pop(arr);
67+
pop(arr);
68+
pop(arr);
69+
pop(arr);
70+
pop(arr);
71+
pop(arr);
72+
73+
}

‎regression/goto-instrument/slice02/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--pointer-check --full-slice
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/goto-instrument/slice03/main.c

+102
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
#include <stdio.h>
2+
3+
#define SIZE 10
4+
5+
typedef struct{
6+
int elemento[SIZE];
7+
int inicio;
8+
int fim;
9+
int quantidade;
10+
} QType;
11+
12+
int inicializa(QType *q) {
13+
q->inicio=0;
14+
q->fim=0;
15+
q->quantidade=0;
16+
}
17+
18+
int empty(QType * q) {
19+
if (q->inicio == q->fim) {
20+
printf("queue is empty\n");
21+
return -1;
22+
}
23+
else return 0;
24+
}
25+
26+
int full(QType * q) {
27+
28+
if (q->quantidade == SIZE) {
29+
printf("queue is full\n");
30+
return -1;
31+
} else{
32+
return 0;
33+
}
34+
}
35+
36+
int enqueue(QType *q, int x) {
37+
q->elemento[q->fim] = x;
38+
q->quantidade++;
39+
if (q->fim == SIZE) {
40+
q->fim = 0;
41+
} else {
42+
q->fim++;
43+
}
44+
return 0;
45+
}
46+
47+
int dequeue(QType *q) {
48+
49+
int x;
50+
51+
x = q->elemento[q->inicio];
52+
q->quantidade--;
53+
if (q->inicio == SIZE) {
54+
q->inicio = 0;
55+
} else {
56+
q->inicio++;
57+
}
58+
59+
return x;
60+
}
61+
62+
63+
int main(void) {
64+
65+
QType queue;
66+
67+
int i,temp;
68+
69+
inicializa(&queue);
70+
71+
empty(&queue);
72+
73+
enqueue(&queue,2);
74+
75+
empty(&queue);
76+
77+
enqueue(&queue,4);
78+
enqueue(&queue,1);
79+
enqueue(&queue,5);
80+
enqueue(&queue,3);
81+
enqueue(&queue,8);
82+
enqueue(&queue,6);
83+
enqueue(&queue,7);
84+
enqueue(&queue,10);
85+
enqueue(&queue,9);
86+
87+
full(&queue);
88+
89+
temp = dequeue(&queue);
90+
91+
printf("temp = %d\n", temp);
92+
93+
temp = dequeue(&queue);
94+
95+
printf("temp = %d\n", temp);
96+
97+
for(i=queue.inicio; i<queue.fim; i++){
98+
printf("queue[%d] = %d\n", i, queue.elemento[i]);
99+
}
100+
101+
return 0;
102+
}

‎regression/goto-instrument/slice03/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--unwind 10 --pointer-check --bounds-check --full-slice
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/goto-instrument/slice04/main.c

+58
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
/*
2+
** float-rounder-bug.c
3+
**
4+
** Martin Brain
5+
** [email protected]
6+
** 20/05/13
7+
**
8+
** Another manifestation of the casting bug.
9+
** If the number is in (0,0x1p-126) it is rounded to zero rather than a subnormal number.
10+
*/
11+
#include <assert.h>
12+
13+
#define FULP 1
14+
15+
void bug (float min) {
16+
__CPROVER_assume(min == 0x1.fffffep-105f);
17+
float modifier = (0x1.0p-23 * (1<<FULP));
18+
float ulpdiff = min * modifier;
19+
20+
assert(ulpdiff == 0x1p-126f); // Should be true
21+
22+
return;
23+
}
24+
25+
void bugBrokenOut (float min) {
26+
__CPROVER_assume(min == 0x1.fffffep-105f);
27+
float modifier = (0x1.0p-23 * (1<<FULP));
28+
double dulpdiff = (double)min * (double)modifier; // Fine up to here
29+
float ulpdiff = (float)dulpdiff; // Error
30+
31+
assert(ulpdiff == 0x1p-126f); // Should be true
32+
33+
return;
34+
}
35+
36+
void bugCasting (double d) {
37+
__CPROVER_assume(d == 0x1.fffffep-127);
38+
39+
float f = (float) d;
40+
41+
assert(f == 0x1p-126f); // Should be true
42+
43+
return;
44+
}
45+
46+
int main (void) {
47+
float f;
48+
bug(f);
49+
50+
float g;
51+
bugBrokenOut(g);
52+
53+
double d;
54+
bugCasting(d);
55+
56+
return 1;
57+
}
58+

‎regression/goto-instrument/slice04/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--full-slice
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/goto-instrument/slice05/main.c

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
int main()
2+
{
3+
int x = 1; /* considering changing this line */
4+
int y = 3;
5+
int p = x + y;
6+
int z = y -2;
7+
int r = 0;
8+
9+
if(p==0)
10+
r++;
11+
12+
assert(r==0);
13+
14+
return 0;
15+
}

‎regression/goto-instrument/slice05/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--full-slice
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/goto-instrument/slice06/main.c

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#define N 10
2+
3+
int main()
4+
{
5+
int i;
6+
int sum = 0;
7+
int product = 1;
8+
for(i = 1; i < N; ++i) {
9+
sum = sum + i;
10+
product = product * i;
11+
}
12+
assert(sum>0);
13+
14+
return 0;
15+
}

‎regression/goto-instrument/slice06/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--full-slice
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

0 commit comments

Comments
 (0)