Siemens fix260 squashed (do not merge)

regression/cbmc-slice/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;

regression/cbmc-slice/slice01/main.c

@@ -0,0 +1,70 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+
+typedef struct list 
+{
+  int key;
+  struct list *next;
+} mlist;
+
+mlist *head;
+
+mlist* search_list(mlist *l, int k)
+{
+  l = head;
+  while(l!=NULL && l->key!=k)
+  {
+    l = l->next;
+  }
+  return l;
+}
+
+int delete_list(mlist *l)
+{
+  mlist *tmp;
+  tmp = head;
+  if (head != l)
+  {
+    while(tmp->next!=l)
+      tmp = tmp->next;
+      tmp->next = l->next;
+  }
+  else
+  {
+    head = l->next;
+  }
+  free(l);
+  return 0;
+}
+
+int insert_list(mlist *l, int k)
+{
+  l = (mlist*)malloc(sizeof(mlist));
+  if (head==NULL)
+  {
+    l->key = k;
+    l->next = NULL;
+  }
+  else
+  {
+    l->key = k;
+    l->next = head;
+  }
+  head = l;
+  return 0;
+}
+
+int main(void)
+{
+  int i;
+  mlist *mylist, *temp;
+  insert_list(mylist,2);
+  insert_list(mylist,5);
+  insert_list(mylist,1);
+  insert_list(mylist,3);
+  mylist = head;
+  temp = search_list(mylist,2);
+  assert(temp->key == 2);
+  delete_list(temp);
+}

regression/cbmc-slice/slice01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 2 --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-slice/slice02/main.c

@@ -0,0 +1,73 @@
+#include <stdio.h>
+
+#define TRUE	(1)
+#define FALSE	(0) 
+#define SIZE	(10)
+int topo=0;
+
+void inc_topo(void){
+	topo++;
+}
+
+void dec_topo(void){
+	topo--;
+}
+
+int get_topo(void){
+	return topo;
+}
+
+int stack_empty(void){
+	(topo==0) ? TRUE : FALSE; 
+}
+
+int push(int *stack, int x){
+	if (topo==SIZE) {
+		printf("stack overflow\n");
+		return -1;
+	} else {
+		stack[get_topo()] = x;
+		printf("push: stack[%d] = %d\n", get_topo(), stack[get_topo()]);
+		inc_topo();
+	}
+}
+
+int pop(int *stack){
+	if (get_topo()==0) {
+		printf("stack underflow\n");	
+		return -1;
+	} else {
+		dec_topo();
+		printf("pop: stack[%d] = %d\n", get_topo(), stack[get_topo()]);
+		return stack[get_topo()];  
+	}
+}
+
+int main(void) {
+	int arr[SIZE];
+
+	push(arr,3);
+	push(arr,4);
+	push(arr,5);
+	push(arr,1);
+	push(arr,9);
+	push(arr,10);
+	push(arr,6);
+	push(arr,12);
+	push(arr,15);
+	push(arr,8);
+	push(arr,20);
+
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+	pop(arr);
+
+}

regression/cbmc-slice/slice02/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-slice/slice03/main.c

@@ -0,0 +1,102 @@
+#include <stdio.h>
+
+#define SIZE 10
+
+typedef struct{
+    int elemento[SIZE];
+    int inicio;
+    int fim;
+    int quantidade;
+} QType;
+
+int inicializa(QType *q) {
+	q->inicio=0;
+	q->fim=0;
+	q->quantidade=0;
+}
+
+int empty(QType * q) {
+  if (q->inicio == q->fim) { 
+	printf("queue is empty\n");
+    return -1;
+  }
+  else return 0;
+}
+
+int full(QType * q) {
+
+	if (q->quantidade == SIZE) {  
+		printf("queue is full\n");
+		return -1;
+	} else{
+		return 0;
+	}
+}
+
+int enqueue(QType *q, int x) {
+	q->elemento[q->fim] = x;
+	q->quantidade++;
+	if (q->fim == SIZE) {
+		q->fim = 0;
+	} else {
+		q->fim++;
+	}
+	return 0;
+}
+
+int dequeue(QType *q) {
+
+	int x;
+
+	x = q->elemento[q->inicio];
+	q->quantidade--;
+	if (q->inicio == SIZE) {
+		q->inicio = 0;
+	} else { 
+		q->inicio++;
+	}
+
+	return x;
+}
+
+
+int main(void) {
+
+	QType queue;
+
+	int i,temp;
+
+	inicializa(&queue);
+
+	empty(&queue);
+
+	enqueue(&queue,2);
+
+	empty(&queue);
+
+	enqueue(&queue,4);
+	enqueue(&queue,1);
+	enqueue(&queue,5);
+	enqueue(&queue,3);
+	enqueue(&queue,8);
+	enqueue(&queue,6);
+	enqueue(&queue,7);
+	enqueue(&queue,10);
+	enqueue(&queue,9);
+
+	full(&queue);
+
+	temp = dequeue(&queue);
+
+	printf("temp = %d\n", temp);
+
+	temp = dequeue(&queue);
+
+	printf("temp = %d\n", temp);
+
+	for(i=queue.inicio; i<queue.fim; i++){
+		printf("queue[%d] = %d\n", i, queue.elemento[i]);
+	}
+
+	return 0;
+}

regression/cbmc-slice/slice03/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 10 --pointer-check --bounds-check --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-slice/slice04/main.c

@@ -0,0 +1,58 @@
+/*
+** float-rounder-bug.c
+**
+** Martin Brain
+** [email protected]
+** 20/05/13
+**
+** Another manifestation of the casting bug.
+** If the number is in (0,0x1p-126) it is rounded to zero rather than a subnormal number.
+*/
+#include <assert.h>
+
+#define FULP 1
+
+void bug (float min) {
+  __CPROVER_assume(min == 0x1.fffffep-105f);
+  float modifier = (0x1.0p-23 * (1<<FULP));
+  float ulpdiff = min * modifier;
+
+  assert(ulpdiff == 0x1p-126f);    // Should be true
+
+  return;
+}
+
+void bugBrokenOut (float min) {
+  __CPROVER_assume(min == 0x1.fffffep-105f);
+  float modifier = (0x1.0p-23 * (1<<FULP));
+  double dulpdiff = (double)min * (double)modifier;  // Fine up to here
+  float ulpdiff = (float)dulpdiff;  // Error
+
+  assert(ulpdiff == 0x1p-126f); // Should be true
+
+  return;
+}
+
+void bugCasting (double d) {
+  __CPROVER_assume(d == 0x1.fffffep-127);
+
+  float f = (float) d;
+
+  assert(f == 0x1p-126f); // Should be true
+
+  return;
+}
+
+int main (void) {
+  float f;
+  bug(f);
+
+  float g;
+  bugBrokenOut(g);
+
+  double d;
+  bugCasting(d);
+
+  return 1;
+}
+

regression/cbmc-slice/slice04/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-slice/slice05/main.c

@@ -0,0 +1,15 @@
+int main()
+{
+  int x = 1; /* considering changing this line */
+  int y = 3;
+  int p = x + y;
+  int z = y -2;
+  int r = 0;
+
+  if(p==0)
+  r++;
+
+  assert(r==0);
+
+  return 0;
+}

regression/cbmc-slice/slice05/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring