Unwind using GOTO unwinder

regression/heap-data/calendar_false/main.c

@@ -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 == 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;
+    }
+}
+

regression/heap-data/calendar_false/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--heap --values-refine --k-induction
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

regression/heap-data/min_max_false/main.c

@@ -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;
+    }
+}

regression/heap-data/min_max_false/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--heap --values-refine --k-induction
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

regression/heap-data/packet_filter_false/main.c

@@ -0,0 +1,87 @@
+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;
+    unsigned index;
+    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;
+    static unsigned index = 0;
+    index++;
+    packet.size = __VERIFIER_nondet_uint();
+    packet.prio = __VERIFIER_nondet_int() ? LOW : HIGH;
+    packet.payload = __VERIFIER_nondet_charp();
+    packet.index = index;
+    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.index > 4) {
+              append_to_queue(new_packet, &prio_queue);
+            } else 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;
+}

regression/heap-data/packet_filter_false/test.desc

@@ -0,0 +1,6 @@
+THOROUGH
+main.c
+--heap --values-refine --k-induction
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

regression/heap-data/running_example_assume/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --heap --values-refine
 ^EXIT=0$

regression/heap-data/running_example_false/main.c

@@ -0,0 +1,35 @@
+extern int __VERIFIER_nondet_int();
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+
+#include <stdlib.h>
+
+typedef struct node {
+    int val;
+    struct node *next;
+} Node;
+
+int main() {
+    Node *p, *list = malloc(sizeof(*list));
+    Node *tail = list;
+    list->next = NULL;
+    list->val = 10;
+    while (__VERIFIER_nondet_int()) {
+        int x;
+        if (x < 10 || x > 20) continue;
+        p = malloc(sizeof(*p));
+        tail->next = p;
+        p->next = NULL;
+        p->val = x;
+        tail = p;
+    }
+
+    while (1) {
+        for (p = list; p!= NULL; p = p->next) {
+            if (!(p->val <= 20 && p->val >= 10))
+                __VERIFIER_error();
+            if (p->val < 20) p->val--;
+            else p->val /= 2;
+        }
+    }
+}
+

regression/heap-data/running_example_false/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--heap --values-refine --k-induction
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

regression/heap-data/shared_mem1_false/main.c

@@ -0,0 +1,51 @@
+extern int __VERIFIER_nondet_int();
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+
+#include <stdlib.h>
+
+struct mem {
+    int val;
+};
+
+struct list_node {
+    int x;
+    struct mem *mem;
+    struct list_node *next;
+};
+
+int main() {
+    struct mem *m = malloc(sizeof(*m));
+    m->val = 100;
+
+    struct list_node *head = malloc(sizeof(*head));
+    head->x = 1;
+    head->mem = m;
+    head->next = head;
+
+    struct list_node *list = head;
+
+    int i = 0;
+    while (__VERIFIER_nondet_int()) {
+        int x = __VERIFIER_nondet_int();
+        if (x > 0 && x < 10) {
+            struct list_node *n = malloc(sizeof(*n));
+            n->x = x+i;
+            n->mem = m;
+            n->next = head;
+            list->next = n;
+            i++;
+        }
+    }
+
+    list = head;
+    while (list) {
+        if (list->mem->val <= 100)
+            list->mem->val += list->x;
+        else
+            list->mem->val -= list->x;
+        list = list->next;
+
+        if (!(m->val > 90 && m->val < 110))
+            __VERIFIER_error();
+    }
+}

regression/heap-data/shared_mem1_false/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--heap --values-refine --k-induction
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

regression/heap-data/shared_mem2/main.c

@@ -1,4 +1,5 @@
 extern int __VERIFIER_nondet_int();
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
 
 #include <stdlib.h>
 
@@ -41,5 +42,5 @@ int main() {
         list = list->next;
     }
     if (!(m->val == 100))
-        __VERIFIER_nondet_int();
+        __VERIFIER_error();
 }

regression/heap/array_unwind1/test.desc

@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 main.c
---incremental-bmc --heap-interval
+--incremental-bmc --heap --intervals
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\[main\.assertion\.1\] assertion \*a\[0\]==0: OK
+^\[main\.assertion\.1\] assertion \*a\[0\]==0: SUCCESS
 ^\[main\.assertion\.2\] assertion \*a\[1\]==2: FAILURE

regression/heap/array_unwind2/test.desc

@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 main.c
---incremental-bmc --heap-interval
+--incremental-bmc --heap --intervals
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 ^\[main\.assertion\.1\] assertion \*a\[0\]==1: FAILURE
-^\[main\.assertion\.2\] assertion \*a\[1\]==1: OK
+^\[main\.assertion\.2\] assertion \*a\[1\]==1: SUCCESS

regression/heap/list_iter1/test.desc

@@ -1,10 +1,10 @@
-KNOWNBUG
+CORE
 main.c
---incremental-bmc --independent-properties --heap-interval
+--incremental-bmc --independent-properties --heap --intervals
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\[main\.assertion\.1\] assertion l->n->x==0: OK
+^\[main\.assertion\.1\] assertion l->n->x==0: SUCCESS
 ^\[main\.assertion\.2\] assertion l->n->x==1: FAILURE
 ^\[main\.assertion\.3\] assertion l->x==2: FAILURE
-^\[main\.assertion\.4\] assertion l->x==1: OK
+^\[main\.assertion\.4\] assertion l->x==1: SUCCESS

regression/heap/list_iter2/test.desc

@@ -1,10 +1,10 @@
-KNOWNBUG
+CORE
 main.c
---incremental-bmc --independent-properties --heap-interval
+--incremental-bmc --independent-properties --heap --intervals
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\[main\.assertion\.1\] assertion l->n->x==0: OK
-^\[main\.assertion\.2\] assertion l->n->x==1: FAILURE
+^\[main\.assertion\.1\] assertion l->n->x==0: FAILURE
+^\[main\.assertion\.2\] assertion l->n->x==1: SUCCESS
 ^\[main\.assertion\.3\] assertion l->x==2: FAILURE
-^\[main\.assertion\.4\] assertion l->x==1: OK
+^\[main\.assertion\.4\] assertion l->x==1: FAILURE

regression/heap/list_iter3/main.c

@@ -9,7 +9,7 @@ struct list
 
 void main()
 {
-  struct list *l;
+  struct list *l=NULL;
   struct list *nl1=malloc(sizeof(struct list));
   nl1->x=-1;
   nl1->n=l;

regression/heap/list_iter3/test.desc

@@ -1,10 +1,10 @@
-KNOWNBUG
+CORE
 main.c
---incremental-bmc --independent-properties --heap-interval
+--incremental-bmc --independent-properties --heap --intervals
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\[main\.assertion\.1\] assertion l->n->x==0: OK
-^\[main\.assertion\.2\] assertion l->n->x==1: FAILURE
+^\[main\.assertion\.1\] assertion l->n->x==0: FAILURE
+^\[main\.assertion\.2\] assertion l->n->x==1: SUCCESS
 ^\[main\.assertion\.3\] assertion l->x==2: FAILURE
-^\[main\.assertion\.4\] assertion l->x==1: OK
+^\[main\.assertion\.4\] assertion l->x==1: FAILURE