From 97963fff3487c21df81accb95ba6da33d1d123a1 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Wed, 2 Nov 2016 03:42:27 +0000
Subject: [PATCH 01/23] added ignore for input in value_set_fit::apply_code

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/pointer-analysis/value_set_fi.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index d758e40c987..757ed750e54 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -1723,6 +1723,10 @@ void value_set_fit::apply_code(
   {
 	  // doesn't do anything
   }
+  else if(statement==ID_output)
+  {
+    // doesn't do anything
+  }
   else
     throw
       code.pretty()+"\n"+

From 62b3ceae748e963d9eb251fd2d98c7ba04f3524c Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Wed, 2 Nov 2016 03:43:47 +0000
Subject: [PATCH 02/23] do not remove assignments related to
 __CPROVER_initialize

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/goto-instrument/full_slicer.cpp | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 7672036cecf..85f407df097 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/find_symbols.h>
 #include <util/cprover_prefix.h>
+#include <util/prefix.h>
+
 #ifdef DEBUG_FULL_SLICERT
 #include <util/i2string.h>
 #endif
@@ -322,7 +324,7 @@ Function: implicit
 
 \*******************************************************************/
 
-static bool implicit(goto_programt::const_targett target)
+static bool implicit(const namespacet &ns, goto_programt::const_targett target)
 {
   // some variables are used during symbolic execution only
 
@@ -333,7 +335,18 @@ static bool implicit(goto_programt::const_targett target)
 
   const symbol_exprt &s=to_symbol_expr(a.lhs());
 
-  return s.get_identifier()==CPROVER_PREFIX "rounding_mode";
+  if (s.source_location().get_function().empty())
+  {
+    // is it a __CPROVER_* variable?
+    if(has_prefix(id2string(s.get_identifier()), CPROVER_PREFIX))
+	  return true;
+
+    // static lifetime?
+    if(ns.lookup(s.get_identifier()).is_static_lifetime)
+      return true;
+  }
+
+  return false;
 }
 
 /*******************************************************************\
@@ -370,7 +383,7 @@ void full_slicert::operator()(
   {
     if(criterion(e_it->first))
       add_to_queue(queue, e_it->second, e_it->first);
-    else if(implicit(e_it->first))
+    else if(implicit(ns,e_it->first))
       add_to_queue(queue, e_it->second, e_it->first);
     else if((e_it->first->is_goto() && e_it->first->guard.is_true()) ||
             e_it->first->is_throw())
@@ -400,6 +413,9 @@ void full_slicert::operator()(
   Forall_goto_functions(f_it, goto_functions)
     if(f_it->second.body_available())
     {
+   	  if(f_it->first=="pthread_create")
+   		throw "--full-slice does not support C/Pthreads yet";
+
       Forall_goto_program_instructions(i_it, f_it->second.body)
       {
         const cfgt::entryt &e=cfg.entry_map[i_it];

From 80769148ca972b41b9b0055d2cd0c2c4a8393fe5 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Wed, 2 Nov 2016 03:44:48 +0000
Subject: [PATCH 03/23] remove virtual functions, function pointers, and
 returns before building the dependence graph

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/cbmc/cbmc_parse_options.cpp | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 08955180271..db8b60fcb95 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -859,7 +859,20 @@ bool cbmc_parse_optionst::process_goto_program(
     if(cmdline.isset("full-slice"))
     {
       status() << "Performing a full slice" << eom;
-      full_slicer(goto_functions, ns);
+      remove_virtual_functions(symbol_table,goto_functions);
+      remove_function_pointers(symbol_table,goto_functions,false);
+      remove_returns(symbol_table,goto_functions);
+      goto_functions.update();
+      try
+      {
+        full_slicer(goto_functions, ns);
+      }
+
+      catch(const char *error_msg)
+      {
+        error() << error_msg << eom;
+        return 1;
+      }
     }
 
     // do partial inlining

From fa1044139349730f7d0f516501ea96358bddf4f1 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Wed, 2 Nov 2016 03:45:49 +0000
Subject: [PATCH 04/23] add test cases to check the full-slice option

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 regression/cbmc-slice/slice01/main.c    |  70 ++++++++++++++++
 regression/cbmc-slice/slice01/test.desc |  10 +++
 regression/cbmc-slice/slice02/main.c    |  73 +++++++++++++++++
 regression/cbmc-slice/slice02/test.desc |  10 +++
 regression/cbmc-slice/slice03/main.c    | 102 ++++++++++++++++++++++++
 regression/cbmc-slice/slice03/test.desc |  10 +++
 regression/cbmc-slice/slice04/main.c    |  58 ++++++++++++++
 regression/cbmc-slice/slice04/test.desc |  10 +++
 regression/cbmc-slice/slice05/main.c    |  15 ++++
 regression/cbmc-slice/slice05/test.desc |  10 +++
 regression/cbmc-slice/slice06/main.c    |  15 ++++
 regression/cbmc-slice/slice06/test.desc |  10 +++
 regression/cbmc-slice/slice07/main.c    |  50 ++++++++++++
 regression/cbmc-slice/slice07/test.desc |   8 ++
 regression/cbmc-slice/slice08/main.c    |  21 +++++
 regression/cbmc-slice/slice08/test.desc |   8 ++
 regression/cbmc-slice/slice09/main.c    |   9 +++
 regression/cbmc-slice/slice09/test.desc |  10 +++
 regression/cbmc-slice/slice10/main.c    |  18 +++++
 regression/cbmc-slice/slice10/test.desc |  10 +++
 regression/cbmc-slice/slice11/main.c    |  18 +++++
 regression/cbmc-slice/slice11/test.desc |  10 +++
 22 files changed, 555 insertions(+)
 create mode 100644 regression/cbmc-slice/slice01/main.c
 create mode 100644 regression/cbmc-slice/slice01/test.desc
 create mode 100644 regression/cbmc-slice/slice02/main.c
 create mode 100644 regression/cbmc-slice/slice02/test.desc
 create mode 100644 regression/cbmc-slice/slice03/main.c
 create mode 100644 regression/cbmc-slice/slice03/test.desc
 create mode 100644 regression/cbmc-slice/slice04/main.c
 create mode 100644 regression/cbmc-slice/slice04/test.desc
 create mode 100644 regression/cbmc-slice/slice05/main.c
 create mode 100644 regression/cbmc-slice/slice05/test.desc
 create mode 100644 regression/cbmc-slice/slice06/main.c
 create mode 100644 regression/cbmc-slice/slice06/test.desc
 create mode 100644 regression/cbmc-slice/slice07/main.c
 create mode 100644 regression/cbmc-slice/slice07/test.desc
 create mode 100644 regression/cbmc-slice/slice08/main.c
 create mode 100644 regression/cbmc-slice/slice08/test.desc
 create mode 100644 regression/cbmc-slice/slice09/main.c
 create mode 100644 regression/cbmc-slice/slice09/test.desc
 create mode 100644 regression/cbmc-slice/slice10/main.c
 create mode 100644 regression/cbmc-slice/slice10/test.desc
 create mode 100644 regression/cbmc-slice/slice11/main.c
 create mode 100644 regression/cbmc-slice/slice11/test.desc

diff --git a/regression/cbmc-slice/slice01/main.c b/regression/cbmc-slice/slice01/main.c
new file mode 100644
index 00000000000..7502ff7413a
--- /dev/null
+++ b/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);
+}
diff --git a/regression/cbmc-slice/slice01/test.desc b/regression/cbmc-slice/slice01/test.desc
new file mode 100644
index 00000000000..70c57b14a59
--- /dev/null
+++ b/regression/cbmc-slice/slice01/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--unwind 2 --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^size of program expression: 208 steps$
+^simple slicing removed 6 assignments$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice02/main.c b/regression/cbmc-slice/slice02/main.c
new file mode 100644
index 00000000000..8c7aa38de2c
--- /dev/null
+++ b/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);
+
+}
diff --git a/regression/cbmc-slice/slice02/test.desc b/regression/cbmc-slice/slice02/test.desc
new file mode 100644
index 00000000000..36ac80afc72
--- /dev/null
+++ b/regression/cbmc-slice/slice02/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^size of program expression: 678 steps$
+^simple slicing removed 24 assignments$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice03/main.c b/regression/cbmc-slice/slice03/main.c
new file mode 100644
index 00000000000..589c5db2e70
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc-slice/slice03/test.desc b/regression/cbmc-slice/slice03/test.desc
new file mode 100644
index 00000000000..1c925e4c66e
--- /dev/null
+++ b/regression/cbmc-slice/slice03/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--unwind 10 --pointer-check --bounds-check --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^size of program expression: 280 steps$
+^simple slicing removed 16 assignments$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice04/main.c b/regression/cbmc-slice/slice04/main.c
new file mode 100644
index 00000000000..23a87d492c9
--- /dev/null
+++ b/regression/cbmc-slice/slice04/main.c
@@ -0,0 +1,58 @@
+/*
+** float-rounder-bug.c
+**
+** Martin Brain
+** martin.brain@cs.ox.ac.uk
+** 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;
+}
+
diff --git a/regression/cbmc-slice/slice04/test.desc b/regression/cbmc-slice/slice04/test.desc
new file mode 100644
index 00000000000..3c3a608beef
--- /dev/null
+++ b/regression/cbmc-slice/slice04/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--floatbv --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^size of program expression: 62 steps$
+^simple slicing removed 4 assignments$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice05/main.c b/regression/cbmc-slice/slice05/main.c
new file mode 100644
index 00000000000..30e59ce9c7e
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc-slice/slice05/test.desc b/regression/cbmc-slice/slice05/test.desc
new file mode 100644
index 00000000000..b553464bdeb
--- /dev/null
+++ b/regression/cbmc-slice/slice05/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^size of program expression: 38 steps$
+^simple slicing removed 0 assignments$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice06/main.c b/regression/cbmc-slice/slice06/main.c
new file mode 100644
index 00000000000..0bdb68d3c5f
--- /dev/null
+++ b/regression/cbmc-slice/slice06/main.c
@@ -0,0 +1,15 @@
+#define N 10
+
+int main()
+{
+  int i;
+  int sum = 0;
+  int product = 1;
+  for(i = 1; i < N; ++i) {
+    sum = sum + i;
+    product = product * i;
+  }
+  assert(sum>0);
+
+  return 0;
+}
diff --git a/regression/cbmc-slice/slice06/test.desc b/regression/cbmc-slice/slice06/test.desc
new file mode 100644
index 00000000000..186b56e5f8d
--- /dev/null
+++ b/regression/cbmc-slice/slice06/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^size of program expression: 70 steps$
+^simple slicing removed 0 assignments$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice07/main.c b/regression/cbmc-slice/slice07/main.c
new file mode 100644
index 00000000000..b0acb74a73c
--- /dev/null
+++ b/regression/cbmc-slice/slice07/main.c
@@ -0,0 +1,50 @@
+#include <assert.h>
+#include <pthread.h>
+
+//#define NULL 0
+
+int g;
+
+void *t1(void *arg)
+{
+  int a1, *aptr1;
+  
+  aptr1=(int *)arg;
+  a1=*aptr1;
+  g=0;
+  // this should pass
+  assert(a1==10);
+  assert(g==0);
+
+  return NULL;
+}
+
+void *t2(void *arg)
+{
+  int a2, *aptr2;
+  
+  aptr2=(int *)arg;
+  a2=*aptr2;
+  g=0;
+  // this should pass
+  assert(a2==20);
+
+  return NULL;
+}
+
+int main()
+{
+  pthread_t id1, id2;
+  
+  int arg1=10, arg2=20;
+
+  pthread_create(&id1, NULL, t1, &arg1);
+  pthread_create(&id2, NULL, t2, &arg2);
+
+  assert(g==0);
+
+  pthread_join(id1, NULL);
+  pthread_join(id2, NULL);
+
+  return 0;
+}
diff --git a/regression/cbmc-slice/slice07/test.desc b/regression/cbmc-slice/slice07/test.desc
new file mode 100644
index 00000000000..7d88efc76ad
--- /dev/null
+++ b/regression/cbmc-slice/slice07/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=6$
+^SIGNAL=0$
+^\-\-full\-slice does not support C/Pthreads yet$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice08/main.c b/regression/cbmc-slice/slice08/main.c
new file mode 100644
index 00000000000..c16cd2784ab
--- /dev/null
+++ b/regression/cbmc-slice/slice08/main.c
@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <pthread.h>
+
+int main (void) 
+{
+  int x;
+  int i;
+
+  if (x > 0) {
+    for (i = 0; i < x; ++i) {
+        // Do nothing;
+    }
+  } else {
+    x = 1;
+  }
+
+  assert(x >= 1);
+
+  return 0;
+}
+
diff --git a/regression/cbmc-slice/slice08/test.desc b/regression/cbmc-slice/slice08/test.desc
new file mode 100644
index 00000000000..67625747cf1
--- /dev/null
+++ b/regression/cbmc-slice/slice08/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice --unwind 1
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice09/main.c b/regression/cbmc-slice/slice09/main.c
new file mode 100644
index 00000000000..6cc9ba5bc92
--- /dev/null
+++ b/regression/cbmc-slice/slice09/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+int n=2;
+void main()
+{
+  int i=1;
+  while (i <= n) 
+    i++;
+  assert(i>=0);
+}
diff --git a/regression/cbmc-slice/slice09/test.desc b/regression/cbmc-slice/slice09/test.desc
new file mode 100644
index 00000000000..ad7f834babf
--- /dev/null
+++ b/regression/cbmc-slice/slice09/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^size of program expression: 39 steps$
+^simple slicing removed 0 assignments$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice10/main.c b/regression/cbmc-slice/slice10/main.c
new file mode 100644
index 00000000000..dd59d87af39
--- /dev/null
+++ b/regression/cbmc-slice/slice10/main.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+int n=2, i, s, a = 0;
+void main()
+{
+  i = 1;
+  s = 1;
+  if (a > 0)
+    s = 0;
+  while (i <= n) 
+  {
+    if (a > 0)
+      s += 2;
+    else
+      s *= 2;
+    i++;
+  }
+  assert(s>0);
+}
diff --git a/regression/cbmc-slice/slice10/test.desc b/regression/cbmc-slice/slice10/test.desc
new file mode 100644
index 00000000000..5115cc835cc
--- /dev/null
+++ b/regression/cbmc-slice/slice10/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^size of program expression: 56 steps$
+^simple slicing removed 0 assignments$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice11/main.c b/regression/cbmc-slice/slice11/main.c
new file mode 100644
index 00000000000..b87123d1abe
--- /dev/null
+++ b/regression/cbmc-slice/slice11/main.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+int n=2, i, s, a = 0;
+void main()
+{
+  i = 1;
+  s = 1;
+  if (a > 0)
+    s = 0;
+  while (i <= n) 
+  {
+    if (a > 0)
+      s += 2;
+    else
+      s *= 2;
+    i++;
+  }
+  assert(i>0);
+}
diff --git a/regression/cbmc-slice/slice11/test.desc b/regression/cbmc-slice/slice11/test.desc
new file mode 100644
index 00000000000..6b16bf4501c
--- /dev/null
+++ b/regression/cbmc-slice/slice11/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^size of program expression: 40 steps$
+^simple slicing removed 0 assignments$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From f826a4ef771e429a9f54b38383a7ec088841ab87 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Fri, 11 Nov 2016 13:50:41 +0000
Subject: [PATCH 05/23] add test case slice12

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 regression/cbmc-slice/slice12/main.c    | 12 ++++++++++++
 regression/cbmc-slice/slice12/test.desc | 10 ++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 regression/cbmc-slice/slice12/main.c
 create mode 100644 regression/cbmc-slice/slice12/test.desc

diff --git a/regression/cbmc-slice/slice12/main.c b/regression/cbmc-slice/slice12/main.c
new file mode 100644
index 00000000000..7b395dc27d3
--- /dev/null
+++ b/regression/cbmc-slice/slice12/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+int n=2, i, s, a = 0;
+void main()
+{
+  i = 1;
+  s = 1;
+  if (a > 0)
+    s = 0;
+  if (n==1)
+    s=1;
+  assert(n>0);
+}
diff --git a/regression/cbmc-slice/slice12/test.desc b/regression/cbmc-slice/slice12/test.desc
new file mode 100644
index 00000000000..2d394d0bf18
--- /dev/null
+++ b/regression/cbmc-slice/slice12/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^size of program expression: 36 steps$
+^simple slicing removed 0 assignments$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From e126a1e0918431968054c07f6585a05f5ebb575a Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Fri, 11 Nov 2016 14:20:47 +0000
Subject: [PATCH 06/23] check whether symbol is a __CPROVER_rounding_mode

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/goto-instrument/full_slicer.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 85f407df097..4d860f7f56d 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -346,7 +346,7 @@ static bool implicit(const namespacet &ns, goto_programt::const_targett target)
       return true;
   }
 
-  return false;
+  return s.get_identifier()==CPROVER_PREFIX "rounding_mode";
 }
 
 /*******************************************************************\

From b53ac9127b561cbf5f9cb7310545002b12ffabb6 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Fri, 11 Nov 2016 14:21:49 +0000
Subject: [PATCH 07/23] add test case slice13

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 regression/cbmc-slice/slice13/main.c    |  23 ++++
 regression/cbmc-slice/slice13/test.desc |  10 ++
 regression/cbmc-slice/slice13/tmp1      | 135 ++++++++++++++++++++++++
 regression/cbmc-slice/slice13/tmp2      | 130 +++++++++++++++++++++++
 4 files changed, 298 insertions(+)
 create mode 100644 regression/cbmc-slice/slice13/main.c
 create mode 100644 regression/cbmc-slice/slice13/test.desc
 create mode 100644 regression/cbmc-slice/slice13/tmp1
 create mode 100644 regression/cbmc-slice/slice13/tmp2

diff --git a/regression/cbmc-slice/slice13/main.c b/regression/cbmc-slice/slice13/main.c
new file mode 100644
index 00000000000..3354961512a
--- /dev/null
+++ b/regression/cbmc-slice/slice13/main.c
@@ -0,0 +1,23 @@
+#ifdef __GNUC__
+#include <assert.h>
+#include <math.h>
+#include <fenv.h>
+
+float setRoundingModeAndCast(int mode, double d) {
+  fesetround(mode);
+  return (float)d;
+}
+
+void test (int mode, double d, float result) {
+  float f = setRoundingModeAndCast(mode,d);
+  assert(f == result);
+  return;
+}
+#endif
+
+int main (void)
+{
+  // Nearer to 0x1.fffffep+127 than to 0x1.000000p+128
+  test(FE_UPWARD, 0x1.fffffe0000001p+127, +INFINITY);
+  return 1;
+}
diff --git a/regression/cbmc-slice/slice13/test.desc b/regression/cbmc-slice/slice13/test.desc
new file mode 100644
index 00000000000..63fdcce05c8
--- /dev/null
+++ b/regression/cbmc-slice/slice13/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--floatbv --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^size of program expression: 55 steps$
+^simple slicing removed 0 assignments$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-slice/slice13/tmp1 b/regression/cbmc-slice/slice13/tmp1
new file mode 100644
index 00000000000..77b4ff26cdf
--- /dev/null
+++ b/regression/cbmc-slice/slice13/tmp1
@@ -0,0 +1,135 @@
+CBMC version 5.5 64-bit x86_64 linux
+Parsing main.c
+Converting
+Type-checking main
+Generating GOTO Program
+Adding CPROVER library (x86_64)
+Removal of function pointers and virtual functions
+Partial Inlining
+Generic Property Instrumentation
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+main /* main */
+        // 0 file main.c line 21 function main
+        float return_value___builtin_inff$1;
+        // 1 file main.c line 21 function main
+        LOCATION
+        // 2 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
+        return_value___builtin_inff$1 = 1.000000f / 0.000000f;
+        // 3 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
+        LOCATION
+        // 4 file main.c line 21 function main
+        test(0x800, 3.402823e+38, +return_value___builtin_inff$1);
+        // 5 file main.c line 22 function main
+        main#return_value = 1;
+        // 6 file main.c line 22 function main
+        dead return_value___builtin_inff$1;
+        // 7 file main.c line 23 function main
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+_start /* _start */
+        // 8 no location
+        __CPROVER_initialize();
+        // 9 file main.c line 18
+        main();
+        // 10 file main.c line 18
+        return' = main#return_value;
+        // 11 file main.c line 18
+        dead main#return_value;
+        // 12 file main.c line 18
+        OUTPUT("return", return');
+        // 13 no location
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+__CPROVER_initialize /* __CPROVER_initialize */
+        // 14 no location
+        // Labels: __CPROVER_HIDE
+        SKIP
+        // 15 file <built-in-additions> line 39
+        __CPROVER_dead_object = NULL;
+        // 16 file <built-in-additions> line 38
+        __CPROVER_deallocated = NULL;
+        // 17 file <built-in-additions> line 42
+        __CPROVER_malloc_is_new_array = 0 != 0;
+        // 18 file <built-in-additions> line 40
+        __CPROVER_malloc_object = NULL;
+        // 19 file <built-in-additions> line 41
+        __CPROVER_malloc_size = 0ul;
+        // 20 file <built-in-additions> line 43
+        __CPROVER_memory_leak = NULL;
+        // 21 file <built-in-additions> line 31
+        __CPROVER_next_thread_id = (unsigned long int)0;
+        // 22 file <built-in-additions> line 85
+        __CPROVER_pipe_count = (unsigned int)0;
+        // 23 file <built-in-additions> line 65
+        __CPROVER_rounding_mode = 0;
+        // 24 file <built-in-additions> line 29
+        __CPROVER_thread_id = (unsigned long int)0;
+        // 25 file <built-in-additions> line 30
+        __CPROVER_threads_exited = ARRAY_OF(FALSE);
+        // 26 no location
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+__builtin_inff /* __builtin_inff */
+        // 27 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
+        __builtin_inff#return_value = 1.000000f / 0.000000f;
+        // 28 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+fesetround /* fesetround */
+        // 29 file <builtin-library-fesetround> line 6 function fesetround
+        // Labels: __CPROVER_HIDE
+        SKIP
+        // 30 file <builtin-library-fesetround> line 8 function fesetround
+        __CPROVER_rounding_mode = rounding_mode == 0x400 ? 1 : (rounding_mode == 0 ? 0 : (rounding_mode == 0xC00 ? 3 : (rounding_mode == 0x800 ? 2 : 0)));
+        // 31 file <builtin-library-fesetround> line 18 function fesetround
+        fesetround#return_value = 0;
+        // 32 file <builtin-library-fesetround> line 19 function fesetround
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+setRoundingModeAndCast /* setRoundingModeAndCast */
+        // 33 file main.c line 7 function setRoundingModeAndCast
+        LOCATION
+        // 34 file main.c line 7 function setRoundingModeAndCast
+        signed int rounding_mode;
+        // 35 file main.c line 7 function setRoundingModeAndCast
+        rounding_mode = mode;
+        // 36 file main.c line 7 function setRoundingModeAndCast
+        // Labels: __CPROVER_HIDE
+        SKIP
+        // 37 file main.c line 7 function setRoundingModeAndCast
+        __CPROVER_rounding_mode = rounding_mode == 0x400 ? 1 : (rounding_mode == 0 ? 0 : (rounding_mode == 0xC00 ? 3 : (rounding_mode == 0x800 ? 2 : 0)));
+        // 38 file main.c line 7 function setRoundingModeAndCast
+        0;
+        // 39 file main.c line 7 function setRoundingModeAndCast
+        LOCATION
+        // 40 file main.c line 7 function setRoundingModeAndCast
+        dead rounding_mode;
+        // 41 file main.c line 8 function setRoundingModeAndCast
+        setRoundingModeAndCast#return_value = (float)d;
+        // 42 file main.c line 9 function setRoundingModeAndCast
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+test /* test */
+        // 43 file main.c line 12 function test
+        float f;
+        // 44 file main.c line 12 function test
+        setRoundingModeAndCast(mode, d);
+        // 45 file main.c line 12 function test
+        f = setRoundingModeAndCast#return_value;
+        // 46 file main.c line 12 function test
+        dead setRoundingModeAndCast#return_value;
+        // 47 file main.c line 13 function test
+        ASSERT IEEE_FLOAT_EQUAL(f, result) // assertion f == result
+        // 48 file main.c line 13 function test
+        IF !IEEE_FLOAT_EQUAL(f, result) THEN GOTO 1
+        // 49 file main.c line 14 function test
+     1: dead f;
+        // 50 file main.c line 15 function test
+        END_FUNCTION
diff --git a/regression/cbmc-slice/slice13/tmp2 b/regression/cbmc-slice/slice13/tmp2
new file mode 100644
index 00000000000..d1aa9aca781
--- /dev/null
+++ b/regression/cbmc-slice/slice13/tmp2
@@ -0,0 +1,130 @@
+CBMC version 5.5 64-bit x86_64 linux
+Parsing main.c
+Converting
+Type-checking main
+Generating GOTO Program
+Adding CPROVER library (x86_64)
+Removal of function pointers and virtual functions
+Performing a full slice
+Partial Inlining
+Generic Property Instrumentation
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+main /* main */
+        // 0 file main.c line 21 function main
+        float return_value___builtin_inff$1;
+        // 1 file main.c line 21 function main
+        LOCATION
+        // 2 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
+        __builtin_inff#return_value = 1.000000f / 0.000000f;
+        // 3 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
+        LOCATION
+        // 4 file main.c line 21 function main
+        return_value___builtin_inff$1 = __builtin_inff#return_value;
+        // 5 file main.c line 21 function main
+        dead __builtin_inff#return_value;
+        // 6 file main.c line 21 function main
+        test(0x800, 3.402823e+38, +return_value___builtin_inff$1);
+        // 7 file main.c line 22 function main
+        main#return_value = 1;
+        // 8 file main.c line 22 function main
+        dead return_value___builtin_inff$1;
+        // 9 file main.c line 23 function main
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+_start /* _start */
+        // 10 no location
+        __CPROVER_initialize();
+        // 11 file main.c line 18
+        main();
+        // 12 file main.c line 18
+        dead main#return_value;
+        // 13 no location
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+__CPROVER_initialize /* __CPROVER_initialize */
+        // 14 no location
+        // Labels: __CPROVER_HIDE
+        SKIP
+        // 15 file <built-in-additions> line 39
+        __CPROVER_dead_object = NULL;
+        // 16 file <built-in-additions> line 38
+        __CPROVER_deallocated = NULL;
+        // 17 file <built-in-additions> line 42
+        __CPROVER_malloc_is_new_array = 0 != 0;
+        // 18 file <built-in-additions> line 40
+        __CPROVER_malloc_object = NULL;
+        // 19 file <built-in-additions> line 41
+        __CPROVER_malloc_size = 0ul;
+        // 20 file <built-in-additions> line 43
+        __CPROVER_memory_leak = NULL;
+        // 21 file <built-in-additions> line 31
+        __CPROVER_next_thread_id = (unsigned long int)0;
+        // 22 file <built-in-additions> line 85
+        __CPROVER_pipe_count = (unsigned int)0;
+        // 23 file <built-in-additions> line 65
+        __CPROVER_rounding_mode = 0;
+        // 24 file <built-in-additions> line 29
+        __CPROVER_thread_id = (unsigned long int)0;
+        // 25 file <built-in-additions> line 30
+        __CPROVER_threads_exited = ARRAY_OF(FALSE);
+        // 26 no location
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+__builtin_inff /* __builtin_inff */
+        // 27 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
+        __builtin_inff#return_value = 1.000000f / 0.000000f;
+        // 28 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+fesetround /* fesetround */
+        // 29 file <builtin-library-fesetround> line 6 function fesetround
+        // Labels: __CPROVER_HIDE
+        SKIP
+        // 30 file <builtin-library-fesetround> line 18 function fesetround
+        fesetround#return_value = 0;
+        // 31 file <builtin-library-fesetround> line 19 function fesetround
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+setRoundingModeAndCast /* setRoundingModeAndCast */
+        // 32 file main.c line 7 function setRoundingModeAndCast
+        LOCATION
+        // 33 file main.c line 7 function setRoundingModeAndCast
+        signed int rounding_mode;
+        // 34 file main.c line 7 function setRoundingModeAndCast
+        rounding_mode = mode;
+        // 35 file main.c line 7 function setRoundingModeAndCast
+        // Labels: __CPROVER_HIDE
+        SKIP
+        // 36 file main.c line 7 function setRoundingModeAndCast
+        fesetround#return_value = 0;
+        // 37 file main.c line 7 function setRoundingModeAndCast
+        LOCATION
+        // 38 file main.c line 7 function setRoundingModeAndCast
+        dead rounding_mode;
+        // 39 file main.c line 8 function setRoundingModeAndCast
+        setRoundingModeAndCast#return_value = (float)d;
+        // 40 file main.c line 9 function setRoundingModeAndCast
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+test /* test */
+        // 41 file main.c line 12 function test
+        float f;
+        // 42 file main.c line 12 function test
+        setRoundingModeAndCast(mode, d);
+        // 43 file main.c line 12 function test
+        f = setRoundingModeAndCast#return_value;
+        // 44 file main.c line 12 function test
+        dead setRoundingModeAndCast#return_value;
+        // 45 file main.c line 13 function test
+        ASSERT IEEE_FLOAT_EQUAL(f, result) // assertion f == result
+        // 46 file main.c line 14 function test
+        dead f;
+        // 47 file main.c line 15 function test
+        END_FUNCTION

From bdc6b83f8d0382637fe4664b23bec0522fb34079 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Fri, 11 Nov 2016 14:22:21 +0000
Subject: [PATCH 08/23] remove unused files from slice13

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 regression/cbmc-slice/slice13/tmp1 | 135 -----------------------------
 regression/cbmc-slice/slice13/tmp2 | 130 ---------------------------
 2 files changed, 265 deletions(-)
 delete mode 100644 regression/cbmc-slice/slice13/tmp1
 delete mode 100644 regression/cbmc-slice/slice13/tmp2

diff --git a/regression/cbmc-slice/slice13/tmp1 b/regression/cbmc-slice/slice13/tmp1
deleted file mode 100644
index 77b4ff26cdf..00000000000
--- a/regression/cbmc-slice/slice13/tmp1
+++ /dev/null
@@ -1,135 +0,0 @@
-CBMC version 5.5 64-bit x86_64 linux
-Parsing main.c
-Converting
-Type-checking main
-Generating GOTO Program
-Adding CPROVER library (x86_64)
-Removal of function pointers and virtual functions
-Partial Inlining
-Generic Property Instrumentation
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-main /* main */
-        // 0 file main.c line 21 function main
-        float return_value___builtin_inff$1;
-        // 1 file main.c line 21 function main
-        LOCATION
-        // 2 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
-        return_value___builtin_inff$1 = 1.000000f / 0.000000f;
-        // 3 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
-        LOCATION
-        // 4 file main.c line 21 function main
-        test(0x800, 3.402823e+38, +return_value___builtin_inff$1);
-        // 5 file main.c line 22 function main
-        main#return_value = 1;
-        // 6 file main.c line 22 function main
-        dead return_value___builtin_inff$1;
-        // 7 file main.c line 23 function main
-        END_FUNCTION
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-_start /* _start */
-        // 8 no location
-        __CPROVER_initialize();
-        // 9 file main.c line 18
-        main();
-        // 10 file main.c line 18
-        return' = main#return_value;
-        // 11 file main.c line 18
-        dead main#return_value;
-        // 12 file main.c line 18
-        OUTPUT("return", return');
-        // 13 no location
-        END_FUNCTION
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-__CPROVER_initialize /* __CPROVER_initialize */
-        // 14 no location
-        // Labels: __CPROVER_HIDE
-        SKIP
-        // 15 file <built-in-additions> line 39
-        __CPROVER_dead_object = NULL;
-        // 16 file <built-in-additions> line 38
-        __CPROVER_deallocated = NULL;
-        // 17 file <built-in-additions> line 42
-        __CPROVER_malloc_is_new_array = 0 != 0;
-        // 18 file <built-in-additions> line 40
-        __CPROVER_malloc_object = NULL;
-        // 19 file <built-in-additions> line 41
-        __CPROVER_malloc_size = 0ul;
-        // 20 file <built-in-additions> line 43
-        __CPROVER_memory_leak = NULL;
-        // 21 file <built-in-additions> line 31
-        __CPROVER_next_thread_id = (unsigned long int)0;
-        // 22 file <built-in-additions> line 85
-        __CPROVER_pipe_count = (unsigned int)0;
-        // 23 file <built-in-additions> line 65
-        __CPROVER_rounding_mode = 0;
-        // 24 file <built-in-additions> line 29
-        __CPROVER_thread_id = (unsigned long int)0;
-        // 25 file <built-in-additions> line 30
-        __CPROVER_threads_exited = ARRAY_OF(FALSE);
-        // 26 no location
-        END_FUNCTION
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-__builtin_inff /* __builtin_inff */
-        // 27 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
-        __builtin_inff#return_value = 1.000000f / 0.000000f;
-        // 28 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
-        END_FUNCTION
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-fesetround /* fesetround */
-        // 29 file <builtin-library-fesetround> line 6 function fesetround
-        // Labels: __CPROVER_HIDE
-        SKIP
-        // 30 file <builtin-library-fesetround> line 8 function fesetround
-        __CPROVER_rounding_mode = rounding_mode == 0x400 ? 1 : (rounding_mode == 0 ? 0 : (rounding_mode == 0xC00 ? 3 : (rounding_mode == 0x800 ? 2 : 0)));
-        // 31 file <builtin-library-fesetround> line 18 function fesetround
-        fesetround#return_value = 0;
-        // 32 file <builtin-library-fesetround> line 19 function fesetround
-        END_FUNCTION
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-setRoundingModeAndCast /* setRoundingModeAndCast */
-        // 33 file main.c line 7 function setRoundingModeAndCast
-        LOCATION
-        // 34 file main.c line 7 function setRoundingModeAndCast
-        signed int rounding_mode;
-        // 35 file main.c line 7 function setRoundingModeAndCast
-        rounding_mode = mode;
-        // 36 file main.c line 7 function setRoundingModeAndCast
-        // Labels: __CPROVER_HIDE
-        SKIP
-        // 37 file main.c line 7 function setRoundingModeAndCast
-        __CPROVER_rounding_mode = rounding_mode == 0x400 ? 1 : (rounding_mode == 0 ? 0 : (rounding_mode == 0xC00 ? 3 : (rounding_mode == 0x800 ? 2 : 0)));
-        // 38 file main.c line 7 function setRoundingModeAndCast
-        0;
-        // 39 file main.c line 7 function setRoundingModeAndCast
-        LOCATION
-        // 40 file main.c line 7 function setRoundingModeAndCast
-        dead rounding_mode;
-        // 41 file main.c line 8 function setRoundingModeAndCast
-        setRoundingModeAndCast#return_value = (float)d;
-        // 42 file main.c line 9 function setRoundingModeAndCast
-        END_FUNCTION
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-test /* test */
-        // 43 file main.c line 12 function test
-        float f;
-        // 44 file main.c line 12 function test
-        setRoundingModeAndCast(mode, d);
-        // 45 file main.c line 12 function test
-        f = setRoundingModeAndCast#return_value;
-        // 46 file main.c line 12 function test
-        dead setRoundingModeAndCast#return_value;
-        // 47 file main.c line 13 function test
-        ASSERT IEEE_FLOAT_EQUAL(f, result) // assertion f == result
-        // 48 file main.c line 13 function test
-        IF !IEEE_FLOAT_EQUAL(f, result) THEN GOTO 1
-        // 49 file main.c line 14 function test
-     1: dead f;
-        // 50 file main.c line 15 function test
-        END_FUNCTION
diff --git a/regression/cbmc-slice/slice13/tmp2 b/regression/cbmc-slice/slice13/tmp2
deleted file mode 100644
index d1aa9aca781..00000000000
--- a/regression/cbmc-slice/slice13/tmp2
+++ /dev/null
@@ -1,130 +0,0 @@
-CBMC version 5.5 64-bit x86_64 linux
-Parsing main.c
-Converting
-Type-checking main
-Generating GOTO Program
-Adding CPROVER library (x86_64)
-Removal of function pointers and virtual functions
-Performing a full slice
-Partial Inlining
-Generic Property Instrumentation
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-main /* main */
-        // 0 file main.c line 21 function main
-        float return_value___builtin_inff$1;
-        // 1 file main.c line 21 function main
-        LOCATION
-        // 2 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
-        __builtin_inff#return_value = 1.000000f / 0.000000f;
-        // 3 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
-        LOCATION
-        // 4 file main.c line 21 function main
-        return_value___builtin_inff$1 = __builtin_inff#return_value;
-        // 5 file main.c line 21 function main
-        dead __builtin_inff#return_value;
-        // 6 file main.c line 21 function main
-        test(0x800, 3.402823e+38, +return_value___builtin_inff$1);
-        // 7 file main.c line 22 function main
-        main#return_value = 1;
-        // 8 file main.c line 22 function main
-        dead return_value___builtin_inff$1;
-        // 9 file main.c line 23 function main
-        END_FUNCTION
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-_start /* _start */
-        // 10 no location
-        __CPROVER_initialize();
-        // 11 file main.c line 18
-        main();
-        // 12 file main.c line 18
-        dead main#return_value;
-        // 13 no location
-        END_FUNCTION
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-__CPROVER_initialize /* __CPROVER_initialize */
-        // 14 no location
-        // Labels: __CPROVER_HIDE
-        SKIP
-        // 15 file <built-in-additions> line 39
-        __CPROVER_dead_object = NULL;
-        // 16 file <built-in-additions> line 38
-        __CPROVER_deallocated = NULL;
-        // 17 file <built-in-additions> line 42
-        __CPROVER_malloc_is_new_array = 0 != 0;
-        // 18 file <built-in-additions> line 40
-        __CPROVER_malloc_object = NULL;
-        // 19 file <built-in-additions> line 41
-        __CPROVER_malloc_size = 0ul;
-        // 20 file <built-in-additions> line 43
-        __CPROVER_memory_leak = NULL;
-        // 21 file <built-in-additions> line 31
-        __CPROVER_next_thread_id = (unsigned long int)0;
-        // 22 file <built-in-additions> line 85
-        __CPROVER_pipe_count = (unsigned int)0;
-        // 23 file <built-in-additions> line 65
-        __CPROVER_rounding_mode = 0;
-        // 24 file <built-in-additions> line 29
-        __CPROVER_thread_id = (unsigned long int)0;
-        // 25 file <built-in-additions> line 30
-        __CPROVER_threads_exited = ARRAY_OF(FALSE);
-        // 26 no location
-        END_FUNCTION
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-__builtin_inff /* __builtin_inff */
-        // 27 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
-        __builtin_inff#return_value = 1.000000f / 0.000000f;
-        // 28 file <builtin-library-__builtin_inff> line 2 function __builtin_inff
-        END_FUNCTION
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-fesetround /* fesetround */
-        // 29 file <builtin-library-fesetround> line 6 function fesetround
-        // Labels: __CPROVER_HIDE
-        SKIP
-        // 30 file <builtin-library-fesetround> line 18 function fesetround
-        fesetround#return_value = 0;
-        // 31 file <builtin-library-fesetround> line 19 function fesetround
-        END_FUNCTION
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-setRoundingModeAndCast /* setRoundingModeAndCast */
-        // 32 file main.c line 7 function setRoundingModeAndCast
-        LOCATION
-        // 33 file main.c line 7 function setRoundingModeAndCast
-        signed int rounding_mode;
-        // 34 file main.c line 7 function setRoundingModeAndCast
-        rounding_mode = mode;
-        // 35 file main.c line 7 function setRoundingModeAndCast
-        // Labels: __CPROVER_HIDE
-        SKIP
-        // 36 file main.c line 7 function setRoundingModeAndCast
-        fesetround#return_value = 0;
-        // 37 file main.c line 7 function setRoundingModeAndCast
-        LOCATION
-        // 38 file main.c line 7 function setRoundingModeAndCast
-        dead rounding_mode;
-        // 39 file main.c line 8 function setRoundingModeAndCast
-        setRoundingModeAndCast#return_value = (float)d;
-        // 40 file main.c line 9 function setRoundingModeAndCast
-        END_FUNCTION
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-test /* test */
-        // 41 file main.c line 12 function test
-        float f;
-        // 42 file main.c line 12 function test
-        setRoundingModeAndCast(mode, d);
-        // 43 file main.c line 12 function test
-        f = setRoundingModeAndCast#return_value;
-        // 44 file main.c line 12 function test
-        dead setRoundingModeAndCast#return_value;
-        // 45 file main.c line 13 function test
-        ASSERT IEEE_FLOAT_EQUAL(f, result) // assertion f == result
-        // 46 file main.c line 14 function test
-        dead f;
-        // 47 file main.c line 15 function test
-        END_FUNCTION

From 226b3f90dd85b669aed7e133c1d7eeda056d8908 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Fri, 11 Nov 2016 14:22:53 +0000
Subject: [PATCH 09/23] add makefile to cbmc-slice

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 regression/cbmc-slice/Makefile | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 regression/cbmc-slice/Makefile

diff --git a/regression/cbmc-slice/Makefile b/regression/cbmc-slice/Makefile
new file mode 100644
index 00000000000..cbdd3378bac
--- /dev/null
+++ b/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;

From efb1fc41dbf846abca57105691483bedeef4534c Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Fri, 11 Nov 2016 15:43:00 +0000
Subject: [PATCH 10/23] do not remove assignments related to dereference

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/goto-instrument/full_slicer.cpp | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 4d860f7f56d..5c723839c8d 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -6,6 +6,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
+#include <iostream>
+
 #include <util/find_symbols.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
@@ -331,6 +333,7 @@ static bool implicit(const namespacet &ns, goto_programt::const_targett target)
   if(!target->is_assign()) return false;
 
   const code_assignt &a=to_code_assign(target->code);
+  if(a.lhs().id()==ID_dereference) return true;
   if(a.lhs().id()!=ID_symbol) return false;
 
   const symbol_exprt &s=to_symbol_expr(a.lhs());
@@ -346,7 +349,11 @@ static bool implicit(const namespacet &ns, goto_programt::const_targett target)
       return true;
   }
 
-  return s.get_identifier()==CPROVER_PREFIX "rounding_mode";
+  if (s.get_identifier()==CPROVER_PREFIX "rounding_mode" ||
+      s.get_identifier()==CPROVER_PREFIX "deallocated")
+    return true;
+
+  return false;
 }
 
 /*******************************************************************\

From 42af01ec932e83a9b1933aaaa0b1c516d9d9df65 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Fri, 11 Nov 2016 15:44:13 +0000
Subject: [PATCH 11/23] add test case slice14

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 regression/cbmc-slice/slice01/test.desc |  4 ++--
 regression/cbmc-slice/slice14/main.c    | 15 +++++++++++++++
 regression/cbmc-slice/slice14/test.desc |  8 ++++++++
 3 files changed, 25 insertions(+), 2 deletions(-)
 create mode 100644 regression/cbmc-slice/slice14/main.c
 create mode 100644 regression/cbmc-slice/slice14/test.desc

diff --git a/regression/cbmc-slice/slice01/test.desc b/regression/cbmc-slice/slice01/test.desc
index 70c57b14a59..db6294f3d5f 100644
--- a/regression/cbmc-slice/slice01/test.desc
+++ b/regression/cbmc-slice/slice01/test.desc
@@ -3,8 +3,8 @@ main.c
 --unwind 2 --full-slice
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 208 steps$
-^simple slicing removed 6 assignments$
+^size of program expression: 215 steps$
+^simple slicing removed 13 assignments$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-slice/slice14/main.c b/regression/cbmc-slice/slice14/main.c
new file mode 100644
index 00000000000..ef23ab68a1a
--- /dev/null
+++ b/regression/cbmc-slice/slice14/main.c
@@ -0,0 +1,15 @@
+void *malloc(__CPROVER_size_t);
+void free(void *);
+
+int main()
+{
+  int *p=malloc(sizeof(int));
+  int *q=p;
+  int i, x;
+  i=x;
+  
+  if(i==4711) free(q);
+
+  // should fail if i==4711
+  *p=1;
+}
diff --git a/regression/cbmc-slice/slice14/test.desc b/regression/cbmc-slice/slice14/test.desc
new file mode 100644
index 00000000000..a2b36885fc7
--- /dev/null
+++ b/regression/cbmc-slice/slice14/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --full-slice
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

From 0f2ea7b37e3469d577692cadad466f3a9c5bf422 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Fri, 18 Nov 2016 16:05:01 +0000
Subject: [PATCH 12/23] add test case slice15

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 regression/cbmc-slice/slice15/main.c    | 24 ++++++++++++++++++++++++
 regression/cbmc-slice/slice15/test.desc |  8 ++++++++
 2 files changed, 32 insertions(+)
 create mode 100644 regression/cbmc-slice/slice15/main.c
 create mode 100644 regression/cbmc-slice/slice15/test.desc

diff --git a/regression/cbmc-slice/slice15/main.c b/regression/cbmc-slice/slice15/main.c
new file mode 100644
index 00000000000..0572b279999
--- /dev/null
+++ b/regression/cbmc-slice/slice15/main.c
@@ -0,0 +1,24 @@
+int nondet_int();
+
+double d = 0.0;
+
+void f1()
+{
+  d = 1.0;
+}
+
+int main()
+{
+  int x = 2;
+
+  if(nondet_int())
+    x = 4;
+
+  (void) f1();
+
+  d += (x == 2);
+
+  d += (x > 3);
+
+  assert(d == 2.0);
+}
diff --git a/regression/cbmc-slice/slice15/test.desc b/regression/cbmc-slice/slice15/test.desc
new file mode 100644
index 00000000000..8e6dafcc8e6
--- /dev/null
+++ b/regression/cbmc-slice/slice15/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--fixedbv --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From a77eb88d1f4de27225ccff6f312dd5bb6c6f492f Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Mon, 21 Nov 2016 15:24:13 +0000
Subject: [PATCH 13/23] add test case slice16 from the paper 'On Slicing
 Programs with Jump Statements'

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 regression/cbmc-slice/slice16/main.c    | 48 +++++++++++++++++++++++++
 regression/cbmc-slice/slice16/test.desc |  9 +++++
 2 files changed, 57 insertions(+)
 create mode 100644 regression/cbmc-slice/slice16/main.c
 create mode 100644 regression/cbmc-slice/slice16/test.desc

diff --git a/regression/cbmc-slice/slice16/main.c b/regression/cbmc-slice/slice16/main.c
new file mode 100644
index 00000000000..99d0cda2c16
--- /dev/null
+++ b/regression/cbmc-slice/slice16/main.c
@@ -0,0 +1,48 @@
+/* running example extracted from 
+"In Slicing Programs with Jump Statements" 
+by Hiralal Afrawal */
+#include <assert.h>
+int x;
+_Bool nondet_bool();
+unsigned int nondet_uint();
+
+_Bool leof() {
+  return nondet_bool();
+}
+
+int f1(int x) {
+  return x*1;
+}
+
+int f2(int x) {
+  return x*2;
+}
+
+int f3(int x) {
+  return x*3;
+}
+
+void read(int *x) {
+  x = nondet_uint();
+}
+
+int main() {
+  int sum=0;
+  int positives=0;
+  while(leof())
+  {
+    read(x);
+    if (x <= 0)  
+      sum = sum + f1(x);
+    else
+    {
+      positives = positives + 1;
+      if (x%2 == 0)
+        sum = sum + f2(x);
+      else
+        sum = sum + f3(x);
+    }
+  }
+  assert(sum>=0);
+  assert(positives>=0);
+}
diff --git a/regression/cbmc-slice/slice16/test.desc b/regression/cbmc-slice/slice16/test.desc
new file mode 100644
index 00000000000..6064ea8e758
--- /dev/null
+++ b/regression/cbmc-slice/slice16/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--full-slice --unwind 2
+^EXIT=0$
+^SIGNAL=0$
+^size of program expression: 86 steps$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From a9c1ea7ff3999e1d705d0b52adaf27523c171cf7 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Tue, 22 Nov 2016 13:01:09 +0000
Subject: [PATCH 14/23] add function calls to the queue before computing the
 dependency graph

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/goto-instrument/full_slicer.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 5c723839c8d..a78847390d8 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -405,6 +405,8 @@ void full_slicert::operator()(
       const exprt &s=to_code_dead(e_it->first->code).symbol();
       decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
     }
+    else if(e_it->first->is_function_call())
+      add_to_queue(queue, e_it->second, e_it->first);
   }
 
   // compute program dependence graph (and post-dominators)

