-
Notifications
You must be signed in to change notification settings - Fork 24
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Improvements to the shape abstract domain and to memory safety analysis #120
Changes from 62 commits
64daeeb
5f59a7d
424cf5e
b624ec9
942511d
5e6503e
66a12ca
26684c8
4af058e
5859255
7c5cada
b3eff2a
cf4c5e3
5ba86f4
1a282c0
7ade32c
8705014
18b148b
0be684c
06e0128
0ce8606
42afc71
ebb2d97
56210f3
1fdd369
d04098e
d6428b5
4cb88ab
ff40be0
2bfac82
6524bf1
4863739
99d6003
0c8a3ab
6b2d154
4b20b5d
67bc0fc
328499c
df862c9
970b11b
f665fb1
c3ab3f3
7ae8727
154bb4c
cf39cd2
0cbf7de
37d74d7
735e5c4
16ffaa1
6b67494
b414e3c
14bad7b
c75c8d4
bc085cd
719684c
4fe5103
dd533c8
54c9a2e
d70047e
40facd1
9572ea2
c9a7d89
c71334c
d022890
ed80b24
556c9c7
9104bda
cbb660c
d938e3e
215ab5d
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
default: tests.log | ||
|
||
FLAGS = --verbosity 10 | ||
|
||
test: | ||
@../test.pl -p -c "../../../src/2ls/2ls $(FLAGS)" | ||
|
||
tests.log: ../test.pl | ||
@../test.pl -p -c "../../../src/2ls/2ls $(FLAGS)" | ||
|
||
show: | ||
@for dir in *; do \ | ||
if [ -d "$$dir" ]; then \ | ||
vim -o "$$dir/*.c" "$$dir/*.out"; \ | ||
fi; \ | ||
done; | ||
|
||
clean: | ||
@rm -f *.log | ||
@for dir in *; do rm -f $$dir/*.out; done; |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
extern int __VERIFIER_nondet_int(); | ||
extern void __VERIFIER_error() __attribute__ ((__noreturn__)); | ||
|
||
#include <stdlib.h> | ||
|
||
#define APPEND(l,i) {i->next=l; l=i;} | ||
|
||
typedef struct node { | ||
struct node *next; | ||
int event1; | ||
int event2; | ||
} Node; | ||
|
||
int main() { | ||
Node *l = NULL; | ||
|
||
while (__VERIFIER_nondet_int()) { | ||
int ev1 = __VERIFIER_nondet_int(); | ||
int ev2 = __VERIFIER_nondet_int(); | ||
if (ev1 < 0 || ev1 > 3 || ev2 < 0 || ev2 > 3) | ||
continue; | ||
|
||
if (((ev1 == 0) && (ev2 == 2)) || ((ev1 == 1) && (ev2 == 3)) || ((ev1 == 0) && (ev2 == 3))) | ||
continue; | ||
|
||
Node *p = malloc(sizeof(*p)); | ||
p->event1 = ev1; | ||
p->event2 = ev2; | ||
APPEND(l,p) | ||
} | ||
|
||
Node *i = l; | ||
|
||
while (i != NULL) { | ||
if (((i->event1 == 1) && (i->event2 == 3)) || ((i->event1 == 0) && (i->event2 == 2))) | ||
__VERIFIER_error(); | ||
i = i->next; | ||
} | ||
} | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
CORE | ||
main.c | ||
--heap-values-incremental --sympath --inline | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'm not sure There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I changed the name to -refine. I suggest we leave implementation of a more generic solution with --refine-domains switch to Matej as a part of his work on generic domain combinations. This is closely related to it and I think it should be designed all together. |
||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,46 @@ | ||
extern int __VERIFIER_nondet_int(); | ||
extern void __VERIFIER_error() __attribute__ ((__noreturn__)); | ||
|
||
#include <stdlib.h> | ||
|
||
#define APPEND(l,i) {i->next=l; l=i;} | ||
|
||
typedef struct node { | ||
struct node *next; | ||
int stock; | ||
int order; | ||
} Node; | ||
|
||
int main() { | ||
Node *l = NULL; | ||
|
||
while (__VERIFIER_nondet_int()) { | ||
int stock = __VERIFIER_nondet_int(); | ||
if (stock < 0) | ||
continue; | ||
|
||
Node *p = malloc(sizeof(*p)); | ||
p->stock = stock; | ||
p->order = 0; | ||
APPEND(l,p) | ||
} | ||
|
||
Node *i = l; | ||
while (i != NULL) { | ||
int order = __VERIFIER_nondet_int(); | ||
if (order < 0 || i->stock < order) | ||
continue; | ||
i->order = order; | ||
i->stock = i->stock; | ||
i = i->next; | ||
} | ||
|
||
|
||
i = l; | ||
while (i != NULL) { | ||
if (i->order > i->stock) | ||
__VERIFIER_error(); | ||
i = i->next; | ||
} | ||
} | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
CORE | ||
main.c | ||
--heap-values-incremental --sympath --inline | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,42 @@ | ||
extern int __VERIFIER_nondet_int(); | ||
extern void __VERIFIER_error() __attribute__ ((__noreturn__)); | ||
|
||
#include <stdlib.h> | ||
|
||
#define INTERVAL_SIZE 100 | ||
|
||
struct node { | ||
int hash; | ||
struct node *next; | ||
}; | ||
|
||
int hash_fun(); | ||
|
||
void append_to_list(struct node **list, int hash) { | ||
struct node *node = malloc(sizeof(*node)); | ||
node->next = *list; | ||
node->hash = hash; | ||
*list = node; | ||
} | ||
|
||
int main() { | ||
struct node *list = NULL; | ||
|
||
int base = __VERIFIER_nondet_int(); | ||
|
||
while (__VERIFIER_nondet_int()) { | ||
if (base >= 0 && base <= 1000000) { | ||
base = base; | ||
int hash = hash_fun(); | ||
|
||
if (hash > base && hash < base + INTERVAL_SIZE) | ||
append_to_list(&list, hash); | ||
} | ||
} | ||
|
||
while (list) { | ||
if (!(list->hash >= base && list->hash < base + INTERVAL_SIZE)) | ||
__VERIFIER_error(); | ||
list = list->next; | ||
} | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
CORE | ||
main.c | ||
--heap-values-incremental --sympath --inline | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
extern int __VERIFIER_nondet_int(); | ||
extern void __VERIFIER_error() __attribute__ ((__noreturn__)); | ||
|
||
#include <stdlib.h> | ||
#include <limits.h> | ||
|
||
#define APPEND(l,i) {i->next=l; l=i;} | ||
|
||
typedef struct node { | ||
struct node *next; | ||
int val; | ||
} Node; | ||
|
||
int main() { | ||
Node *l = NULL; | ||
int min = INT_MAX, max = -INT_MAX; | ||
|
||
while (__VERIFIER_nondet_int()) { | ||
Node *p = malloc(sizeof(*p)); | ||
p->val = __VERIFIER_nondet_int(); | ||
APPEND(l, p) | ||
|
||
if (min > p->val) { | ||
min = p->val; | ||
} | ||
if (max < p->val) { | ||
max = p->val; | ||
} | ||
|
||
} | ||
|
||
Node *i = l; | ||
while (i != NULL) { | ||
if (i->val < min) | ||
__VERIFIER_error(); | ||
if (i->val > max) | ||
__VERIFIER_error(); | ||
i = i->next; | ||
} | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
CORE | ||
main.c | ||
--heap-values-incremental --sympath --inline | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,81 @@ | ||
extern unsigned __VERIFIER_nondet_uint(); | ||
extern int __VERIFIER_nondet_int(); | ||
extern char *__VERIFIER_nondet_charp(); | ||
extern void __VERIFIER_error() __attribute__ ((__noreturn__)); | ||
|
||
#include <stdlib.h> | ||
|
||
#define LOW 0 | ||
#define HIGH 1 | ||
|
||
typedef struct packet { | ||
unsigned size; | ||
unsigned prio; | ||
char *payload; | ||
} Packet; | ||
|
||
typedef struct packet_list_node { | ||
struct packet packet; | ||
struct packet_list_node *next; | ||
} *Node; | ||
|
||
struct packet_queue { | ||
struct packet_list_node *front; | ||
}; | ||
|
||
|
||
Packet receive() { | ||
Packet packet; | ||
packet.size = __VERIFIER_nondet_uint(); | ||
packet.prio = __VERIFIER_nondet_int() ? LOW : HIGH; | ||
packet.payload = __VERIFIER_nondet_charp(); | ||
return packet; | ||
} | ||
|
||
extern void send(struct packet p); | ||
|
||
void append_to_queue(Packet p, Node *q) { | ||
Node node = malloc(sizeof(*node)); | ||
node->packet = p; | ||
node->next = *q; | ||
*q = node; | ||
} | ||
|
||
void process_prio_queue(Node q) { | ||
for (Node node = q; node != NULL; node = node->next) { | ||
if (!(node->packet.prio == HIGH || node->packet.size < 500)) | ||
__VERIFIER_error(); | ||
send(node->packet); | ||
} | ||
} | ||
|
||
void process_normal_queue(Node q) { | ||
for (Node node = q; node != NULL; node = node->next) { | ||
if (!(node->packet.prio == LOW && node->packet.size >= 500)) | ||
__VERIFIER_error(); | ||
send(node->packet); | ||
} | ||
} | ||
|
||
int main() { | ||
Node prio_queue = NULL; | ||
Node normal_queue = NULL; | ||
|
||
while (__VERIFIER_nondet_int()) { | ||
Packet new_packet = receive(); | ||
if (new_packet.size > 0) { | ||
if (new_packet.prio == HIGH) { | ||
append_to_queue(new_packet, &prio_queue); | ||
} else if (new_packet.size < 500) { | ||
append_to_queue(new_packet, &prio_queue); | ||
} else { | ||
append_to_queue(new_packet, &normal_queue); | ||
} | ||
} | ||
} | ||
|
||
process_prio_queue(prio_queue); | ||
process_normal_queue(normal_queue); | ||
|
||
return 0; | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
THOROUGH | ||
main.c | ||
--heap-values-incremental --sympath --inline | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,69 @@ | ||
extern int __VERIFIER_nondet_int(); | ||
extern void __VERIFIER_error() __attribute__ ((__noreturn__)); | ||
|
||
#include <stdlib.h> | ||
|
||
#define MAX_PROC 1000 | ||
|
||
struct process_node { | ||
int process_id; | ||
int time_to_wait; | ||
|
||
struct process_node *next; | ||
}; | ||
|
||
extern void run_process(int id); | ||
|
||
void append_to_queue(struct process_node *n, struct process_node **q) { | ||
n->next = *q; | ||
*q = n; | ||
} | ||
|
||
struct process_node *choose_next(struct process_node **q) { | ||
struct process_node *node = *q; | ||
struct process_node *prev = NULL; | ||
struct process_node *result = NULL; | ||
while (node != NULL) { | ||
if (node->time_to_wait == 1) { | ||
result = node; | ||
if (prev == NULL) | ||
*q = node->next; | ||
else | ||
prev->next = node->next; | ||
} else { | ||
node->time_to_wait--; | ||
} | ||
prev = node; | ||
node = node->next; | ||
} | ||
return result; | ||
} | ||
|
||
void check_queue(struct process_node *q) { | ||
for (struct process_node *n = q; n != NULL; n = n->next) | ||
if (!n->time_to_wait >= 1) | ||
__VERIFIER_error(); | ||
} | ||
|
||
|
||
int main() { | ||
struct process_node *queue = NULL; | ||
int next_time = 1; | ||
|
||
while (__VERIFIER_nondet_int()) { | ||
if (next_time < MAX_PROC && __VERIFIER_nondet_int()) { | ||
int new_id = __VERIFIER_nondet_int(); | ||
|
||
struct process_node *new_process = malloc(sizeof(*new_process)); | ||
new_process->process_id = __VERIFIER_nondet_int(); | ||
new_process->time_to_wait = next_time++; | ||
append_to_queue(new_process, &queue); | ||
} else if (next_time > 1){ | ||
struct process_node *p = choose_next(&queue); | ||
next_time--; | ||
run_process(p->process_id); | ||
} | ||
|
||
check_queue(queue); | ||
} | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
CORE | ||
main.c | ||
--heap-values-incremental --sympath --inline | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Put every directory on a separate line