From 83d5b2ed84e4fde2820aab658e769af79136df19 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Tue, 13 Dec 2016 13:39:45 +0000
Subject: [PATCH 15/23] update test desc for full-slice

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 regression/cbmc-slice/slice01/test.desc | 2 --
 regression/cbmc-slice/slice02/test.desc | 2 --
 regression/cbmc-slice/slice03/test.desc | 2 --
 regression/cbmc-slice/slice04/test.desc | 2 --
 regression/cbmc-slice/slice05/test.desc | 2 --
 regression/cbmc-slice/slice06/test.desc | 2 --
 regression/cbmc-slice/slice09/test.desc | 2 --
 regression/cbmc-slice/slice10/test.desc | 2 --
 regression/cbmc-slice/slice11/test.desc | 2 --
 regression/cbmc-slice/slice12/test.desc | 2 --
 regression/cbmc-slice/slice13/test.desc | 2 --
 regression/cbmc-slice/slice16/test.desc | 1 -
 12 files changed, 23 deletions(-)

diff --git a/regression/cbmc-slice/slice01/test.desc b/regression/cbmc-slice/slice01/test.desc
index db6294f3d5f..6f19f2d9ef6 100644
--- a/regression/cbmc-slice/slice01/test.desc
+++ b/regression/cbmc-slice/slice01/test.desc
@@ -3,8 +3,6 @@ main.c
 --unwind 2 --full-slice
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 215 steps$
-^simple slicing removed 13 assignments$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-slice/slice02/test.desc b/regression/cbmc-slice/slice02/test.desc
index 36ac80afc72..2d61905c826 100644
--- a/regression/cbmc-slice/slice02/test.desc
+++ b/regression/cbmc-slice/slice02/test.desc
@@ -3,8 +3,6 @@ main.c
 --pointer-check --full-slice
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 678 steps$
-^simple slicing removed 24 assignments$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-slice/slice03/test.desc b/regression/cbmc-slice/slice03/test.desc
index 1c925e4c66e..f9810300c02 100644
--- a/regression/cbmc-slice/slice03/test.desc
+++ b/regression/cbmc-slice/slice03/test.desc
@@ -3,8 +3,6 @@ main.c
 --unwind 10 --pointer-check --bounds-check --full-slice
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 280 steps$
-^simple slicing removed 16 assignments$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-slice/slice04/test.desc b/regression/cbmc-slice/slice04/test.desc
index 3c3a608beef..4d8899e64c7 100644
--- a/regression/cbmc-slice/slice04/test.desc
+++ b/regression/cbmc-slice/slice04/test.desc
@@ -3,8 +3,6 @@ main.c
 --floatbv --full-slice
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 62 steps$
-^simple slicing removed 4 assignments$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-slice/slice05/test.desc b/regression/cbmc-slice/slice05/test.desc
index b553464bdeb..3793f7374e1 100644
--- a/regression/cbmc-slice/slice05/test.desc
+++ b/regression/cbmc-slice/slice05/test.desc
@@ -3,8 +3,6 @@ main.c
 --full-slice
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 38 steps$
-^simple slicing removed 0 assignments$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-slice/slice06/test.desc b/regression/cbmc-slice/slice06/test.desc
index 186b56e5f8d..3793f7374e1 100644
--- a/regression/cbmc-slice/slice06/test.desc
+++ b/regression/cbmc-slice/slice06/test.desc
@@ -3,8 +3,6 @@ main.c
 --full-slice
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 70 steps$
-^simple slicing removed 0 assignments$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-slice/slice09/test.desc b/regression/cbmc-slice/slice09/test.desc
index ad7f834babf..3793f7374e1 100644
--- a/regression/cbmc-slice/slice09/test.desc
+++ b/regression/cbmc-slice/slice09/test.desc
@@ -3,8 +3,6 @@ main.c
 --full-slice
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 39 steps$
-^simple slicing removed 0 assignments$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-slice/slice10/test.desc b/regression/cbmc-slice/slice10/test.desc
index 5115cc835cc..3793f7374e1 100644
--- a/regression/cbmc-slice/slice10/test.desc
+++ b/regression/cbmc-slice/slice10/test.desc
@@ -3,8 +3,6 @@ main.c
 --full-slice
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 56 steps$
-^simple slicing removed 0 assignments$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-slice/slice11/test.desc b/regression/cbmc-slice/slice11/test.desc
index 6b16bf4501c..3793f7374e1 100644
--- a/regression/cbmc-slice/slice11/test.desc
+++ b/regression/cbmc-slice/slice11/test.desc
@@ -3,8 +3,6 @@ main.c
 --full-slice
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 40 steps$
-^simple slicing removed 0 assignments$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-slice/slice12/test.desc b/regression/cbmc-slice/slice12/test.desc
index 2d394d0bf18..3793f7374e1 100644
--- a/regression/cbmc-slice/slice12/test.desc
+++ b/regression/cbmc-slice/slice12/test.desc
@@ -3,8 +3,6 @@ main.c
 --full-slice
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 36 steps$
-^simple slicing removed 0 assignments$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-slice/slice13/test.desc b/regression/cbmc-slice/slice13/test.desc
index 63fdcce05c8..4d8899e64c7 100644
--- a/regression/cbmc-slice/slice13/test.desc
+++ b/regression/cbmc-slice/slice13/test.desc
@@ -3,8 +3,6 @@ main.c
 --floatbv --full-slice
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 55 steps$
-^simple slicing removed 0 assignments$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-slice/slice16/test.desc b/regression/cbmc-slice/slice16/test.desc
index 6064ea8e758..0f63776547f 100644
--- a/regression/cbmc-slice/slice16/test.desc
+++ b/regression/cbmc-slice/slice16/test.desc
@@ -3,7 +3,6 @@ main.c
 --full-slice --unwind 2
 ^EXIT=0$
 ^SIGNAL=0$
-^size of program expression: 86 steps$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

From 5a82815c1766e4339bd0466e32788ccb005c5817 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Tue, 13 Dec 2016 14:06:20 +0000
Subject: [PATCH 16/23] remove function pointers by adding the safety assertion

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/cbmc/cbmc_parse_options.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index db8b60fcb95..ec7036ec6a3 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -860,7 +860,7 @@ bool cbmc_parse_optionst::process_goto_program(
     {
       status() << "Performing a full slice" << eom;
       remove_virtual_functions(symbol_table,goto_functions);
-      remove_function_pointers(symbol_table,goto_functions,false);
+      remove_function_pointers(symbol_table,goto_functions,cmdline.isset("pointer-check"));
       remove_returns(symbol_table,goto_functions);
       goto_functions.update();
       try

From d59dd58d8868f31b2d694a51b3b8d9a8ba6aaace Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Tue, 13 Dec 2016 14:38:45 +0000
Subject: [PATCH 17/23] add test case related to equality through union

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 regression/cbmc-slice/slice17/main.c    | 35 +++++++++++++++++++++++++
 regression/cbmc-slice/slice17/test.desc |  8 ++++++
 2 files changed, 43 insertions(+)
 create mode 100644 regression/cbmc-slice/slice17/main.c
 create mode 100644 regression/cbmc-slice/slice17/test.desc

diff --git a/regression/cbmc-slice/slice17/main.c b/regression/cbmc-slice/slice17/main.c
new file mode 100644
index 00000000000..ccc03df0596
--- /dev/null
+++ b/regression/cbmc-slice/slice17/main.c
@@ -0,0 +1,35 @@
+#include <assert.h>
+#include <stdint.h>
+
+union u
+{
+  uint32_t x;
+   int32_t y;
+   int8_t  z[4];
+};
+
+union u pass_through_union (uint32_t q)
+{
+  union u un;
+
+  un.z[0] = 0x0;
+  un.y = q;
+  un.z[3] = 0x0;
+  un.z[0] = 0x0;
+
+  return un;
+}
+
+int main (void)
+{
+  uint32_t q;
+
+  __CPROVER_assume((q & q - 1) == 0);
+  __CPROVER_assume(256 <= q && q <= (1 << 23));
+
+  union u un = pass_through_union(q);
+
+  assert(q == un.y);
+
+  return 1;
+}
diff --git a/regression/cbmc-slice/slice17/test.desc b/regression/cbmc-slice/slice17/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc-slice/slice17/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From be2709ce590a6edeefcd31a1accfb039460def07 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Tue, 13 Dec 2016 15:30:44 +0000
Subject: [PATCH 18/23] consider assume statements during symbolic execution

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/goto-instrument/full_slicer.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index a78847390d8..54dd954a54e 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -330,6 +330,7 @@ static bool implicit(const namespacet &ns, goto_programt::const_targett target)
 {
   // some variables are used during symbolic execution only
 
+  if (target->is_assume()) return true;
   if(!target->is_assign()) return false;
 
   const code_assignt &a=to_code_assign(target->code);

From fada6185d03028840f415fda8f5ab057218a602c Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Tue, 13 Dec 2016 15:32:46 +0000
Subject: [PATCH 19/23] add test case related to the exit function

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 regression/cbmc-slice/slice18/main.c    | 11 +++++++++++
 regression/cbmc-slice/slice18/test.desc |  8 ++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 regression/cbmc-slice/slice18/main.c
 create mode 100644 regression/cbmc-slice/slice18/test.desc

diff --git a/regression/cbmc-slice/slice18/main.c b/regression/cbmc-slice/slice18/main.c
new file mode 100644
index 00000000000..0661315487b
--- /dev/null
+++ b/regression/cbmc-slice/slice18/main.c
@@ -0,0 +1,11 @@
+void exit(int status);
+
+int main() {
+  int x;
+  
+  if(x==10)
+    exit(1);
+
+  if(x==10)
+    assert(0);
+}
diff --git a/regression/cbmc-slice/slice18/test.desc b/regression/cbmc-slice/slice18/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc-slice/slice18/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From ed9b8019991ebaf5578ab8d5d161191fb2f79100 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Tue, 13 Dec 2016 16:07:10 +0000
Subject: [PATCH 20/23] execute full-slice after goto_check

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/cbmc/cbmc_parse_options.cpp | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index ec7036ec6a3..0cacfec3ba5 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -855,6 +855,19 @@ bool cbmc_parse_optionst::process_goto_program(
       cmdline.isset("pointer-check"));
     remove_virtual_functions(symbol_table, goto_functions);
 
+    // do partial inlining
+    status() << "Partial Inlining" << eom;
+    goto_partial_inline(goto_functions, ns, ui_message_handler);
+
+    // remove returns, gcc vectors, complex
+    remove_returns(symbol_table, goto_functions);
+    remove_vector(symbol_table, goto_functions);
+    remove_complex(symbol_table, goto_functions);
+
+    // add generic checks
+    status() << "Generic Property Instrumentation" << eom;
+    goto_check(ns, options, goto_functions);
+
     // full slice?
     if(cmdline.isset("full-slice"))
     {
@@ -875,6 +888,7 @@ bool cbmc_parse_optionst::process_goto_program(
       }
     }
 
+<<<<<<< fada6185d03028840f415fda8f5ab057218a602c
     // do partial inlining
     status() << "Partial Inlining" << eom;
     goto_partial_inline(goto_functions, ns, ui_message_handler);

From c57f66383a75e4e764b58815c18b87ea2672a756 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Wed, 28 Dec 2016 16:14:46 +0000
Subject: [PATCH 21/23] check whether a given state exists before adding
 dependencies

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/analyses/ai.h                   |  8 ++++++++
 src/goto-instrument/full_slicer.cpp | 19 +++++++++++--------
 2 files changed, 19 insertions(+), 8 deletions(-)

diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index a0938b514bc..c8e6dff9d57 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -274,6 +274,14 @@ class ait:public ai_baset
     ai_baset::clear();
   }
 
+  // this one just finds states
+  virtual const bool state_exist(locationt l) const
+  {
+    typename state_mapt::const_iterator it=state_map.find(l);
+    if(it==state_map.end()) return false;
+    return true;
+  }
+
 protected:
   typedef hash_map_cont<locationt, domainT, const_target_hash> state_mapt;
   state_mapt state_map;
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 54dd954a54e..aa9e09c6d4b 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -41,14 +41,17 @@ void full_slicert::add_dependencies(
   const dependence_grapht &dep_graph,
   const dep_node_to_cfgt &dep_node_to_cfg)
 {
-  const dependence_grapht::nodet &d_node=
-    dep_graph[dep_graph[node.PC].get_node_id()];
-
-  for(dependence_grapht::edgest::const_iterator
-      it=d_node.in.begin();
-      it!=d_node.in.end();
-      ++it)
-    add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
+  if (dep_graph.state_exist(node.PC))
+  {
+    const dependence_grapht::nodet &d_node=
+      dep_graph[dep_graph[node.PC].get_node_id()];
+
+    for(dependence_grapht::edgest::const_iterator
+        it=d_node.in.begin();
+        it!=d_node.in.end();
+        ++it)
+      add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
+  }
 }
 
 /*******************************************************************\

From 517fbd266fb66bce0f71a741329ba0edd81d8577 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Wed, 28 Dec 2016 16:39:51 +0000
Subject: [PATCH 22/23] fix merge conflict in cbmc_parse_options.cpp

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/cbmc/cbmc_parse_options.cpp | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 0cacfec3ba5..6d928df72ce 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -868,6 +868,7 @@ bool cbmc_parse_optionst::process_goto_program(
     status() << "Generic Property Instrumentation" << eom;
     goto_check(ns, options, goto_functions);
 
+<<<<<<< c57f66383a75e4e764b58815c18b87ea2672a756
     // full slice?
     if(cmdline.isset("full-slice"))
     {
@@ -977,6 +978,30 @@ bool cbmc_parse_optionst::process_goto_program(
     // remove skips
     remove_skip(goto_functions);
     goto_functions.update();
+
+    // full slice?
+    if(cmdline.isset("full-slice"))
+    {
+      status() << "Performing a full slice" << eom;
+      remove_virtual_functions(symbol_table,goto_functions);
+      remove_function_pointers(symbol_table,goto_functions,cmdline.isset("pointer-check"));
+      remove_returns(symbol_table,goto_functions);
+      goto_functions.update();
+
+      //status() << "Performing full inlining" << eom;
+      //goto_inline(goto_functions, ns, ui_message_handler);
+
+      try
+      {
+        full_slicer(goto_functions, ns);
+      }
+
+      catch(const char *error_msg)
+      {
+        error() << error_msg << eom;
+        return 1;
+      }
+    }
   }
 
   catch(const char *e)

From 3bbca7c1935733a427b7c637bd86e7bee0d047fe Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Tue, 3 Jan 2017 15:51:21 +0000
Subject: [PATCH 23/23] check for array_copy during the implicit call

Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
---
 src/cbmc/cbmc_parse_options.cpp       | 26 --------------------------
 src/goto-instrument/full_slicer.cpp   |  5 ++++-
 src/pointer-analysis/value_set_fi.cpp |  2 +-
 3 files changed, 5 insertions(+), 28 deletions(-)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 6d928df72ce..9ed14620649 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -868,7 +868,6 @@ bool cbmc_parse_optionst::process_goto_program(
     status() << "Generic Property Instrumentation" << eom;
     goto_check(ns, options, goto_functions);
 
-<<<<<<< c57f66383a75e4e764b58815c18b87ea2672a756
     // full slice?
     if(cmdline.isset("full-slice"))
     {
@@ -889,7 +888,6 @@ bool cbmc_parse_optionst::process_goto_program(
       }
     }
 
-<<<<<<< fada6185d03028840f415fda8f5ab057218a602c
     // do partial inlining
     status() << "Partial Inlining" << eom;
     goto_partial_inline(goto_functions, ns, ui_message_handler);
@@ -978,30 +976,6 @@ bool cbmc_parse_optionst::process_goto_program(
     // remove skips
     remove_skip(goto_functions);
     goto_functions.update();
-
-    // full slice?
-    if(cmdline.isset("full-slice"))
-    {
-      status() << "Performing a full slice" << eom;
-      remove_virtual_functions(symbol_table,goto_functions);
-      remove_function_pointers(symbol_table,goto_functions,cmdline.isset("pointer-check"));
-      remove_returns(symbol_table,goto_functions);
-      goto_functions.update();
-
-      //status() << "Performing full inlining" << eom;
-      //goto_inline(goto_functions, ns, ui_message_handler);
-
-      try
-      {
-        full_slicer(goto_functions, ns);
-      }
-
-      catch(const char *error_msg)
-      {
-        error() << error_msg << eom;
-        return 1;
-      }
-    }
   }
 
   catch(const char *e)
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index aa9e09c6d4b..9b1959ecc7f 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -277,7 +277,7 @@ void full_slicert::fixedpoint(
 {
   std::vector<cfgt::entryt> dep_node_to_cfg;
   dep_node_to_cfg.reserve(dep_graph.size());
-  for(dependence_grapht::node_indext i=0; i<dep_graph.size(); ++i)
+  for(unsigned i=0; i<dep_graph.size(); ++i)
   {
     cfgt::entry_mapt::const_iterator entry=
       cfg.entry_map.find(dep_graph[i].PC);
@@ -333,6 +333,9 @@ static bool implicit(const namespacet &ns, goto_programt::const_targett target)
 {
   // some variables are used during symbolic execution only
 
+  const irep_idt &statement=target->code.get(ID_statement);
+  if (statement==ID_array_copy) return true;
+
   if (target->is_assume()) return true;
   if(!target->is_assign()) return false;
 
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 757ed750e54..90acadc1dcc 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -1723,7 +1723,7 @@ void value_set_fit::apply_code(
   {
 	  // doesn't do anything
   }
-  else if(statement==ID_output)
+  else if(statement==ID_array_copy)
   {
     // doesn't do anything
   }