From 1309671e95ba3e1d203c87d1782314c0afba6aea Mon Sep 17 00:00:00 2001
From: Daniel Neville <daniel.neville@cs.ox.ac.uk>
Date: Wed, 21 Sep 2016 13:28:51 +0100
Subject: [PATCH 1/9] Errors

---
 regression/cbmc-concurrency/deadlock1/main.c  |  44 +--
 regression/cbmc-concurrency/deadlock2/main.c  |  46 +--
 .../cbmc-concurrency/norace_array1/main.c     |  52 +--
 .../cbmc-concurrency/norace_scalar1/main.c    |  52 +--
 .../cbmc-concurrency/norace_struct1/main.c    |  52 +--
 .../cbmc-concurrency/struct_and_array1/main.c |  80 ++---
 .../cbmc-from-CVS/Struct_Pointer2/main.c      |  54 +--
 .../cbmc-from-CVS/Unbounded_Array5/main.c     |  40 +--
 .../cbmc-from-CVS/return2/tcas_v23_523.c      | 336 +++++++++---------
 regression/cbmc-with-incr/Float-div1/main.c   | 100 +++---
 .../cbmc-with-incr/Float-to-double2/main.c    |  24 +-
 regression/cbmc-with-incr/Float19/main.c      |  48 +--
 regression/cbmc-with-incr/Float20/main.c      | 112 +++---
 regression/cbmc-with-incr/Float21/main.c      | 132 +++----
 regression/cbmc-with-incr/Recursion4/main.c   |  34 +-
 regression/cpp-from-CVS/Array1/main.cpp       |  22 +-
 regression/cpp-from-CVS/Array2/main.cpp       |  22 +-
 regression/cpp/Decltype2/main.cpp             |  28 +-
 regression/cpp/Decltype3/main.cpp             |  36 +-
 19 files changed, 657 insertions(+), 657 deletions(-)

diff --git a/regression/cbmc-concurrency/deadlock1/main.c b/regression/cbmc-concurrency/deadlock1/main.c
index 2e134bc5f9d..891fb419e7e 100644
--- a/regression/cbmc-concurrency/deadlock1/main.c
+++ b/regression/cbmc-concurrency/deadlock1/main.c
@@ -1,22 +1,22 @@
-#include <pthread.h>
-#include <stdlib.h>
-#include <assert.h>
-
-pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
-
-void* lock_never_unlock_002_tsk_001(void* pram) { 
-  pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);  
-  return NULL; 
-} 
-
-void main() { 
-  pthread_t tid1; 
-  pthread_t tid2; 
-  pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL); 
-  pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL); 
-  pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL); 
-  pthread_join(tid1, NULL); 
-  pthread_join(tid2, NULL); 
-  // deadlock in the threads; assertion should not be reachable
-  assert(0);
-} 
+#include <pthread.h>
+#include <stdlib.h>
+#include <assert.h>
+
+pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void* lock_never_unlock_002_tsk_001(void* pram) { 
+  pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);  
+  return NULL; 
+} 
+
+void main() { 
+  pthread_t tid1; 
+  pthread_t tid2; 
+  pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL); 
+  pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL); 
+  pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL); 
+  pthread_join(tid1, NULL); 
+  pthread_join(tid2, NULL); 
+  // deadlock in the threads; assertion should not be reachable
+  assert(0);
+} 
diff --git a/regression/cbmc-concurrency/deadlock2/main.c b/regression/cbmc-concurrency/deadlock2/main.c
index c2ebc9b9a01..d8000f2027d 100644
--- a/regression/cbmc-concurrency/deadlock2/main.c
+++ b/regression/cbmc-concurrency/deadlock2/main.c
@@ -1,23 +1,23 @@
-#include <pthread.h>
-#include <stdlib.h>
-#include <assert.h>
-
-pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
-
-void* lock_never_unlock_002_tsk_001(void* pram) { 
-  pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);  
-  pthread_mutex_unlock(&lock_never_unlock_002_glb_mutex);  
-  return NULL; 
-} 
-
-void main() { 
-  pthread_t tid1; 
-  pthread_t tid2; 
-  pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL); 
-  pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL); 
-  pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL); 
-  pthread_join(tid1, NULL); 
-  pthread_join(tid2, NULL); 
-  // no deadlock in the threads; assertion should be reached
-  assert(0);
-} 
+#include <pthread.h>
+#include <stdlib.h>
+#include <assert.h>
+
+pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void* lock_never_unlock_002_tsk_001(void* pram) { 
+  pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);  
+  pthread_mutex_unlock(&lock_never_unlock_002_glb_mutex);  
+  return NULL; 
+} 
+
+void main() { 
+  pthread_t tid1; 
+  pthread_t tid2; 
+  pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL); 
+  pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL); 
+  pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL); 
+  pthread_join(tid1, NULL); 
+  pthread_join(tid2, NULL); 
+  // no deadlock in the threads; assertion should be reached
+  assert(0);
+} 
diff --git a/regression/cbmc-concurrency/norace_array1/main.c b/regression/cbmc-concurrency/norace_array1/main.c
index debc6871438..721065d6182 100644
--- a/regression/cbmc-concurrency/norace_array1/main.c
+++ b/regression/cbmc-concurrency/norace_array1/main.c
@@ -1,26 +1,26 @@
-#include <pthread.h>
-#include <assert.h>
-
-int s[2];
-
-void* thread_0(void* arg)
-{
-  s[0] = 2;
-  assert(s[0] == 2);
-  return NULL;
-}
-
-void* thread_1(void* arg)
-{
-  s[1] = 1;
-  assert(s[1] == 1);
-  return NULL;
-}
-
-int main(void)
-{
-  pthread_t thread0, thread1;
-  pthread_create(&thread0, NULL, thread_0, 0);
-  pthread_create(&thread1, NULL, thread_1, 0);
-  return 0;
-}
+#include <pthread.h>
+#include <assert.h>
+
+int s[2];
+
+void* thread_0(void* arg)
+{
+  s[0] = 2;
+  assert(s[0] == 2);
+  return NULL;
+}
+
+void* thread_1(void* arg)
+{
+  s[1] = 1;
+  assert(s[1] == 1);
+  return NULL;
+}
+
+int main(void)
+{
+  pthread_t thread0, thread1;
+  pthread_create(&thread0, NULL, thread_0, 0);
+  pthread_create(&thread1, NULL, thread_1, 0);
+  return 0;
+}
diff --git a/regression/cbmc-concurrency/norace_scalar1/main.c b/regression/cbmc-concurrency/norace_scalar1/main.c
index 8c39510fd73..eb5baf7fd6a 100644
--- a/regression/cbmc-concurrency/norace_scalar1/main.c
+++ b/regression/cbmc-concurrency/norace_scalar1/main.c
@@ -1,26 +1,26 @@
-#include <pthread.h>
-#include <assert.h>
-
-int f0, f1;
-
-void* thread_0(void* arg)
-{
-  f0 = 2;
-  assert(f0 == 2);
-  return NULL;
-}
-
-void* thread_1(void* arg)
-{
-  f1 = 1;
-  assert(f1 == 1);
-  return NULL;
-}
-
-int main(void)
-{
-  pthread_t thread0, thread1;
-  pthread_create(&thread0, NULL, thread_0, 0);
-  pthread_create(&thread1, NULL, thread_1, 0);
-  return 0;
-}
+#include <pthread.h>
+#include <assert.h>
+
+int f0, f1;
+
+void* thread_0(void* arg)
+{
+  f0 = 2;
+  assert(f0 == 2);
+  return NULL;
+}
+
+void* thread_1(void* arg)
+{
+  f1 = 1;
+  assert(f1 == 1);
+  return NULL;
+}
+
+int main(void)
+{
+  pthread_t thread0, thread1;
+  pthread_create(&thread0, NULL, thread_0, 0);
+  pthread_create(&thread1, NULL, thread_1, 0);
+  return 0;
+}
diff --git a/regression/cbmc-concurrency/norace_struct1/main.c b/regression/cbmc-concurrency/norace_struct1/main.c
index 1fca06df093..31dd7e324e3 100644
--- a/regression/cbmc-concurrency/norace_struct1/main.c
+++ b/regression/cbmc-concurrency/norace_struct1/main.c
@@ -1,26 +1,26 @@
-#include <pthread.h>
-#include <assert.h>
-
-struct { int f0; int f1; } s;
-
-void* thread_0(void* arg)
-{
-  s.f0 = 2;
-  assert(s.f0 == 2);
-  return NULL;
-}
-
-void* thread_1(void* arg)
-{
-  s.f1 = 1;
-  assert(s.f1 == 1);
-  return NULL;
-}
-
-int main(void)
-{
-  pthread_t thread0, thread1;
-  pthread_create(&thread0, NULL, thread_0, 0);
-  pthread_create(&thread1, NULL, thread_1, 0);
-  return 0;
-}
+#include <pthread.h>
+#include <assert.h>
+
+struct { int f0; int f1; } s;
+
+void* thread_0(void* arg)
+{
+  s.f0 = 2;
+  assert(s.f0 == 2);
+  return NULL;
+}
+
+void* thread_1(void* arg)
+{
+  s.f1 = 1;
+  assert(s.f1 == 1);
+  return NULL;
+}
+
+int main(void)
+{
+  pthread_t thread0, thread1;
+  pthread_create(&thread0, NULL, thread_0, 0);
+  pthread_create(&thread1, NULL, thread_1, 0);
+  return 0;
+}
diff --git a/regression/cbmc-concurrency/struct_and_array1/main.c b/regression/cbmc-concurrency/struct_and_array1/main.c
index cc3dd606089..42164904232 100644
--- a/regression/cbmc-concurrency/struct_and_array1/main.c
+++ b/regression/cbmc-concurrency/struct_and_array1/main.c
@@ -1,40 +1,40 @@
-#include <pthread.h>
-
-typedef struct st_t
-{
-  unsigned char x;
-  unsigned char y;
-} ST;
-
-ST st;
-
-char my_array[10];
-
-_Bool done1, done2;
-
-void *foo1(void *arg1)
-{
-  st.x = 1;
-  my_array[1]=1;
-  done1 = 1;
-}
-
-void *foo2(void *arg2)
-{
-  st.y = 1;
-  my_array[2]=2;
-  done2 = 1;
-}
-
-int main()
-{
-  pthread_t t;
-  pthread_create(&t,NULL,foo1,NULL);
-  pthread_create(&t,NULL,foo2,NULL);
-  
-  if(done1 && done2)
-  {
-    assert(st.x==st.y);
-    assert(my_array[1]==my_array[2]);
-  }
-}
+#include <pthread.h>
+
+typedef struct st_t
+{
+  unsigned char x;
+  unsigned char y;
+} ST;
+
+ST st;
+
+char my_array[10];
+
+_Bool done1, done2;
+
+void *foo1(void *arg1)
+{
+  st.x = 1;
+  my_array[1]=1;
+  done1 = 1;
+}
+
+void *foo2(void *arg2)
+{
+  st.y = 1;
+  my_array[2]=2;
+  done2 = 1;
+}
+
+int main()
+{
+  pthread_t t;
+  pthread_create(&t,NULL,foo1,NULL);
+  pthread_create(&t,NULL,foo2,NULL);
+  
+  if(done1 && done2)
+  {
+    assert(st.x==st.y);
+    assert(my_array[1]==my_array[2]);
+  }
+}
diff --git a/regression/cbmc-from-CVS/Struct_Pointer2/main.c b/regression/cbmc-from-CVS/Struct_Pointer2/main.c
index b50cfcd0f97..bf8ab0817c2 100644
--- a/regression/cbmc-from-CVS/Struct_Pointer2/main.c
+++ b/regression/cbmc-from-CVS/Struct_Pointer2/main.c
@@ -1,27 +1,27 @@
-#include <stdlib.h>
-#include <assert.h>
-
-struct mylist
-{
-  int  data;
-  struct mylist *next;
-};
-
-int main()
-{
-  struct mylist *p;
-
-  // Allocations:
-  p=malloc( sizeof(struct mylist ) );  
-  p->data=1;
-  p->next=malloc( sizeof(struct mylist ) );  
-  p->next->data=2;
-  p->next->next=malloc( sizeof(struct mylist ) );    
-  p->next->next->data=3;
-  p->next->next->next=malloc( sizeof(struct mylist ) );    
-  p->next->next->next->data=4;
-  
-  assert(p->next->next->data==3);
-
-  return 0;
-}
+#include <stdlib.h>
+#include <assert.h>
+
+struct mylist
+{
+  int  data;
+  struct mylist *next;
+};
+
+int main()
+{
+  struct mylist *p;
+
+  // Allocations:
+  p=malloc( sizeof(struct mylist ) );  
+  p->data=1;
+  p->next=malloc( sizeof(struct mylist ) );  
+  p->next->data=2;
+  p->next->next=malloc( sizeof(struct mylist ) );    
+  p->next->next->data=3;
+  p->next->next->next=malloc( sizeof(struct mylist ) );    
+  p->next->next->next->data=4;
+  
+  assert(p->next->next->data==3);
+
+  return 0;
+}
diff --git a/regression/cbmc-from-CVS/Unbounded_Array5/main.c b/regression/cbmc-from-CVS/Unbounded_Array5/main.c
index d797c3c2923..aebfa1e3a94 100644
--- a/regression/cbmc-from-CVS/Unbounded_Array5/main.c
+++ b/regression/cbmc-from-CVS/Unbounded_Array5/main.c
@@ -1,20 +1,20 @@
-int mem[__CPROVER_constant_infinity_uint];
-
-int  main()
-{
-  int i, j, mem_j;
-  
-  mem[0] = 0;
-  mem[1] = 1;
-
-  mem[j] = 1;
-  mem_j = mem[j];
-  assert(mem_j == 1);
-
-  mem[i] = mem[mem_j];
-   
-  unsigned xxxi=mem[i];
-  unsigned xxx1=mem[1];
-
-  __CPROVER_assert(xxxi == xxx1, "Check infinite mem");
-}
+int mem[__CPROVER_constant_infinity_uint];
+
+int  main()
+{
+  int i, j, mem_j;
+  
+  mem[0] = 0;
+  mem[1] = 1;
+
+  mem[j] = 1;
+  mem_j = mem[j];
+  assert(mem_j == 1);
+
+  mem[i] = mem[mem_j];
+   
+  unsigned xxxi=mem[i];
+  unsigned xxx1=mem[1];
+
+  __CPROVER_assert(xxxi == xxx1, "Check infinite mem");
+}
diff --git a/regression/cbmc-from-CVS/return2/tcas_v23_523.c b/regression/cbmc-from-CVS/return2/tcas_v23_523.c
index 6670715a6d2..4504d9c4dd4 100644
--- a/regression/cbmc-from-CVS/return2/tcas_v23_523.c
+++ b/regression/cbmc-from-CVS/return2/tcas_v23_523.c
@@ -1,171 +1,171 @@
-
-/*  -*- Last-Edit:  Fri Jan 29 11:13:27 1993 by Tarak S. Goradia; -*- */
+
+/*  -*- Last-Edit:  Fri Jan 29 11:13:27 1993 by Tarak S. Goradia; -*- */
 /* $Log: tcas_v23_523.c,v $
 /* Revision 1.1  2006-04-04 08:38:22  kroening
 /* more
-/*
- * Revision 1.2  1993/03/12  19:29:50  foster
- * Correct logic bug which didn't allow output of 2 - hf
- * */
-
-#include <stdio.h>
-
-#define OLEV       600		/* in feets/minute */
-#define MAXALTDIFF 600		/* max altitude difference in feet */
-#define MINSEP     300          /* min separation in feet */
-#define NOZCROSS   100		/* in feet */
-				/* variables */
-
-typedef int bool;
-
-int Cur_Vertical_Sep;
-bool High_Confidence;
-bool Two_of_Three_Reports_Valid;
-
-int Own_Tracked_Alt;
-int Own_Tracked_Alt_Rate;
-int Other_Tracked_Alt;
-
-int Alt_Layer_Value;		/* 0, 1, 2, 3 */
-int Positive_RA_Alt_Thresh[4];
-
-int Up_Separation;
-int Down_Separation;
-
-				/* state variables */
-int Other_RAC;			/* NO_INTENT, DO_NOT_CLIMB, DO_NOT_DESCEND */
-#define NO_INTENT 0
-#define DO_NOT_CLIMB 1
-#define DO_NOT_DESCEND 2
-
-int Other_Capability;		/* TCAS_TA, OTHER */
-#define TCAS_TA 1
-#define OTHER 2
-
-int Climb_Inhibit;		/* true/false */
-
-#define UNRESOLVED 0
-#define UPWARD_RA 1
-#define DOWNWARD_RA 2
-
-int  ALIM();
-int  Inhibit_Biased_Climb();
-bool   Non_Crossing_Biased_Climb();
-bool   Non_Crossing_Biased_Descend();
-bool   Own_Below_Threat();
-bool   Own_Above_Threat();
-int  alt_sep_test();
-void initialize()
-{
-    Positive_RA_Alt_Thresh[0] = 400;
-    Positive_RA_Alt_Thresh[1] = 500;
-    Positive_RA_Alt_Thresh[2] = 640;
-    Positive_RA_Alt_Thresh[3] = 740;
-}
-
-int ALIM ()
-{
- return Positive_RA_Alt_Thresh[Alt_Layer_Value];
-}
-
-int Inhibit_Biased_Climb ()
-{
-    return (Climb_Inhibit ? Up_Separation + NOZCROSS : Up_Separation);
-}
-
-bool Non_Crossing_Biased_Climb()
-{
-    int upward_preferred;
-    int upward_crossing_situation;
-    bool result;
-
-    upward_preferred = Inhibit_Biased_Climb() > Down_Separation;
-    if (upward_preferred)
-    {
-	result = !(Own_Below_Threat()) || ((Own_Below_Threat()) && (!(Down_Separation >= ALIM())));
-    }
-    else
-    {	
-	result = Own_Above_Threat() && (Cur_Vertical_Sep >= MINSEP) && (Up_Separation >= ALIM());
-    }
-    return result;
-}
-
-bool Non_Crossing_Biased_Descend()
-{
-    int upward_preferred;
-    int upward_crossing_situation;
-    bool result;
-
-    upward_preferred = (Up_Separation + NOZCROSS) > Down_Separation;
-    if (upward_preferred)
-    {
-	result = Own_Below_Threat() && (Cur_Vertical_Sep >= MINSEP) && (Down_Separation >= ALIM());
-    }
-    else
-    {
-	result = !(Own_Above_Threat()) || ((Own_Above_Threat()) && (Up_Separation >= ALIM()));
-    }
-    return result;
-}
-
-bool Own_Below_Threat()
-{
-    return (Own_Tracked_Alt < Other_Tracked_Alt);
-}
-
-bool Own_Above_Threat()
-{
-    return (Other_Tracked_Alt < Own_Tracked_Alt);
-}
-
-int alt_sep_test()
-{
-    bool enabled, tcas_equipped, intent_not_known;
-    bool need_upward_RA, need_downward_RA;
-    int alt_sep;
-
-    enabled = High_Confidence && (Own_Tracked_Alt_Rate <= OLEV) && (Cur_Vertical_Sep > MAXALTDIFF);
-    tcas_equipped = Other_Capability == TCAS_TA;
-    intent_not_known = Two_of_Three_Reports_Valid && Other_RAC == NO_INTENT;
-    
-    alt_sep = UNRESOLVED;
-    
-    if (enabled && ((tcas_equipped && intent_not_known) || !tcas_equipped))
-    {
-	need_upward_RA = Non_Crossing_Biased_Climb() && Own_Below_Threat();
-	need_downward_RA = Non_Crossing_Biased_Descend() && Own_Above_Threat();
-	if (need_upward_RA && need_downward_RA)
-        /* unreachable: requires Own_Below_Threat and Own_Above_Threat
-           to both be true - that requires Own_Tracked_Alt < Other_Tracked_Alt
-           and Other_Tracked_Alt < Own_Tracked_Alt, which isn't possible */
-	    alt_sep = UNRESOLVED;
-	else if (need_upward_RA)
-	    alt_sep = UPWARD_RA;
-	else if (need_downward_RA)
-	    alt_sep = DOWNWARD_RA;
-	else
-	    alt_sep = UNRESOLVED;
-    }
-    
-    return alt_sep;
-}
-
-main(int argc, char*argv[])
-{
-
-  initialize();
-  Cur_Vertical_Sep =  860; 
-  High_Confidence = 1; 
-  Two_of_Three_Reports_Valid = 1; 
-  Own_Tracked_Alt =  618; 
-  Own_Tracked_Alt_Rate =  329; 
-  Other_Tracked_Alt =  574; 
-  Alt_Layer_Value =  4; 
-  Up_Separation =  893; 
-  Down_Separation =  914; 
-  Other_RAC =  0; 
-  Other_Capability =  2; 
-  Climb_Inhibit =  0; 
-  assert(alt_sep_test()==0);
-}
+/*
+ * Revision 1.2  1993/03/12  19:29:50  foster
+ * Correct logic bug which didn't allow output of 2 - hf
+ * */
+
+#include <stdio.h>
+
+#define OLEV       600		/* in feets/minute */
+#define MAXALTDIFF 600		/* max altitude difference in feet */
+#define MINSEP     300          /* min separation in feet */
+#define NOZCROSS   100		/* in feet */
+				/* variables */
+
+typedef int bool;
+
+int Cur_Vertical_Sep;
+bool High_Confidence;
+bool Two_of_Three_Reports_Valid;
+
+int Own_Tracked_Alt;
+int Own_Tracked_Alt_Rate;
+int Other_Tracked_Alt;
+
+int Alt_Layer_Value;		/* 0, 1, 2, 3 */
+int Positive_RA_Alt_Thresh[4];
+
+int Up_Separation;
+int Down_Separation;
+
+				/* state variables */
+int Other_RAC;			/* NO_INTENT, DO_NOT_CLIMB, DO_NOT_DESCEND */
+#define NO_INTENT 0
+#define DO_NOT_CLIMB 1
+#define DO_NOT_DESCEND 2
+
+int Other_Capability;		/* TCAS_TA, OTHER */
+#define TCAS_TA 1
+#define OTHER 2
+
+int Climb_Inhibit;		/* true/false */
+
+#define UNRESOLVED 0
+#define UPWARD_RA 1
+#define DOWNWARD_RA 2
+
+int  ALIM();
+int  Inhibit_Biased_Climb();
+bool   Non_Crossing_Biased_Climb();
+bool   Non_Crossing_Biased_Descend();
+bool   Own_Below_Threat();
+bool   Own_Above_Threat();
+int  alt_sep_test();
+void initialize()
+{
+    Positive_RA_Alt_Thresh[0] = 400;
+    Positive_RA_Alt_Thresh[1] = 500;
+    Positive_RA_Alt_Thresh[2] = 640;
+    Positive_RA_Alt_Thresh[3] = 740;
+}
+
+int ALIM ()
+{
+ return Positive_RA_Alt_Thresh[Alt_Layer_Value];
+}
+
+int Inhibit_Biased_Climb ()
+{
+    return (Climb_Inhibit ? Up_Separation + NOZCROSS : Up_Separation);
+}
+
+bool Non_Crossing_Biased_Climb()
+{
+    int upward_preferred;
+    int upward_crossing_situation;
+    bool result;
+
+    upward_preferred = Inhibit_Biased_Climb() > Down_Separation;
+    if (upward_preferred)
+    {
+	result = !(Own_Below_Threat()) || ((Own_Below_Threat()) && (!(Down_Separation >= ALIM())));
+    }
+    else
+    {	
+	result = Own_Above_Threat() && (Cur_Vertical_Sep >= MINSEP) && (Up_Separation >= ALIM());
+    }
+    return result;
+}
+
+bool Non_Crossing_Biased_Descend()
+{
+    int upward_preferred;
+    int upward_crossing_situation;
+    bool result;
+
+    upward_preferred = (Up_Separation + NOZCROSS) > Down_Separation;
+    if (upward_preferred)
+    {
+	result = Own_Below_Threat() && (Cur_Vertical_Sep >= MINSEP) && (Down_Separation >= ALIM());
+    }
+    else
+    {
+	result = !(Own_Above_Threat()) || ((Own_Above_Threat()) && (Up_Separation >= ALIM()));
+    }
+    return result;
+}
+
+bool Own_Below_Threat()
+{
+    return (Own_Tracked_Alt < Other_Tracked_Alt);
+}
+
+bool Own_Above_Threat()
+{
+    return (Other_Tracked_Alt < Own_Tracked_Alt);
+}
+
+int alt_sep_test()
+{
+    bool enabled, tcas_equipped, intent_not_known;
+    bool need_upward_RA, need_downward_RA;
+    int alt_sep;
+
+    enabled = High_Confidence && (Own_Tracked_Alt_Rate <= OLEV) && (Cur_Vertical_Sep > MAXALTDIFF);
+    tcas_equipped = Other_Capability == TCAS_TA;
+    intent_not_known = Two_of_Three_Reports_Valid && Other_RAC == NO_INTENT;
+    
+    alt_sep = UNRESOLVED;
+    
+    if (enabled && ((tcas_equipped && intent_not_known) || !tcas_equipped))
+    {
+	need_upward_RA = Non_Crossing_Biased_Climb() && Own_Below_Threat();
+	need_downward_RA = Non_Crossing_Biased_Descend() && Own_Above_Threat();
+	if (need_upward_RA && need_downward_RA)
+        /* unreachable: requires Own_Below_Threat and Own_Above_Threat
+           to both be true - that requires Own_Tracked_Alt < Other_Tracked_Alt
+           and Other_Tracked_Alt < Own_Tracked_Alt, which isn't possible */
+	    alt_sep = UNRESOLVED;
+	else if (need_upward_RA)
+	    alt_sep = UPWARD_RA;
+	else if (need_downward_RA)
+	    alt_sep = DOWNWARD_RA;
+	else
+	    alt_sep = UNRESOLVED;
+    }
+    
+    return alt_sep;
+}
+
+main(int argc, char*argv[])
+{
+
+  initialize();
+  Cur_Vertical_Sep =  860; 
+  High_Confidence = 1; 
+  Two_of_Three_Reports_Valid = 1; 
+  Own_Tracked_Alt =  618; 
+  Own_Tracked_Alt_Rate =  329; 
+  Other_Tracked_Alt =  574; 
+  Alt_Layer_Value =  4; 
+  Up_Separation =  893; 
+  Down_Separation =  914; 
+  Other_RAC =  0; 
+  Other_Capability =  2; 
+  Climb_Inhibit =  0; 
+  assert(alt_sep_test()==0);
+}
diff --git a/regression/cbmc-with-incr/Float-div1/main.c b/regression/cbmc-with-incr/Float-div1/main.c
index dee31965dac..63f8512a7c2 100644
--- a/regression/cbmc-with-incr/Float-div1/main.c
+++ b/regression/cbmc-with-incr/Float-div1/main.c
@@ -1,50 +1,50 @@
-#include <assert.h>
-#include <math.h>
-
-#ifdef __GNUC__
-void inductiveStepHunt (float startState)
-{
-  float target = 0x1.fffffep-3f;
-
-  __CPROVER_assume((0 < startState) && (fpclassify(startState) == FP_NORMAL) && (0x1p-126f <= startState));
-
-  float secondPoint = (target / startState);
-
-  float nextState = (startState + secondPoint) / 2;
-
-  float oneAfter = (target / nextState);
-
-  assert(oneAfter > 0);
-}
-
-void simplifiedInductiveStepHunt (float nextState)
-{
-  float target = 0x1.fffffep-3f;
-
-  // Implies nextState == 0x1p+124f;
-  __CPROVER_assume((0x1.fffffep+123f < nextState) && (nextState < 0x1.000002p+124f));
-  
-  float oneAfter = (target / nextState);
-
-  // Is true and correctly proven by constant evaluation
-  // Note that this is the smallest normal number
-  assert(0x1.fffffep-3f / 0x1p+124f == 0x1p-126f);
-
-  assert(oneAfter > 0);
-}
-#endif
-
-int main (void)
-{
-  #ifdef __GNUC__
-  //  inductiveStepHunt(0x1p+125f);
-  //  simplifiedInductiveStepHunt(0x1p+124f);
-
-  float f, g;
-
-  inductiveStepHunt(f);
-  simplifiedInductiveStepHunt(g);
-  #endif
-
-  return 0;
-}
+#include <assert.h>
+#include <math.h>
+
+#ifdef __GNUC__
+void inductiveStepHunt (float startState)
+{
+  float target = 0x1.fffffep-3f;
+
+  __CPROVER_assume((0 < startState) && (fpclassify(startState) == FP_NORMAL) && (0x1p-126f <= startState));
+
+  float secondPoint = (target / startState);
+
+  float nextState = (startState + secondPoint) / 2;
+
+  float oneAfter = (target / nextState);
+
+  assert(oneAfter > 0);
+}
+
+void simplifiedInductiveStepHunt (float nextState)
+{
+  float target = 0x1.fffffep-3f;
+
+  // Implies nextState == 0x1p+124f;
+  __CPROVER_assume((0x1.fffffep+123f < nextState) && (nextState < 0x1.000002p+124f));
+  
+  float oneAfter = (target / nextState);
+
+  // Is true and correctly proven by constant evaluation
+  // Note that this is the smallest normal number
+  assert(0x1.fffffep-3f / 0x1p+124f == 0x1p-126f);
+
+  assert(oneAfter > 0);
+}
+#endif
+
+int main (void)
+{
+  #ifdef __GNUC__
+  //  inductiveStepHunt(0x1p+125f);
+  //  simplifiedInductiveStepHunt(0x1p+124f);
+
+  float f, g;
+
+  inductiveStepHunt(f);
+  simplifiedInductiveStepHunt(g);
+  #endif
+
+  return 0;
+}
diff --git a/regression/cbmc-with-incr/Float-to-double2/main.c b/regression/cbmc-with-incr/Float-to-double2/main.c
index 43ab0927eab..2db129fd08f 100644
--- a/regression/cbmc-with-incr/Float-to-double2/main.c
+++ b/regression/cbmc-with-incr/Float-to-double2/main.c
@@ -1,12 +1,12 @@
-#include <assert.h>
-
-int main(void)
-{
-  float f   = -0x1.0p-127f;
-  double d  = -0x1.0p-127;
-  double fp = (double)f;
-
-  assert(d == fp);
-
-  return 0;
-}
+#include <assert.h>
+
+int main(void)
+{
+  float f   = -0x1.0p-127f;
+  double d  = -0x1.0p-127;
+  double fp = (double)f;
+
+  assert(d == fp);
+
+  return 0;
+}
diff --git a/regression/cbmc-with-incr/Float19/main.c b/regression/cbmc-with-incr/Float19/main.c
index bc09c89924d..56b5548c602 100644
--- a/regression/cbmc-with-incr/Float19/main.c
+++ b/regression/cbmc-with-incr/Float19/main.c
@@ -1,24 +1,24 @@
-#include <assert.h>
-#include <math.h>
-
-#ifdef __GNUC__
-
-void f00 (float f)
-{
-  if (f > 0x1.FFFFFEp+127) {
-    assert(isinf(f));
-  }
-}
-
-#endif
-
-int main (void)
-{
-  #ifdef __GNUC__
-  float f;
-
-  f00(f);
-  #endif
-
-  return 0;
-}
+#include <assert.h>
+#include <math.h>
+
+#ifdef __GNUC__
+
+void f00 (float f)
+{
+  if (f > 0x1.FFFFFEp+127) {
+    assert(isinf(f));
+  }
+}
+
+#endif
+
+int main (void)
+{
+  #ifdef __GNUC__
+  float f;
+
+  f00(f);
+  #endif
+
+  return 0;
+}
diff --git a/regression/cbmc-with-incr/Float20/main.c b/regression/cbmc-with-incr/Float20/main.c
index dfacc8bac6d..b730f0d4f18 100644
--- a/regression/cbmc-with-incr/Float20/main.c
+++ b/regression/cbmc-with-incr/Float20/main.c
@@ -1,56 +1,56 @@
-/*
-** 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.
-*/
-#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;
-}
-
+/*
+** 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.
+*/
+#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-with-incr/Float21/main.c b/regression/cbmc-with-incr/Float21/main.c
index e01c31684a7..883e066cdfc 100644
--- a/regression/cbmc-with-incr/Float21/main.c
+++ b/regression/cbmc-with-incr/Float21/main.c
@@ -1,66 +1,66 @@
-/*
-** subnormal-boundary.c
-**
-** Martin Brain
-** martin.brain@cs.ox.ac.uk
-** 25/07/12
-**
-** Regression tests for casting and classification around the subnormal boundary.
-**
-*/
-
-#include <assert.h>
-#include <math.h>
-
-float nondet_float(void);
-
-int main (void)
-{
-  #ifdef __GNUC__
-
-  float smallestNormalFloat = 0x1.0p-126f;
-  float largestSubnormalFloat = 0x1.fffffcp-127f;
-  
-  double v = 0x1.FFFFFFp-127;
-
-  float f;
-
-
-  // Check the encodings are correct
-  assert(fpclassify(largestSubnormalFloat) == FP_SUBNORMAL);
-
-  f = nondet_float();
-  __CPROVER_assume(fpclassify(f) == FP_SUBNORMAL);
-  assert(f <= largestSubnormalFloat);
-
-
-  assert(fpclassify(smallestNormalFloat) == FP_NORMAL);
-
-  f = nondet_float();
-  __CPROVER_assume(fpclassify(f) == FP_NORMAL);
-  assert(smallestNormalFloat <= fabs(f));
-
-  assert(largestSubnormalFloat < smallestNormalFloat);
-
-
-  // Check the ordering as doubles
-  assert(((double)largestSubnormalFloat) < ((double)smallestNormalFloat));
-  assert(((double)largestSubnormalFloat) < v);
-  assert(v < ((double)smallestNormalFloat));
-
-
-  // Check coercion to float
-  assert((float)((double)largestSubnormalFloat) == largestSubnormalFloat);
-  assert((float)((double)smallestNormalFloat) == smallestNormalFloat);
-
-  assert(((double)smallestNormalFloat) - v <= v - ((double)largestSubnormalFloat));
-  assert(((float)v) == smallestNormalFloat);
-
-  f = nondet_float();
-  __CPROVER_assume(fpclassify(f) == FP_SUBNORMAL);
-  assert( ((float)((double)f)) == f );
-  
-  #endif
-
-  return 0;
-}
+/*
+** subnormal-boundary.c
+**
+** Martin Brain
+** martin.brain@cs.ox.ac.uk
+** 25/07/12
+**
+** Regression tests for casting and classification around the subnormal boundary.
+**
+*/
+
+#include <assert.h>
+#include <math.h>
+
+float nondet_float(void);
+
+int main (void)
+{
+  #ifdef __GNUC__
+
+  float smallestNormalFloat = 0x1.0p-126f;
+  float largestSubnormalFloat = 0x1.fffffcp-127f;
+  
+  double v = 0x1.FFFFFFp-127;
+
+  float f;
+
+
+  // Check the encodings are correct
+  assert(fpclassify(largestSubnormalFloat) == FP_SUBNORMAL);
+
+  f = nondet_float();
+  __CPROVER_assume(fpclassify(f) == FP_SUBNORMAL);
+  assert(f <= largestSubnormalFloat);
+
+
+  assert(fpclassify(smallestNormalFloat) == FP_NORMAL);
+
+  f = nondet_float();
+  __CPROVER_assume(fpclassify(f) == FP_NORMAL);
+  assert(smallestNormalFloat <= fabs(f));
+
+  assert(largestSubnormalFloat < smallestNormalFloat);
+
+
+  // Check the ordering as doubles
+  assert(((double)largestSubnormalFloat) < ((double)smallestNormalFloat));
+  assert(((double)largestSubnormalFloat) < v);
+  assert(v < ((double)smallestNormalFloat));
+
+
+  // Check coercion to float
+  assert((float)((double)largestSubnormalFloat) == largestSubnormalFloat);
+  assert((float)((double)smallestNormalFloat) == smallestNormalFloat);
+
+  assert(((double)smallestNormalFloat) - v <= v - ((double)largestSubnormalFloat));
+  assert(((float)v) == smallestNormalFloat);
+
+  f = nondet_float();
+  __CPROVER_assume(fpclassify(f) == FP_SUBNORMAL);
+  assert( ((float)((double)f)) == f );
+  
+  #endif
+
+  return 0;
+}
diff --git a/regression/cbmc-with-incr/Recursion4/main.c b/regression/cbmc-with-incr/Recursion4/main.c
index 00198d60574..c2cc4c13ae1 100644
--- a/regression/cbmc-with-incr/Recursion4/main.c
+++ b/regression/cbmc-with-incr/Recursion4/main.c
@@ -1,17 +1,17 @@
-int factorial2(int i)
-{
-  if(i==0) return 1;
-
-  // tmp_result gets renamed during recursion!
-  int tmp_result;
-  tmp_result=factorial2(0);
-  return tmp_result;
-}
-
-int main()
-{
-  int result_factorial;
-  result_factorial=factorial2(1);
-  assert(result_factorial==1);
-  return 0;
-}
+int factorial2(int i)
+{
+  if(i==0) return 1;
+
+  // tmp_result gets renamed during recursion!
+  int tmp_result;
+  tmp_result=factorial2(0);
+  return tmp_result;
+}
+
+int main()
+{
+  int result_factorial;
+  result_factorial=factorial2(1);
+  assert(result_factorial==1);
+  return 0;
+}
diff --git a/regression/cpp-from-CVS/Array1/main.cpp b/regression/cpp-from-CVS/Array1/main.cpp
index 8c77e5c8f89..ba02b972c16 100644
--- a/regression/cpp-from-CVS/Array1/main.cpp
+++ b/regression/cpp-from-CVS/Array1/main.cpp
@@ -1,11 +1,11 @@
-int y[5][4][3][2];
-
-int main()
-{
-  for(int i=0; i<5; i++)
-    for(int j=0; j<4; j++)
-      for(int k=0; k<3; k++)
-        for(int l=0; l<2; l++)
-          y[i][j][k][l]=2;
-}
-
+int y[5][4][3][2];
+
+int main()
+{
+  for(int i=0; i<5; i++)
+    for(int j=0; j<4; j++)
+      for(int k=0; k<3; k++)
+        for(int l=0; l<2; l++)
+          y[i][j][k][l]=2;
+}
+
diff --git a/regression/cpp-from-CVS/Array2/main.cpp b/regression/cpp-from-CVS/Array2/main.cpp
index 5359e4e8149..0e3e35b8ad3 100644
--- a/regression/cpp-from-CVS/Array2/main.cpp
+++ b/regression/cpp-from-CVS/Array2/main.cpp
@@ -1,11 +1,11 @@
-int y[2][3][4][5];
-
-int main()
-{
-  for(int i=0; i<5; i++)
-    for(int j=0; j<4; j++)
-      for(int k=0; k<3; k++)
-        for(int l=0; l<2; l++)
-          y[i][j][k][l]=2; // out-of-bounds
-}
-
+int y[2][3][4][5];
+
+int main()
+{
+  for(int i=0; i<5; i++)
+    for(int j=0; j<4; j++)
+      for(int k=0; k<3; k++)
+        for(int l=0; l<2; l++)
+          y[i][j][k][l]=2; // out-of-bounds
+}
+
diff --git a/regression/cpp/Decltype2/main.cpp b/regression/cpp/Decltype2/main.cpp
index f315130f21a..ba26a736059 100644
--- a/regression/cpp/Decltype2/main.cpp
+++ b/regression/cpp/Decltype2/main.cpp
@@ -1,14 +1,14 @@
-// C++11
-// decltype is a C++11 feature to get the "declared type" of an expression.
-// It is similar to 'typeof' but handles reference types "properly".
-
-class base {};
-class derived : public base {};
-
-derived d;
-
-decltype(static_cast<derived *>(&d)) z;
-
-int main()
-{
-}
+// C++11
+// decltype is a C++11 feature to get the "declared type" of an expression.
+// It is similar to 'typeof' but handles reference types "properly".
+
+class base {};
+class derived : public base {};
+
+derived d;
+
+decltype(static_cast<derived *>(&d)) z;
+
+int main()
+{
+}
diff --git a/regression/cpp/Decltype3/main.cpp b/regression/cpp/Decltype3/main.cpp
index 0ded9d5c44f..e0a95f38b00 100644
--- a/regression/cpp/Decltype3/main.cpp
+++ b/regression/cpp/Decltype3/main.cpp
@@ -1,18 +1,18 @@
-// C++11
-// decltype is a C++11 feature to get the "declared type" of an expression.
-// It is similar to 'typeof' but handles reference types "properly".
-
-template <class A, class B>
-struct whatever {
-	int f00 (const B b) {
-		typedef	decltype(static_cast<A>(b)) T;
-		T z;
-		return 1;
-	}
-};
-
-whatever<int,float> thing;
-
-int main()
-{
-}
+// C++11
+// decltype is a C++11 feature to get the "declared type" of an expression.
+// It is similar to 'typeof' but handles reference types "properly".
+
+template <class A, class B>
+struct whatever {
+	int f00 (const B b) {
+		typedef	decltype(static_cast<A>(b)) T;
+		T z;
+		return 1;
+	}
+};
+
+whatever<int,float> thing;
+
+int main()
+{
+}

From fe82a6e537670ae4473eecf131eda6fbb64ff339 Mon Sep 17 00:00:00 2001
From: Daniel Neville <daniel.neville@cs.ox.ac.uk>
Date: Thu, 29 Sep 2016 11:54:13 +0100
Subject: [PATCH 2/9] Line endings issue CRLF to LF

---
 regression/cbmc-concurrency/deadlock1/main.c  |  44 +--
 regression/cbmc-concurrency/deadlock2/main.c  |  46 +--
 .../cbmc-concurrency/norace_array1/main.c     |  52 +--
 .../cbmc-concurrency/norace_scalar1/main.c    |  52 +--
 .../cbmc-concurrency/norace_struct1/main.c    |  52 +--
 .../cbmc-concurrency/struct_and_array1/main.c |  80 ++---
 .../cbmc-from-CVS/Struct_Pointer2/main.c      |  54 +--
 .../cbmc-from-CVS/Unbounded_Array5/main.c     |  40 +--
 .../cbmc-from-CVS/return2/tcas_v23_523.c      | 336 +++++++++---------
 regression/cbmc-with-incr/Float-div1/main.c   | 100 +++---
 .../cbmc-with-incr/Float-to-double2/main.c    |  24 +-
 regression/cbmc-with-incr/Float19/main.c      |  48 +--
 regression/cbmc-with-incr/Float20/main.c      | 112 +++---
 regression/cbmc-with-incr/Float21/main.c      | 132 +++----
 regression/cbmc-with-incr/Recursion4/main.c   |  34 +-
 regression/cpp-from-CVS/Array1/main.cpp       |  22 +-
 regression/cpp-from-CVS/Array2/main.cpp       |  22 +-
 regression/cpp/Decltype2/main.cpp             |  28 +-
 regression/cpp/Decltype3/main.cpp             |  36 +-
 19 files changed, 657 insertions(+), 657 deletions(-)

diff --git a/regression/cbmc-concurrency/deadlock1/main.c b/regression/cbmc-concurrency/deadlock1/main.c
index 2e134bc5f9d..891fb419e7e 100644
--- a/regression/cbmc-concurrency/deadlock1/main.c
+++ b/regression/cbmc-concurrency/deadlock1/main.c
@@ -1,22 +1,22 @@
-#include <pthread.h>
-#include <stdlib.h>
-#include <assert.h>
-
-pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
-
-void* lock_never_unlock_002_tsk_001(void* pram) { 
-  pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);  
-  return NULL; 
-} 
-
-void main() { 
-  pthread_t tid1; 
-  pthread_t tid2; 
-  pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL); 
-  pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL); 
-  pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL); 
-  pthread_join(tid1, NULL); 
-  pthread_join(tid2, NULL); 
-  // deadlock in the threads; assertion should not be reachable
-  assert(0);
-} 
+#include <pthread.h>
+#include <stdlib.h>
+#include <assert.h>
+
+pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void* lock_never_unlock_002_tsk_001(void* pram) { 
+  pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);  
+  return NULL; 
+} 
+
+void main() { 
+  pthread_t tid1; 
+  pthread_t tid2; 
+  pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL); 
+  pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL); 
+  pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL); 
+  pthread_join(tid1, NULL); 
+  pthread_join(tid2, NULL); 
+  // deadlock in the threads; assertion should not be reachable
+  assert(0);
+} 
diff --git a/regression/cbmc-concurrency/deadlock2/main.c b/regression/cbmc-concurrency/deadlock2/main.c
index c2ebc9b9a01..d8000f2027d 100644
--- a/regression/cbmc-concurrency/deadlock2/main.c
+++ b/regression/cbmc-concurrency/deadlock2/main.c
@@ -1,23 +1,23 @@
-#include <pthread.h>
-#include <stdlib.h>
-#include <assert.h>
-
-pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
-
-void* lock_never_unlock_002_tsk_001(void* pram) { 
-  pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);  
-  pthread_mutex_unlock(&lock_never_unlock_002_glb_mutex);  
-  return NULL; 
-} 
-
-void main() { 
-  pthread_t tid1; 
-  pthread_t tid2; 
-  pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL); 
-  pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL); 
-  pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL); 
-  pthread_join(tid1, NULL); 
-  pthread_join(tid2, NULL); 
-  // no deadlock in the threads; assertion should be reached
-  assert(0);
-} 
+#include <pthread.h>
+#include <stdlib.h>
+#include <assert.h>
+
+pthread_mutex_t lock_never_unlock_002_glb_mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void* lock_never_unlock_002_tsk_001(void* pram) { 
+  pthread_mutex_lock(&lock_never_unlock_002_glb_mutex);  
+  pthread_mutex_unlock(&lock_never_unlock_002_glb_mutex);  
+  return NULL; 
+} 
+
+void main() { 
+  pthread_t tid1; 
+  pthread_t tid2; 
+  pthread_mutex_init(&lock_never_unlock_002_glb_mutex, NULL); 
+  pthread_create(&tid1, NULL, lock_never_unlock_002_tsk_001, NULL); 
+  pthread_create(&tid2, NULL, lock_never_unlock_002_tsk_001, NULL); 
+  pthread_join(tid1, NULL); 
+  pthread_join(tid2, NULL); 
+  // no deadlock in the threads; assertion should be reached
+  assert(0);
+} 
diff --git a/regression/cbmc-concurrency/norace_array1/main.c b/regression/cbmc-concurrency/norace_array1/main.c
index debc6871438..721065d6182 100644
--- a/regression/cbmc-concurrency/norace_array1/main.c
+++ b/regression/cbmc-concurrency/norace_array1/main.c
@@ -1,26 +1,26 @@
-#include <pthread.h>
-#include <assert.h>
-
-int s[2];
-
-void* thread_0(void* arg)
-{
-  s[0] = 2;
-  assert(s[0] == 2);
-  return NULL;
-}
-
-void* thread_1(void* arg)
-{
-  s[1] = 1;
-  assert(s[1] == 1);
-  return NULL;
-}
-
-int main(void)
-{
-  pthread_t thread0, thread1;
-  pthread_create(&thread0, NULL, thread_0, 0);
-  pthread_create(&thread1, NULL, thread_1, 0);
-  return 0;
-}
+#include <pthread.h>
+#include <assert.h>
+
+int s[2];
+
+void* thread_0(void* arg)
+{
+  s[0] = 2;
+  assert(s[0] == 2);
+  return NULL;
+}
+
+void* thread_1(void* arg)
+{
+  s[1] = 1;
+  assert(s[1] == 1);
+  return NULL;
+}
+
+int main(void)
+{
+  pthread_t thread0, thread1;
+  pthread_create(&thread0, NULL, thread_0, 0);
+  pthread_create(&thread1, NULL, thread_1, 0);
+  return 0;
+}
diff --git a/regression/cbmc-concurrency/norace_scalar1/main.c b/regression/cbmc-concurrency/norace_scalar1/main.c
index 8c39510fd73..eb5baf7fd6a 100644
--- a/regression/cbmc-concurrency/norace_scalar1/main.c
+++ b/regression/cbmc-concurrency/norace_scalar1/main.c
@@ -1,26 +1,26 @@
-#include <pthread.h>
-#include <assert.h>
-
-int f0, f1;
-
-void* thread_0(void* arg)
-{
-  f0 = 2;
-  assert(f0 == 2);
-  return NULL;
-}
-
-void* thread_1(void* arg)
-{
-  f1 = 1;
-  assert(f1 == 1);
-  return NULL;
-}
-
-int main(void)
-{
-  pthread_t thread0, thread1;
-  pthread_create(&thread0, NULL, thread_0, 0);
-  pthread_create(&thread1, NULL, thread_1, 0);
-  return 0;
-}
+#include <pthread.h>
+#include <assert.h>
+
+int f0, f1;
+
+void* thread_0(void* arg)
+{
+  f0 = 2;
+  assert(f0 == 2);
+  return NULL;
+}
+
+void* thread_1(void* arg)
+{
+  f1 = 1;
+  assert(f1 == 1);
+  return NULL;
+}
+
+int main(void)
+{
+  pthread_t thread0, thread1;
+  pthread_create(&thread0, NULL, thread_0, 0);
+  pthread_create(&thread1, NULL, thread_1, 0);
+  return 0;
+}
diff --git a/regression/cbmc-concurrency/norace_struct1/main.c b/regression/cbmc-concurrency/norace_struct1/main.c
index 1fca06df093..31dd7e324e3 100644
--- a/regression/cbmc-concurrency/norace_struct1/main.c
+++ b/regression/cbmc-concurrency/norace_struct1/main.c
@@ -1,26 +1,26 @@
-#include <pthread.h>
-#include <assert.h>
-
-struct { int f0; int f1; } s;
-
-void* thread_0(void* arg)
-{
-  s.f0 = 2;
-  assert(s.f0 == 2);
-  return NULL;
-}
-
-void* thread_1(void* arg)
-{
-  s.f1 = 1;
-  assert(s.f1 == 1);
-  return NULL;
-}
-
-int main(void)
-{
-  pthread_t thread0, thread1;
-  pthread_create(&thread0, NULL, thread_0, 0);
-  pthread_create(&thread1, NULL, thread_1, 0);
-  return 0;
-}
+#include <pthread.h>
+#include <assert.h>
+
+struct { int f0; int f1; } s;
+
+void* thread_0(void* arg)
+{
+  s.f0 = 2;
+  assert(s.f0 == 2);
+  return NULL;
+}
+
+void* thread_1(void* arg)
+{
+  s.f1 = 1;
+  assert(s.f1 == 1);
+  return NULL;
+}
+
+int main(void)
+{
+  pthread_t thread0, thread1;
+  pthread_create(&thread0, NULL, thread_0, 0);
+  pthread_create(&thread1, NULL, thread_1, 0);
+  return 0;
+}
diff --git a/regression/cbmc-concurrency/struct_and_array1/main.c b/regression/cbmc-concurrency/struct_and_array1/main.c
index cc3dd606089..42164904232 100644
--- a/regression/cbmc-concurrency/struct_and_array1/main.c
+++ b/regression/cbmc-concurrency/struct_and_array1/main.c
@@ -1,40 +1,40 @@
-#include <pthread.h>
-
-typedef struct st_t
-{
-  unsigned char x;
-  unsigned char y;
-} ST;
-
-ST st;
-
-char my_array[10];
-
-_Bool done1, done2;
-
-void *foo1(void *arg1)
-{
-  st.x = 1;
-  my_array[1]=1;
-  done1 = 1;
-}
-
-void *foo2(void *arg2)
-{
-  st.y = 1;
-  my_array[2]=2;
-  done2 = 1;
-}
-
-int main()
-{
-  pthread_t t;
-  pthread_create(&t,NULL,foo1,NULL);
-  pthread_create(&t,NULL,foo2,NULL);
-  
-  if(done1 && done2)
-  {
-    assert(st.x==st.y);
-    assert(my_array[1]==my_array[2]);
-  }
-}
+#include <pthread.h>
+
+typedef struct st_t
+{
+  unsigned char x;
+  unsigned char y;
+} ST;
+
+ST st;
+
+char my_array[10];
+
+_Bool done1, done2;
+
+void *foo1(void *arg1)
+{
+  st.x = 1;
+  my_array[1]=1;
+  done1 = 1;
+}
+
+void *foo2(void *arg2)
+{
+  st.y = 1;
+  my_array[2]=2;
+  done2 = 1;
+}
+
+int main()
+{
+  pthread_t t;
+  pthread_create(&t,NULL,foo1,NULL);
+  pthread_create(&t,NULL,foo2,NULL);
+  
+  if(done1 && done2)
+  {
+    assert(st.x==st.y);
+    assert(my_array[1]==my_array[2]);
+  }
+}
diff --git a/regression/cbmc-from-CVS/Struct_Pointer2/main.c b/regression/cbmc-from-CVS/Struct_Pointer2/main.c
index b50cfcd0f97..bf8ab0817c2 100644
--- a/regression/cbmc-from-CVS/Struct_Pointer2/main.c
+++ b/regression/cbmc-from-CVS/Struct_Pointer2/main.c
@@ -1,27 +1,27 @@
-#include <stdlib.h>
-#include <assert.h>
-
-struct mylist
-{
-  int  data;
-  struct mylist *next;
-};
-
-int main()
-{
-  struct mylist *p;
-
-  // Allocations:
-  p=malloc( sizeof(struct mylist ) );  
-  p->data=1;
-  p->next=malloc( sizeof(struct mylist ) );  
-  p->next->data=2;
-  p->next->next=malloc( sizeof(struct mylist ) );    
-  p->next->next->data=3;
-  p->next->next->next=malloc( sizeof(struct mylist ) );    
-  p->next->next->next->data=4;
-  
-  assert(p->next->next->data==3);
-
-  return 0;
-}
+#include <stdlib.h>
+#include <assert.h>
+
+struct mylist
+{
+  int  data;
+  struct mylist *next;
+};
+
+int main()
+{
+  struct mylist *p;
+
+  // Allocations:
+  p=malloc( sizeof(struct mylist ) );  
+  p->data=1;
+  p->next=malloc( sizeof(struct mylist ) );  
+  p->next->data=2;
+  p->next->next=malloc( sizeof(struct mylist ) );    
+  p->next->next->data=3;
+  p->next->next->next=malloc( sizeof(struct mylist ) );    
+  p->next->next->next->data=4;
+  
+  assert(p->next->next->data==3);
+
+  return 0;
+}
diff --git a/regression/cbmc-from-CVS/Unbounded_Array5/main.c b/regression/cbmc-from-CVS/Unbounded_Array5/main.c
index d797c3c2923..aebfa1e3a94 100644
--- a/regression/cbmc-from-CVS/Unbounded_Array5/main.c
+++ b/regression/cbmc-from-CVS/Unbounded_Array5/main.c
@@ -1,20 +1,20 @@
-int mem[__CPROVER_constant_infinity_uint];
-
-int  main()
-{
-  int i, j, mem_j;
-  
-  mem[0] = 0;
-  mem[1] = 1;
-
-  mem[j] = 1;
-  mem_j = mem[j];
-  assert(mem_j == 1);
-
-  mem[i] = mem[mem_j];
-   
-  unsigned xxxi=mem[i];
-  unsigned xxx1=mem[1];
-
-  __CPROVER_assert(xxxi == xxx1, "Check infinite mem");
-}
+int mem[__CPROVER_constant_infinity_uint];
+
+int  main()
+{
+  int i, j, mem_j;
+  
+  mem[0] = 0;
+  mem[1] = 1;
+
+  mem[j] = 1;
+  mem_j = mem[j];
+  assert(mem_j == 1);
+
+  mem[i] = mem[mem_j];
+   
+  unsigned xxxi=mem[i];
+  unsigned xxx1=mem[1];
+
+  __CPROVER_assert(xxxi == xxx1, "Check infinite mem");
+}
diff --git a/regression/cbmc-from-CVS/return2/tcas_v23_523.c b/regression/cbmc-from-CVS/return2/tcas_v23_523.c
index 6670715a6d2..4504d9c4dd4 100644
--- a/regression/cbmc-from-CVS/return2/tcas_v23_523.c
+++ b/regression/cbmc-from-CVS/return2/tcas_v23_523.c
@@ -1,171 +1,171 @@
-
-/*  -*- Last-Edit:  Fri Jan 29 11:13:27 1993 by Tarak S. Goradia; -*- */
+
+/*  -*- Last-Edit:  Fri Jan 29 11:13:27 1993 by Tarak S. Goradia; -*- */
 /* $Log: tcas_v23_523.c,v $
 /* Revision 1.1  2006-04-04 08:38:22  kroening
 /* more
-/*
- * Revision 1.2  1993/03/12  19:29:50  foster
- * Correct logic bug which didn't allow output of 2 - hf
- * */
-
-#include <stdio.h>
-
-#define OLEV       600		/* in feets/minute */
-#define MAXALTDIFF 600		/* max altitude difference in feet */
-#define MINSEP     300          /* min separation in feet */
-#define NOZCROSS   100		/* in feet */
-				/* variables */
-
-typedef int bool;
-
-int Cur_Vertical_Sep;
-bool High_Confidence;
-bool Two_of_Three_Reports_Valid;
-
-int Own_Tracked_Alt;
-int Own_Tracked_Alt_Rate;
-int Other_Tracked_Alt;
-
-int Alt_Layer_Value;		/* 0, 1, 2, 3 */
-int Positive_RA_Alt_Thresh[4];
-
-int Up_Separation;
-int Down_Separation;
-
-				/* state variables */
-int Other_RAC;			/* NO_INTENT, DO_NOT_CLIMB, DO_NOT_DESCEND */
-#define NO_INTENT 0
-#define DO_NOT_CLIMB 1
-#define DO_NOT_DESCEND 2
-
-int Other_Capability;		/* TCAS_TA, OTHER */
-#define TCAS_TA 1
-#define OTHER 2
-
-int Climb_Inhibit;		/* true/false */
-
-#define UNRESOLVED 0
-#define UPWARD_RA 1
-#define DOWNWARD_RA 2
-
-int  ALIM();
-int  Inhibit_Biased_Climb();
-bool   Non_Crossing_Biased_Climb();
-bool   Non_Crossing_Biased_Descend();
-bool   Own_Below_Threat();
-bool   Own_Above_Threat();
-int  alt_sep_test();
-void initialize()
-{
-    Positive_RA_Alt_Thresh[0] = 400;
-    Positive_RA_Alt_Thresh[1] = 500;
-    Positive_RA_Alt_Thresh[2] = 640;
-    Positive_RA_Alt_Thresh[3] = 740;
-}
-
-int ALIM ()
-{
- return Positive_RA_Alt_Thresh[Alt_Layer_Value];
-}
-
-int Inhibit_Biased_Climb ()
-{
-    return (Climb_Inhibit ? Up_Separation + NOZCROSS : Up_Separation);
-}
-
-bool Non_Crossing_Biased_Climb()
-{
-    int upward_preferred;
-    int upward_crossing_situation;
-    bool result;
-
-    upward_preferred = Inhibit_Biased_Climb() > Down_Separation;
-    if (upward_preferred)
-    {
-	result = !(Own_Below_Threat()) || ((Own_Below_Threat()) && (!(Down_Separation >= ALIM())));
-    }
-    else
-    {	
-	result = Own_Above_Threat() && (Cur_Vertical_Sep >= MINSEP) && (Up_Separation >= ALIM());
-    }
-    return result;
-}
-
-bool Non_Crossing_Biased_Descend()
-{
-    int upward_preferred;
-    int upward_crossing_situation;
-    bool result;
-
-    upward_preferred = (Up_Separation + NOZCROSS) > Down_Separation;
-    if (upward_preferred)
-    {
-	result = Own_Below_Threat() && (Cur_Vertical_Sep >= MINSEP) && (Down_Separation >= ALIM());
-    }
-    else
-    {
-	result = !(Own_Above_Threat()) || ((Own_Above_Threat()) && (Up_Separation >= ALIM()));
-    }
-    return result;
-}
-
-bool Own_Below_Threat()
-{
-    return (Own_Tracked_Alt < Other_Tracked_Alt);
-}
-
-bool Own_Above_Threat()
-{
-    return (Other_Tracked_Alt < Own_Tracked_Alt);
-}
-
-int alt_sep_test()
-{
-    bool enabled, tcas_equipped, intent_not_known;
-    bool need_upward_RA, need_downward_RA;
-    int alt_sep;
-
-    enabled = High_Confidence && (Own_Tracked_Alt_Rate <= OLEV) && (Cur_Vertical_Sep > MAXALTDIFF);
-    tcas_equipped = Other_Capability == TCAS_TA;
-    intent_not_known = Two_of_Three_Reports_Valid && Other_RAC == NO_INTENT;
-    
-    alt_sep = UNRESOLVED;
-    
-    if (enabled && ((tcas_equipped && intent_not_known) || !tcas_equipped))
-    {
-	need_upward_RA = Non_Crossing_Biased_Climb() && Own_Below_Threat();
-	need_downward_RA = Non_Crossing_Biased_Descend() && Own_Above_Threat();
-	if (need_upward_RA && need_downward_RA)
-        /* unreachable: requires Own_Below_Threat and Own_Above_Threat
-           to both be true - that requires Own_Tracked_Alt < Other_Tracked_Alt
-           and Other_Tracked_Alt < Own_Tracked_Alt, which isn't possible */
-	    alt_sep = UNRESOLVED;
-	else if (need_upward_RA)
-	    alt_sep = UPWARD_RA;
-	else if (need_downward_RA)
-	    alt_sep = DOWNWARD_RA;
-	else
-	    alt_sep = UNRESOLVED;
-    }
-    
-    return alt_sep;
-}
-
-main(int argc, char*argv[])
-{
-
-  initialize();
-  Cur_Vertical_Sep =  860; 
-  High_Confidence = 1; 
-  Two_of_Three_Reports_Valid = 1; 
-  Own_Tracked_Alt =  618; 
-  Own_Tracked_Alt_Rate =  329; 
-  Other_Tracked_Alt =  574; 
-  Alt_Layer_Value =  4; 
-  Up_Separation =  893; 
-  Down_Separation =  914; 
-  Other_RAC =  0; 
-  Other_Capability =  2; 
-  Climb_Inhibit =  0; 
-  assert(alt_sep_test()==0);
-}
+/*
+ * Revision 1.2  1993/03/12  19:29:50  foster
+ * Correct logic bug which didn't allow output of 2 - hf
+ * */
+
+#include <stdio.h>
+
+#define OLEV       600		/* in feets/minute */
+#define MAXALTDIFF 600		/* max altitude difference in feet */
+#define MINSEP     300          /* min separation in feet */
+#define NOZCROSS   100		/* in feet */
+				/* variables */
+
+typedef int bool;
+
+int Cur_Vertical_Sep;
+bool High_Confidence;
+bool Two_of_Three_Reports_Valid;
+
+int Own_Tracked_Alt;
+int Own_Tracked_Alt_Rate;
+int Other_Tracked_Alt;
+
+int Alt_Layer_Value;		/* 0, 1, 2, 3 */
+int Positive_RA_Alt_Thresh[4];
+
+int Up_Separation;
+int Down_Separation;
+
+				/* state variables */
+int Other_RAC;			/* NO_INTENT, DO_NOT_CLIMB, DO_NOT_DESCEND */
+#define NO_INTENT 0
+#define DO_NOT_CLIMB 1
+#define DO_NOT_DESCEND 2
+
+int Other_Capability;		/* TCAS_TA, OTHER */
+#define TCAS_TA 1
+#define OTHER 2
+
+int Climb_Inhibit;		/* true/false */
+
+#define UNRESOLVED 0
+#define UPWARD_RA 1
+#define DOWNWARD_RA 2
+
+int  ALIM();
+int  Inhibit_Biased_Climb();
+bool   Non_Crossing_Biased_Climb();
+bool   Non_Crossing_Biased_Descend();
+bool   Own_Below_Threat();
+bool   Own_Above_Threat();
+int  alt_sep_test();
+void initialize()
+{
+    Positive_RA_Alt_Thresh[0] = 400;
+    Positive_RA_Alt_Thresh[1] = 500;
+    Positive_RA_Alt_Thresh[2] = 640;
+    Positive_RA_Alt_Thresh[3] = 740;
+}
+
+int ALIM ()
+{
+ return Positive_RA_Alt_Thresh[Alt_Layer_Value];
+}
+
+int Inhibit_Biased_Climb ()
+{
+    return (Climb_Inhibit ? Up_Separation + NOZCROSS : Up_Separation);
+}
+
+bool Non_Crossing_Biased_Climb()
+{
+    int upward_preferred;
+    int upward_crossing_situation;
+    bool result;
+
+    upward_preferred = Inhibit_Biased_Climb() > Down_Separation;
+    if (upward_preferred)
+    {
+	result = !(Own_Below_Threat()) || ((Own_Below_Threat()) && (!(Down_Separation >= ALIM())));
+    }
+    else
+    {	
+	result = Own_Above_Threat() && (Cur_Vertical_Sep >= MINSEP) && (Up_Separation >= ALIM());
+    }
+    return result;
+}
+
+bool Non_Crossing_Biased_Descend()
+{
+    int upward_preferred;
+    int upward_crossing_situation;
+    bool result;
+
+    upward_preferred = (Up_Separation + NOZCROSS) > Down_Separation;
+    if (upward_preferred)
+    {
+	result = Own_Below_Threat() && (Cur_Vertical_Sep >= MINSEP) && (Down_Separation >= ALIM());
+    }
+    else
+    {
+	result = !(Own_Above_Threat()) || ((Own_Above_Threat()) && (Up_Separation >= ALIM()));
+    }
+    return result;
+}
+
+bool Own_Below_Threat()
+{
+    return (Own_Tracked_Alt < Other_Tracked_Alt);
+}
+
+bool Own_Above_Threat()
+{
+    return (Other_Tracked_Alt < Own_Tracked_Alt);
+}
+
+int alt_sep_test()
+{
+    bool enabled, tcas_equipped, intent_not_known;
+    bool need_upward_RA, need_downward_RA;
+    int alt_sep;
+
+    enabled = High_Confidence && (Own_Tracked_Alt_Rate <= OLEV) && (Cur_Vertical_Sep > MAXALTDIFF);
+    tcas_equipped = Other_Capability == TCAS_TA;
+    intent_not_known = Two_of_Three_Reports_Valid && Other_RAC == NO_INTENT;
+    
+    alt_sep = UNRESOLVED;
+    
+    if (enabled && ((tcas_equipped && intent_not_known) || !tcas_equipped))
+    {
+	need_upward_RA = Non_Crossing_Biased_Climb() && Own_Below_Threat();
+	need_downward_RA = Non_Crossing_Biased_Descend() && Own_Above_Threat();
+	if (need_upward_RA && need_downward_RA)
+        /* unreachable: requires Own_Below_Threat and Own_Above_Threat
+           to both be true - that requires Own_Tracked_Alt < Other_Tracked_Alt
+           and Other_Tracked_Alt < Own_Tracked_Alt, which isn't possible */
+	    alt_sep = UNRESOLVED;
+	else if (need_upward_RA)
+	    alt_sep = UPWARD_RA;
+	else if (need_downward_RA)
+	    alt_sep = DOWNWARD_RA;
+	else
+	    alt_sep = UNRESOLVED;
+    }
+    
+    return alt_sep;
+}
+
+main(int argc, char*argv[])
+{
+
+  initialize();
+  Cur_Vertical_Sep =  860; 
+  High_Confidence = 1; 
+  Two_of_Three_Reports_Valid = 1; 
+  Own_Tracked_Alt =  618; 
+  Own_Tracked_Alt_Rate =  329; 
+  Other_Tracked_Alt =  574; 
+  Alt_Layer_Value =  4; 
+  Up_Separation =  893; 
+  Down_Separation =  914; 
+  Other_RAC =  0; 
+  Other_Capability =  2; 
+  Climb_Inhibit =  0; 
+  assert(alt_sep_test()==0);
+}
diff --git a/regression/cbmc-with-incr/Float-div1/main.c b/regression/cbmc-with-incr/Float-div1/main.c
index dee31965dac..63f8512a7c2 100644
--- a/regression/cbmc-with-incr/Float-div1/main.c
+++ b/regression/cbmc-with-incr/Float-div1/main.c
@@ -1,50 +1,50 @@
-#include <assert.h>
-#include <math.h>
-
-#ifdef __GNUC__
-void inductiveStepHunt (float startState)
-{
-  float target = 0x1.fffffep-3f;
-
-  __CPROVER_assume((0 < startState) && (fpclassify(startState) == FP_NORMAL) && (0x1p-126f <= startState));
-
-  float secondPoint = (target / startState);
-
-  float nextState = (startState + secondPoint) / 2;
-
-  float oneAfter = (target / nextState);
-
-  assert(oneAfter > 0);
-}
-
-void simplifiedInductiveStepHunt (float nextState)
-{
-  float target = 0x1.fffffep-3f;
-
-  // Implies nextState == 0x1p+124f;
-  __CPROVER_assume((0x1.fffffep+123f < nextState) && (nextState < 0x1.000002p+124f));
-  
-  float oneAfter = (target / nextState);
-
-  // Is true and correctly proven by constant evaluation
-  // Note that this is the smallest normal number
-  assert(0x1.fffffep-3f / 0x1p+124f == 0x1p-126f);
-
-  assert(oneAfter > 0);
-}
-#endif
-
-int main (void)
-{
-  #ifdef __GNUC__
-  //  inductiveStepHunt(0x1p+125f);
-  //  simplifiedInductiveStepHunt(0x1p+124f);
-
-  float f, g;
-
-  inductiveStepHunt(f);
-  simplifiedInductiveStepHunt(g);
-  #endif
-
-  return 0;
-}
+#include <assert.h>
+#include <math.h>
+
+#ifdef __GNUC__
+void inductiveStepHunt (float startState)
+{
+  float target = 0x1.fffffep-3f;
+
+  __CPROVER_assume((0 < startState) && (fpclassify(startState) == FP_NORMAL) && (0x1p-126f <= startState));
+
+  float secondPoint = (target / startState);
+
+  float nextState = (startState + secondPoint) / 2;
+
+  float oneAfter = (target / nextState);
+
+  assert(oneAfter > 0);
+}
+
+void simplifiedInductiveStepHunt (float nextState)
+{
+  float target = 0x1.fffffep-3f;
+
+  // Implies nextState == 0x1p+124f;
+  __CPROVER_assume((0x1.fffffep+123f < nextState) && (nextState < 0x1.000002p+124f));
+  
+  float oneAfter = (target / nextState);
+
+  // Is true and correctly proven by constant evaluation
+  // Note that this is the smallest normal number
+  assert(0x1.fffffep-3f / 0x1p+124f == 0x1p-126f);
+
+  assert(oneAfter > 0);
+}
+#endif
+
+int main (void)
+{
+  #ifdef __GNUC__
+  //  inductiveStepHunt(0x1p+125f);
+  //  simplifiedInductiveStepHunt(0x1p+124f);
+
+  float f, g;
+
+  inductiveStepHunt(f);
+  simplifiedInductiveStepHunt(g);
+  #endif
+
+  return 0;
+}
diff --git a/regression/cbmc-with-incr/Float-to-double2/main.c b/regression/cbmc-with-incr/Float-to-double2/main.c
index 43ab0927eab..2db129fd08f 100644
--- a/regression/cbmc-with-incr/Float-to-double2/main.c
+++ b/regression/cbmc-with-incr/Float-to-double2/main.c
@@ -1,12 +1,12 @@
-#include <assert.h>
-
-int main(void)
-{
-  float f   = -0x1.0p-127f;
-  double d  = -0x1.0p-127;
-  double fp = (double)f;
-
-  assert(d == fp);
-
-  return 0;
-}
+#include <assert.h>
+
+int main(void)
+{
+  float f   = -0x1.0p-127f;
+  double d  = -0x1.0p-127;
+  double fp = (double)f;
+
+  assert(d == fp);
+
+  return 0;
+}
diff --git a/regression/cbmc-with-incr/Float19/main.c b/regression/cbmc-with-incr/Float19/main.c
index bc09c89924d..56b5548c602 100644
--- a/regression/cbmc-with-incr/Float19/main.c
+++ b/regression/cbmc-with-incr/Float19/main.c
@@ -1,24 +1,24 @@
-#include <assert.h>
-#include <math.h>
-
-#ifdef __GNUC__
-
-void f00 (float f)
-{
-  if (f > 0x1.FFFFFEp+127) {
-    assert(isinf(f));
-  }
-}
-
-#endif
-
-int main (void)
-{
-  #ifdef __GNUC__
-  float f;
-
-  f00(f);
-  #endif
-
-  return 0;
-}
+#include <assert.h>
+#include <math.h>
+
+#ifdef __GNUC__
+
+void f00 (float f)
+{
+  if (f > 0x1.FFFFFEp+127) {
+    assert(isinf(f));
+  }
+}
+
+#endif
+
+int main (void)
+{
+  #ifdef __GNUC__
+  float f;
+
+  f00(f);
+  #endif
+
+  return 0;
+}
diff --git a/regression/cbmc-with-incr/Float20/main.c b/regression/cbmc-with-incr/Float20/main.c
index dfacc8bac6d..b730f0d4f18 100644
--- a/regression/cbmc-with-incr/Float20/main.c
+++ b/regression/cbmc-with-incr/Float20/main.c
@@ -1,56 +1,56 @@
-/*
-** 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.
-*/
-#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;
-}
-
+/*
+** 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.
+*/
+#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-with-incr/Float21/main.c b/regression/cbmc-with-incr/Float21/main.c
index e01c31684a7..883e066cdfc 100644
--- a/regression/cbmc-with-incr/Float21/main.c
+++ b/regression/cbmc-with-incr/Float21/main.c
@@ -1,66 +1,66 @@
-/*
-** subnormal-boundary.c
-**
-** Martin Brain
-** martin.brain@cs.ox.ac.uk
-** 25/07/12
-**
-** Regression tests for casting and classification around the subnormal boundary.
-**
-*/
-
-#include <assert.h>
-#include <math.h>
-
-float nondet_float(void);
-
-int main (void)
-{
-  #ifdef __GNUC__
-
-  float smallestNormalFloat = 0x1.0p-126f;
-  float largestSubnormalFloat = 0x1.fffffcp-127f;
-  
-  double v = 0x1.FFFFFFp-127;
-
-  float f;
-
-
-  // Check the encodings are correct
-  assert(fpclassify(largestSubnormalFloat) == FP_SUBNORMAL);
-
-  f = nondet_float();
-  __CPROVER_assume(fpclassify(f) == FP_SUBNORMAL);
-  assert(f <= largestSubnormalFloat);
-
-
-  assert(fpclassify(smallestNormalFloat) == FP_NORMAL);
-
-  f = nondet_float();
-  __CPROVER_assume(fpclassify(f) == FP_NORMAL);
-  assert(smallestNormalFloat <= fabs(f));
-
-  assert(largestSubnormalFloat < smallestNormalFloat);
-
-
-  // Check the ordering as doubles
-  assert(((double)largestSubnormalFloat) < ((double)smallestNormalFloat));
-  assert(((double)largestSubnormalFloat) < v);
-  assert(v < ((double)smallestNormalFloat));
-
-
-  // Check coercion to float
-  assert((float)((double)largestSubnormalFloat) == largestSubnormalFloat);
-  assert((float)((double)smallestNormalFloat) == smallestNormalFloat);
-
-  assert(((double)smallestNormalFloat) - v <= v - ((double)largestSubnormalFloat));
-  assert(((float)v) == smallestNormalFloat);
-
-  f = nondet_float();
-  __CPROVER_assume(fpclassify(f) == FP_SUBNORMAL);
-  assert( ((float)((double)f)) == f );
-  
-  #endif
-
-  return 0;
-}
+/*
+** subnormal-boundary.c
+**
+** Martin Brain
+** martin.brain@cs.ox.ac.uk
+** 25/07/12
+**
+** Regression tests for casting and classification around the subnormal boundary.
+**
+*/
+
+#include <assert.h>
+#include <math.h>
+
+float nondet_float(void);
+
+int main (void)
+{
+  #ifdef __GNUC__
+
+  float smallestNormalFloat = 0x1.0p-126f;
+  float largestSubnormalFloat = 0x1.fffffcp-127f;
+  
+  double v = 0x1.FFFFFFp-127;
+
+  float f;
+
+
+  // Check the encodings are correct
+  assert(fpclassify(largestSubnormalFloat) == FP_SUBNORMAL);
+
+  f = nondet_float();
+  __CPROVER_assume(fpclassify(f) == FP_SUBNORMAL);
+  assert(f <= largestSubnormalFloat);
+
+
+  assert(fpclassify(smallestNormalFloat) == FP_NORMAL);
+
+  f = nondet_float();
+  __CPROVER_assume(fpclassify(f) == FP_NORMAL);
+  assert(smallestNormalFloat <= fabs(f));
+
+  assert(largestSubnormalFloat < smallestNormalFloat);
+
+
+  // Check the ordering as doubles
+  assert(((double)largestSubnormalFloat) < ((double)smallestNormalFloat));
+  assert(((double)largestSubnormalFloat) < v);
+  assert(v < ((double)smallestNormalFloat));
+
+
+  // Check coercion to float
+  assert((float)((double)largestSubnormalFloat) == largestSubnormalFloat);
+  assert((float)((double)smallestNormalFloat) == smallestNormalFloat);
+
+  assert(((double)smallestNormalFloat) - v <= v - ((double)largestSubnormalFloat));
+  assert(((float)v) == smallestNormalFloat);
+
+  f = nondet_float();
+  __CPROVER_assume(fpclassify(f) == FP_SUBNORMAL);
+  assert( ((float)((double)f)) == f );
+  
+  #endif
+
+  return 0;
+}
diff --git a/regression/cbmc-with-incr/Recursion4/main.c b/regression/cbmc-with-incr/Recursion4/main.c
index 00198d60574..c2cc4c13ae1 100644
--- a/regression/cbmc-with-incr/Recursion4/main.c
+++ b/regression/cbmc-with-incr/Recursion4/main.c
@@ -1,17 +1,17 @@
-int factorial2(int i)
-{
-  if(i==0) return 1;
-
-  // tmp_result gets renamed during recursion!
-  int tmp_result;
-  tmp_result=factorial2(0);
-  return tmp_result;
-}
-
-int main()
-{
-  int result_factorial;
-  result_factorial=factorial2(1);
-  assert(result_factorial==1);
-  return 0;
-}
+int factorial2(int i)
+{
+  if(i==0) return 1;
+
+  // tmp_result gets renamed during recursion!
+  int tmp_result;
+  tmp_result=factorial2(0);
+  return tmp_result;
+}
+
+int main()
+{
+  int result_factorial;
+  result_factorial=factorial2(1);
+  assert(result_factorial==1);
+  return 0;
+}
diff --git a/regression/cpp-from-CVS/Array1/main.cpp b/regression/cpp-from-CVS/Array1/main.cpp
index 8c77e5c8f89..ba02b972c16 100644
--- a/regression/cpp-from-CVS/Array1/main.cpp
+++ b/regression/cpp-from-CVS/Array1/main.cpp
@@ -1,11 +1,11 @@
-int y[5][4][3][2];
-
-int main()
-{
-  for(int i=0; i<5; i++)
-    for(int j=0; j<4; j++)
-      for(int k=0; k<3; k++)
-        for(int l=0; l<2; l++)
-          y[i][j][k][l]=2;
-}
-
+int y[5][4][3][2];
+
+int main()
+{
+  for(int i=0; i<5; i++)
+    for(int j=0; j<4; j++)
+      for(int k=0; k<3; k++)
+        for(int l=0; l<2; l++)
+          y[i][j][k][l]=2;
+}
+
diff --git a/regression/cpp-from-CVS/Array2/main.cpp b/regression/cpp-from-CVS/Array2/main.cpp
index 5359e4e8149..0e3e35b8ad3 100644
--- a/regression/cpp-from-CVS/Array2/main.cpp
+++ b/regression/cpp-from-CVS/Array2/main.cpp
@@ -1,11 +1,11 @@
-int y[2][3][4][5];
-
-int main()
-{
-  for(int i=0; i<5; i++)
-    for(int j=0; j<4; j++)
-      for(int k=0; k<3; k++)
-        for(int l=0; l<2; l++)
-          y[i][j][k][l]=2; // out-of-bounds
-}
-
+int y[2][3][4][5];
+
+int main()
+{
+  for(int i=0; i<5; i++)
+    for(int j=0; j<4; j++)
+      for(int k=0; k<3; k++)
+        for(int l=0; l<2; l++)
+          y[i][j][k][l]=2; // out-of-bounds
+}
+
diff --git a/regression/cpp/Decltype2/main.cpp b/regression/cpp/Decltype2/main.cpp
index f315130f21a..ba26a736059 100644
--- a/regression/cpp/Decltype2/main.cpp
+++ b/regression/cpp/Decltype2/main.cpp
@@ -1,14 +1,14 @@
-// C++11
-// decltype is a C++11 feature to get the "declared type" of an expression.
-// It is similar to 'typeof' but handles reference types "properly".
-
-class base {};
-class derived : public base {};
-
-derived d;
-
-decltype(static_cast<derived *>(&d)) z;
-
-int main()
-{
-}
+// C++11
+// decltype is a C++11 feature to get the "declared type" of an expression.
+// It is similar to 'typeof' but handles reference types "properly".
+
+class base {};
+class derived : public base {};
+
+derived d;
+
+decltype(static_cast<derived *>(&d)) z;
+
+int main()
+{
+}
diff --git a/regression/cpp/Decltype3/main.cpp b/regression/cpp/Decltype3/main.cpp
index 0ded9d5c44f..e0a95f38b00 100644
--- a/regression/cpp/Decltype3/main.cpp
+++ b/regression/cpp/Decltype3/main.cpp
@@ -1,18 +1,18 @@
-// C++11
-// decltype is a C++11 feature to get the "declared type" of an expression.
-// It is similar to 'typeof' but handles reference types "properly".
-
-template <class A, class B>
-struct whatever {
-	int f00 (const B b) {
-		typedef	decltype(static_cast<A>(b)) T;
-		T z;
-		return 1;
-	}
-};
-
-whatever<int,float> thing;
-
-int main()
-{
-}
+// C++11
+// decltype is a C++11 feature to get the "declared type" of an expression.
+// It is similar to 'typeof' but handles reference types "properly".
+
+template <class A, class B>
+struct whatever {
+	int f00 (const B b) {
+		typedef	decltype(static_cast<A>(b)) T;
+		T z;
+		return 1;
+	}
+};
+
+whatever<int,float> thing;
+
+int main()
+{
+}

From c87c768e183d8f93567103fa5666a24475ea17b9 Mon Sep 17 00:00:00 2001
From: Daniel Neville <daniel.neville@cs.ox.ac.uk>
Date: Thu, 29 Sep 2016 14:08:37 +0100
Subject: [PATCH 3/9] Taint analysis for Symex.

---
 regression/symex-taint-analysis/Makefile      |  14 ++
 .../array-all-taint-inline/array_all_taint.c  |  15 ++
 .../array-all-taint-inline/taint.json         |   6 +
 .../array-all-taint-json/array_all_taint.c    |  15 ++
 .../array-all-taint-json/main.c               |  15 ++
 .../array-all-taint-json/taint.json           |   6 +
 .../array-all-taint-json/test.desc            |   8 +
 .../array-taint-inline/array_taint.c          |  17 ++
 .../array-taint-inline/main.c                 |  17 ++
 .../array-taint-inline/test.desc              |   8 +
 .../array-taint-json/array_taint.c            |  15 ++
 .../array-taint-json/main.c                   |  15 ++
 .../array-taint-json/taint.json               |   7 +
 .../array-taint-json/test.desc                |   8 +
 .../array-untaint-inline/array_untaint.c      |  17 ++
 .../array-untaint-inline/main.c               |  17 ++
 .../array-untaint-inline/test.desc            |   8 +
 .../func-taint-inline/func_taint.c            |  19 ++
 .../func-taint-inline/main.c                  |  18 ++
 .../func-taint-inline/test.desc               |   8 +
 .../loop-taint-inline/loop_taint.c            |  23 +++
 .../loop-taint-inline/main.c                  |  27 +++
 .../loop-taint-inline/test.desc               |   8 +
 .../loop-untaint-inline/loop_untaint.c        |  23 +++
 .../loop-untaint-inline/main.c                |  24 +++
 .../loop-untaint-inline/test.desc             |   8 +
 .../recursive-taint-inline/main.c             |  22 +++
 .../recursive-taint-inline/test.desc          |   8 +
 .../recursive-untaint-inline/main.c           |  26 +++
 .../recursive-untaint-inline/test.desc        |   8 +
 .../simple-taint-inline/main.c                |  19 ++
 .../simple-taint-inline/simple_taint.c        |  19 ++
 .../simple-taint-inline/test.desc             |   8 +
 .../simple-taint-json/main.c                  |  17 ++
 .../simple-taint-json/simple_taint.c          |  17 ++
 .../simple-taint-json/taint.json              |   6 +
 .../simple-taint-json/test.desc               |   8 +
 .../simple-untaint-inline/main.c              |  20 ++
 .../simple-untaint-inline/simple_untaint.c    |  20 ++
 .../simple-untaint-inline/test.desc           |   8 +
 .../simple-untaint-json/main.c                |  18 ++
 .../simple-untaint-json/simple_untaint.c      |  18 ++
 .../simple-untaint-json/taint.json            |   6 +
 .../simple-untaint-json/test.desc             |   8 +
 .../struct-copy-taint-inline/main.c           |  24 +++
 .../struct-copy-taint-inline/test.desc        |   8 +
 .../struct-taint-inline/main.c                |  19 ++
 .../struct-taint-inline/struct_taint.c        |  19 ++
 .../struct-taint-inline/test.desc             |   8 +
 .../struct-untaint-inline/main.c              |  19 ++
 .../struct-untaint-inline/struct_untaint.c    |  19 ++
 .../struct-untaint-inline/test.desc           |   8 +
 .../symex-taint-analysis/test2/taint.json     |   6 +
 .../symex-taint-analysis/test2/taint_test.c   |  14 ++
 src/ansi-c/ansi_c_internal_additions.cpp      |   4 +
 src/ansi-c/c_typecheck_expr.cpp               |  51 +++++
 src/ansi-c/expr2c.cpp                         |   9 +
 src/ansi-c/library/cprover.h                  |   5 +
 src/path-symex/Makefile                       |   7 +-
 src/path-symex/path_symex.cpp                 | 177 +++++++++++++++++-
 src/path-symex/path_symex_class.h             |  12 +-
 src/path-symex/path_symex_state.cpp           |  55 +++++-
 src/path-symex/path_symex_state.h             |  27 ++-
 src/path-symex/path_symex_state_read.cpp      |  60 ++++++
 src/path-symex/path_symex_taint_analysis.cpp  |  96 ++++++++++
 src/path-symex/path_symex_taint_analysis.h    | 123 ++++++++++++
 src/path-symex/path_symex_taint_data.cpp      | 164 ++++++++++++++++
 src/path-symex/path_symex_taint_data.h        |  56 ++++++
 src/path-symex/path_symex_taint_parser.cpp    | 105 +++++++++++
 src/path-symex/path_symex_taint_parser.h      |  25 +++
 src/symex/Makefile                            |   1 +
 src/symex/path_search.cpp                     |  28 ++-
 src/symex/path_search.h                       |  14 ++
 src/symex/symex_parse_options.cpp             |  78 ++++++++
 src/symex/symex_parse_options.h               |   4 +
 src/util/irep_ids.txt                         |   3 +
 76 files changed, 1854 insertions(+), 16 deletions(-)
 create mode 100644 regression/symex-taint-analysis/Makefile
 create mode 100644 regression/symex-taint-analysis/array-all-taint-inline/array_all_taint.c
 create mode 100644 regression/symex-taint-analysis/array-all-taint-inline/taint.json
 create mode 100644 regression/symex-taint-analysis/array-all-taint-json/array_all_taint.c
 create mode 100644 regression/symex-taint-analysis/array-all-taint-json/main.c
 create mode 100644 regression/symex-taint-analysis/array-all-taint-json/taint.json
 create mode 100644 regression/symex-taint-analysis/array-all-taint-json/test.desc
 create mode 100644 regression/symex-taint-analysis/array-taint-inline/array_taint.c
 create mode 100644 regression/symex-taint-analysis/array-taint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/array-taint-inline/test.desc
 create mode 100644 regression/symex-taint-analysis/array-taint-json/array_taint.c
 create mode 100644 regression/symex-taint-analysis/array-taint-json/main.c
 create mode 100644 regression/symex-taint-analysis/array-taint-json/taint.json
 create mode 100644 regression/symex-taint-analysis/array-taint-json/test.desc
 create mode 100644 regression/symex-taint-analysis/array-untaint-inline/array_untaint.c
 create mode 100644 regression/symex-taint-analysis/array-untaint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/array-untaint-inline/test.desc
 create mode 100644 regression/symex-taint-analysis/func-taint-inline/func_taint.c
 create mode 100644 regression/symex-taint-analysis/func-taint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/func-taint-inline/test.desc
 create mode 100644 regression/symex-taint-analysis/loop-taint-inline/loop_taint.c
 create mode 100644 regression/symex-taint-analysis/loop-taint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/loop-taint-inline/test.desc
 create mode 100644 regression/symex-taint-analysis/loop-untaint-inline/loop_untaint.c
 create mode 100644 regression/symex-taint-analysis/loop-untaint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/loop-untaint-inline/test.desc
 create mode 100644 regression/symex-taint-analysis/recursive-taint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/recursive-taint-inline/test.desc
 create mode 100644 regression/symex-taint-analysis/recursive-untaint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/recursive-untaint-inline/test.desc
 create mode 100644 regression/symex-taint-analysis/simple-taint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/simple-taint-inline/simple_taint.c
 create mode 100644 regression/symex-taint-analysis/simple-taint-inline/test.desc
 create mode 100644 regression/symex-taint-analysis/simple-taint-json/main.c
 create mode 100644 regression/symex-taint-analysis/simple-taint-json/simple_taint.c
 create mode 100644 regression/symex-taint-analysis/simple-taint-json/taint.json
 create mode 100644 regression/symex-taint-analysis/simple-taint-json/test.desc
 create mode 100644 regression/symex-taint-analysis/simple-untaint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/simple-untaint-inline/simple_untaint.c
 create mode 100644 regression/symex-taint-analysis/simple-untaint-inline/test.desc
 create mode 100644 regression/symex-taint-analysis/simple-untaint-json/main.c
 create mode 100644 regression/symex-taint-analysis/simple-untaint-json/simple_untaint.c
 create mode 100644 regression/symex-taint-analysis/simple-untaint-json/taint.json
 create mode 100644 regression/symex-taint-analysis/simple-untaint-json/test.desc
 create mode 100644 regression/symex-taint-analysis/struct-copy-taint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/struct-copy-taint-inline/test.desc
 create mode 100644 regression/symex-taint-analysis/struct-taint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/struct-taint-inline/struct_taint.c
 create mode 100644 regression/symex-taint-analysis/struct-taint-inline/test.desc
 create mode 100644 regression/symex-taint-analysis/struct-untaint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/struct-untaint-inline/struct_untaint.c
 create mode 100644 regression/symex-taint-analysis/struct-untaint-inline/test.desc
 create mode 100644 regression/symex-taint-analysis/test2/taint.json
 create mode 100644 regression/symex-taint-analysis/test2/taint_test.c
 create mode 100644 src/path-symex/path_symex_taint_analysis.cpp
 create mode 100644 src/path-symex/path_symex_taint_analysis.h
 create mode 100644 src/path-symex/path_symex_taint_data.cpp
 create mode 100644 src/path-symex/path_symex_taint_data.h
 create mode 100644 src/path-symex/path_symex_taint_parser.cpp
 create mode 100644 src/path-symex/path_symex_taint_parser.h

diff --git a/regression/symex-taint-analysis/Makefile b/regression/symex-taint-analysis/Makefile
new file mode 100644
index 00000000000..d8a99eec731
--- /dev/null
+++ b/regression/symex-taint-analysis/Makefile
@@ -0,0 +1,14 @@
+default: tests.log
+
+test:
+	@../test.pl -c ../../../src/symex/symex
+
+tests.log: ../test.pl
+	@../test.pl -c ../../../src/symex/symex
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
diff --git a/regression/symex-taint-analysis/array-all-taint-inline/array_all_taint.c b/regression/symex-taint-analysis/array-all-taint-inline/array_all_taint.c
new file mode 100644
index 00000000000..dee45cb1a8c
--- /dev/null
+++ b/regression/symex-taint-analysis/array-all-taint-inline/array_all_taint.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	int y = x[0];
+
+	int c = ++y;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/array-all-taint-inline/taint.json b/regression/symex-taint-analysis/array-all-taint-inline/taint.json
new file mode 100644
index 00000000000..40c7105fba1
--- /dev/null
+++ b/regression/symex-taint-analysis/array-all-taint-inline/taint.json
@@ -0,0 +1,6 @@
+[
+{
+	"loc": 0,
+	"taint": "tainted"
+}
+]
\ No newline at end of file
diff --git a/regression/symex-taint-analysis/array-all-taint-json/array_all_taint.c b/regression/symex-taint-analysis/array-all-taint-json/array_all_taint.c
new file mode 100644
index 00000000000..dee45cb1a8c
--- /dev/null
+++ b/regression/symex-taint-analysis/array-all-taint-json/array_all_taint.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	int y = x[0];
+
+	int c = ++y;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/array-all-taint-json/main.c b/regression/symex-taint-analysis/array-all-taint-json/main.c
new file mode 100644
index 00000000000..dee45cb1a8c
--- /dev/null
+++ b/regression/symex-taint-analysis/array-all-taint-json/main.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	int y = x[0];
+
+	int c = ++y;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/array-all-taint-json/taint.json b/regression/symex-taint-analysis/array-all-taint-json/taint.json
new file mode 100644
index 00000000000..40c7105fba1
--- /dev/null
+++ b/regression/symex-taint-analysis/array-all-taint-json/taint.json
@@ -0,0 +1,6 @@
+[
+{
+	"loc": 0,
+	"taint": "tainted"
+}
+]
\ No newline at end of file
diff --git a/regression/symex-taint-analysis/array-all-taint-json/test.desc b/regression/symex-taint-analysis/array-all-taint-json/test.desc
new file mode 100644
index 00000000000..e82794f1c78
--- /dev/null
+++ b/regression/symex-taint-analysis/array-all-taint-json/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple --taint-file taint.json
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/array-taint-inline/array_taint.c b/regression/symex-taint-analysis/array-taint-inline/array_taint.c
new file mode 100644
index 00000000000..a78ababf38f
--- /dev/null
+++ b/regression/symex-taint-analysis/array-taint-inline/array_taint.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	__CPROVER_set_taint("main::1::x[3]", "tainted");
+
+	int y = x[3];
+	
+	x[0] = ++y;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::x[0]", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/array-taint-inline/main.c b/regression/symex-taint-analysis/array-taint-inline/main.c
new file mode 100644
index 00000000000..a78ababf38f
--- /dev/null
+++ b/regression/symex-taint-analysis/array-taint-inline/main.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	__CPROVER_set_taint("main::1::x[3]", "tainted");
+
+	int y = x[3];
+	
+	x[0] = ++y;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::x[0]", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/array-taint-inline/test.desc b/regression/symex-taint-analysis/array-taint-inline/test.desc
new file mode 100644
index 00000000000..bd29ae0ffb0
--- /dev/null
+++ b/regression/symex-taint-analysis/array-taint-inline/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/array-taint-json/array_taint.c b/regression/symex-taint-analysis/array-taint-json/array_taint.c
new file mode 100644
index 00000000000..59dce2568c5
--- /dev/null
+++ b/regression/symex-taint-analysis/array-taint-json/array_taint.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	int y = x[3];
+	
+	x[0] = ++y;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::x[0]", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/array-taint-json/main.c b/regression/symex-taint-analysis/array-taint-json/main.c
new file mode 100644
index 00000000000..59dce2568c5
--- /dev/null
+++ b/regression/symex-taint-analysis/array-taint-json/main.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	int y = x[3];
+	
+	x[0] = ++y;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::x[0]", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/array-taint-json/taint.json b/regression/symex-taint-analysis/array-taint-json/taint.json
new file mode 100644
index 00000000000..c4fde6b5a99
--- /dev/null
+++ b/regression/symex-taint-analysis/array-taint-json/taint.json
@@ -0,0 +1,7 @@
+[
+{
+	"loc": 0,
+	"taint": "tainted",
+	"symbol": "main::1::x[3]"
+}
+]
\ No newline at end of file
diff --git a/regression/symex-taint-analysis/array-taint-json/test.desc b/regression/symex-taint-analysis/array-taint-json/test.desc
new file mode 100644
index 00000000000..e82794f1c78
--- /dev/null
+++ b/regression/symex-taint-analysis/array-taint-json/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple --taint-file taint.json
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/array-untaint-inline/array_untaint.c b/regression/symex-taint-analysis/array-untaint-inline/array_untaint.c
new file mode 100644
index 00000000000..f9259ea1cf4
--- /dev/null
+++ b/regression/symex-taint-analysis/array-untaint-inline/array_untaint.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	__CPROVER_set_taint("main::1::x[3]", "tainted");
+
+	int y = x[3];
+
+	x[1] = ++y;
+
+	// assert c is tainted.
+	assert(!__CPROVER_is_taint("main::1::x[0]", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/array-untaint-inline/main.c b/regression/symex-taint-analysis/array-untaint-inline/main.c
new file mode 100644
index 00000000000..f9259ea1cf4
--- /dev/null
+++ b/regression/symex-taint-analysis/array-untaint-inline/main.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main(){
+
+	int x[4];
+
+	__CPROVER_set_taint("main::1::x[3]", "tainted");
+
+	int y = x[3];
+
+	x[1] = ++y;
+
+	// assert c is tainted.
+	assert(!__CPROVER_is_taint("main::1::x[0]", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/array-untaint-inline/test.desc b/regression/symex-taint-analysis/array-untaint-inline/test.desc
new file mode 100644
index 00000000000..bd29ae0ffb0
--- /dev/null
+++ b/regression/symex-taint-analysis/array-untaint-inline/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/func-taint-inline/func_taint.c b/regression/symex-taint-analysis/func-taint-inline/func_taint.c
new file mode 100644
index 00000000000..064efdba1ad
--- /dev/null
+++ b/regression/symex-taint-analysis/func-taint-inline/func_taint.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stdlib.h>
+
+
+int main(){
+
+	int *x = malloc(sizeof(int));
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	*x = 9;
+
+	int *y = x;
+
+	assert(__CPROVER_is_taint("main::1::y", "tainted"));
+	free(y);
+
+    return 0;
+}
diff --git a/regression/symex-taint-analysis/func-taint-inline/main.c b/regression/symex-taint-analysis/func-taint-inline/main.c
new file mode 100644
index 00000000000..ffe6a906aad
--- /dev/null
+++ b/regression/symex-taint-analysis/func-taint-inline/main.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main(){
+
+	int *x = malloc(sizeof(int));
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	*x = 9;
+
+	int *y = x;
+
+	assert(__CPROVER_is_taint("main::1::y", "tainted"));
+	free(y);
+
+    return 0;
+}
diff --git a/regression/symex-taint-analysis/func-taint-inline/test.desc b/regression/symex-taint-analysis/func-taint-inline/test.desc
new file mode 100644
index 00000000000..bd29ae0ffb0
--- /dev/null
+++ b/regression/symex-taint-analysis/func-taint-inline/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/loop-taint-inline/loop_taint.c b/regression/symex-taint-analysis/loop-taint-inline/loop_taint.c
new file mode 100644
index 00000000000..1879b3c9302
--- /dev/null
+++ b/regression/symex-taint-analysis/loop-taint-inline/loop_taint.c
@@ -0,0 +1,23 @@
+#include <assert.h>
+
+int main(){
+
+	int j;
+
+	__CPROVER_set_taint("main::1::j", "tainted");
+
+
+	int x[4];
+
+	int i = 0;
+
+	for (i = 0; i < 4; i++){
+
+		 x[i] = i == 4 ? j : 0;
+	}
+
+	assert(__CPROVER_is_taint("main::1::x[3]", "tainted"));
+
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/loop-taint-inline/main.c b/regression/symex-taint-analysis/loop-taint-inline/main.c
new file mode 100644
index 00000000000..e3e472db2a6
--- /dev/null
+++ b/regression/symex-taint-analysis/loop-taint-inline/main.c
@@ -0,0 +1,27 @@
+#include <assert.h>
+
+int main() {
+
+	int j;
+
+	__CPROVER_set_taint("main::1::j", "tainted");
+
+	int x[4];
+
+	int i = 0;
+
+	for (i = 0; i < 4; i++) {
+
+		if (i == 3)
+			x[i] = j;
+		else
+			x[i] = 0;
+	}
+
+	assert(__CPROVER_is_taint("main::1::x[0]", "untainted"));
+	assert(__CPROVER_is_taint("main::1::x[1]", "untainted"));
+	assert(__CPROVER_is_taint("main::1::x[2]", "untainted"));
+	assert(__CPROVER_is_taint("main::1::x[3]", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/loop-taint-inline/test.desc b/regression/symex-taint-analysis/loop-taint-inline/test.desc
new file mode 100644
index 00000000000..bd29ae0ffb0
--- /dev/null
+++ b/regression/symex-taint-analysis/loop-taint-inline/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/loop-untaint-inline/loop_untaint.c b/regression/symex-taint-analysis/loop-untaint-inline/loop_untaint.c
new file mode 100644
index 00000000000..7908904019a
--- /dev/null
+++ b/regression/symex-taint-analysis/loop-untaint-inline/loop_untaint.c
@@ -0,0 +1,23 @@
+#include <assert.h>
+
+int main(){
+
+	int j;
+
+	__CPROVER_set_taint("main::1::j", "tainted");
+
+
+	int x[4];
+
+	int i = 0;
+
+	for (i = 0; i < 4; i++){
+
+		 x[i] = i == 4 ? j : 0;
+	}
+
+	assert(!__CPROVER_is_taint("main::1::x[3]", "tainted"));
+
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/loop-untaint-inline/main.c b/regression/symex-taint-analysis/loop-untaint-inline/main.c
new file mode 100644
index 00000000000..e3179992be1
--- /dev/null
+++ b/regression/symex-taint-analysis/loop-untaint-inline/main.c
@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int main(){
+
+	int j;
+
+	__CPROVER_set_taint("main::1::j", "tainted");
+
+
+	int x[4];
+
+	int i = 0;
+
+	for (i = 0; i < 4; i++){
+
+		 x[i] = (i == 8) ? j : 0;
+	}
+
+
+	assert(__CPROVER_is_taint("main::1::x[3]", "tainted"));
+
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/loop-untaint-inline/test.desc b/regression/symex-taint-analysis/loop-untaint-inline/test.desc
new file mode 100644
index 00000000000..bd29ae0ffb0
--- /dev/null
+++ b/regression/symex-taint-analysis/loop-untaint-inline/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/recursive-taint-inline/main.c b/regression/symex-taint-analysis/recursive-taint-inline/main.c
new file mode 100644
index 00000000000..987f7aa891e
--- /dev/null
+++ b/regression/symex-taint-analysis/recursive-taint-inline/main.c
@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int factorial(unsigned int i) {
+
+	if (i <= 1) {
+		return 1;
+	}
+	return i * factorial(i - 1);
+}
+
+int main() {
+
+	unsigned int x = 80;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	unsigned int y = factorial(x);
+	
+	assert(__CPROVER_is_taint("main::1::y", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/recursive-taint-inline/test.desc b/regression/symex-taint-analysis/recursive-taint-inline/test.desc
new file mode 100644
index 00000000000..bd29ae0ffb0
--- /dev/null
+++ b/regression/symex-taint-analysis/recursive-taint-inline/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/recursive-untaint-inline/main.c b/regression/symex-taint-analysis/recursive-untaint-inline/main.c
new file mode 100644
index 00000000000..670691caa2f
--- /dev/null
+++ b/regression/symex-taint-analysis/recursive-untaint-inline/main.c
@@ -0,0 +1,26 @@
+#include <assert.h>
+
+int factorial(unsigned int i) {
+
+	if (i <= 1) {
+		return 1;
+	}
+	return i * factorial(i - 1);
+}
+
+int main() {
+
+	unsigned int y;
+
+	unsigned int x = 80;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	y = factorial(x);
+
+	y = 0;
+	
+	assert(!__CPROVER_is_taint("main::1::y", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/recursive-untaint-inline/test.desc b/regression/symex-taint-analysis/recursive-untaint-inline/test.desc
new file mode 100644
index 00000000000..bd29ae0ffb0
--- /dev/null
+++ b/regression/symex-taint-analysis/recursive-untaint-inline/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/simple-taint-inline/main.c b/regression/symex-taint-analysis/simple-taint-inline/main.c
new file mode 100644
index 00000000000..479516fc1ce
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-taint-inline/main.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int main(){
+
+	int x;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	// taint propagation from x to y.
+	int y = x;
+	
+	// taint propagation from y to c.
+	int c = y + 7;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/simple-taint-inline/simple_taint.c b/regression/symex-taint-analysis/simple-taint-inline/simple_taint.c
new file mode 100644
index 00000000000..479516fc1ce
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-taint-inline/simple_taint.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int main(){
+
+	int x;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	// taint propagation from x to y.
+	int y = x;
+	
+	// taint propagation from y to c.
+	int c = y + 7;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/simple-taint-inline/test.desc b/regression/symex-taint-analysis/simple-taint-inline/test.desc
new file mode 100644
index 00000000000..bd29ae0ffb0
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-taint-inline/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/simple-taint-json/main.c b/regression/symex-taint-analysis/simple-taint-json/main.c
new file mode 100644
index 00000000000..3881f6396c0
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-taint-json/main.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main(){
+
+	int x;
+
+	// taint propagation from x to y.
+	int y = x;
+	
+	// taint propagation from y to c.
+	int c = y + 7;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/simple-taint-json/simple_taint.c b/regression/symex-taint-analysis/simple-taint-json/simple_taint.c
new file mode 100644
index 00000000000..3881f6396c0
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-taint-json/simple_taint.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main(){
+
+	int x;
+
+	// taint propagation from x to y.
+	int y = x;
+	
+	// taint propagation from y to c.
+	int c = y + 7;
+
+	// assert c is tainted.
+	assert(__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/simple-taint-json/taint.json b/regression/symex-taint-analysis/simple-taint-json/taint.json
new file mode 100644
index 00000000000..40c7105fba1
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-taint-json/taint.json
@@ -0,0 +1,6 @@
+[
+{
+	"loc": 0,
+	"taint": "tainted"
+}
+]
\ No newline at end of file
diff --git a/regression/symex-taint-analysis/simple-taint-json/test.desc b/regression/symex-taint-analysis/simple-taint-json/test.desc
new file mode 100644
index 00000000000..e82794f1c78
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-taint-json/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple --taint-file taint.json
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/simple-untaint-inline/main.c b/regression/symex-taint-analysis/simple-untaint-inline/main.c
new file mode 100644
index 00000000000..ea75d486502
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-untaint-inline/main.c
@@ -0,0 +1,20 @@
+#include <assert.h>
+
+int main(){
+
+	int x;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	int y = x;
+	
+	int c = y + 8;
+
+	// c is set an immediate value.
+	c = 0;
+
+	// assert that c is not tainted.
+	assert(!__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/simple-untaint-inline/simple_untaint.c b/regression/symex-taint-analysis/simple-untaint-inline/simple_untaint.c
new file mode 100644
index 00000000000..ea75d486502
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-untaint-inline/simple_untaint.c
@@ -0,0 +1,20 @@
+#include <assert.h>
+
+int main(){
+
+	int x;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	int y = x;
+	
+	int c = y + 8;
+
+	// c is set an immediate value.
+	c = 0;
+
+	// assert that c is not tainted.
+	assert(!__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/simple-untaint-inline/test.desc b/regression/symex-taint-analysis/simple-untaint-inline/test.desc
new file mode 100644
index 00000000000..bd29ae0ffb0
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-untaint-inline/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/simple-untaint-json/main.c b/regression/symex-taint-analysis/simple-untaint-json/main.c
new file mode 100644
index 00000000000..bdc15d8cb2d
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-untaint-json/main.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+
+int main(){
+
+	int x;
+
+	int y = x;
+	
+	int c = y + 8;
+
+	// c is set an immediate value.
+	c = 0;
+
+	// assert that c is not tainted.
+	assert(!__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/simple-untaint-json/simple_untaint.c b/regression/symex-taint-analysis/simple-untaint-json/simple_untaint.c
new file mode 100644
index 00000000000..bdc15d8cb2d
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-untaint-json/simple_untaint.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+
+int main(){
+
+	int x;
+
+	int y = x;
+	
+	int c = y + 8;
+
+	// c is set an immediate value.
+	c = 0;
+
+	// assert that c is not tainted.
+	assert(!__CPROVER_is_taint("main::1::c", "tainted"));
+
+	return 0;
+}
diff --git a/regression/symex-taint-analysis/simple-untaint-json/taint.json b/regression/symex-taint-analysis/simple-untaint-json/taint.json
new file mode 100644
index 00000000000..40c7105fba1
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-untaint-json/taint.json
@@ -0,0 +1,6 @@
+[
+{
+	"loc": 0,
+	"taint": "tainted"
+}
+]
\ No newline at end of file
diff --git a/regression/symex-taint-analysis/simple-untaint-json/test.desc b/regression/symex-taint-analysis/simple-untaint-json/test.desc
new file mode 100644
index 00000000000..e82794f1c78
--- /dev/null
+++ b/regression/symex-taint-analysis/simple-untaint-json/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple --taint-file taint.json
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/struct-copy-taint-inline/main.c b/regression/symex-taint-analysis/struct-copy-taint-inline/main.c
new file mode 100644
index 00000000000..ae5def0c4b6
--- /dev/null
+++ b/regression/symex-taint-analysis/struct-copy-taint-inline/main.c
@@ -0,0 +1,24 @@
+#include <assert.h>
+
+struct name{
+   int a;
+   float b;
+};
+int main(){
+
+	int x;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	struct name my_name;
+	my_name.a = x;
+	my_name.b = -2.1459f;
+
+	struct name my_name_copy;
+	my_name_copy.a = my_name.a;
+	my_name_copy.b = my_name.b;
+
+	assert(__CPROVER_is_taint("main::1::my_name_copy.a", "tainted"));
+
+    return 0;
+}
diff --git a/regression/symex-taint-analysis/struct-copy-taint-inline/test.desc b/regression/symex-taint-analysis/struct-copy-taint-inline/test.desc
new file mode 100644
index 00000000000..bd29ae0ffb0
--- /dev/null
+++ b/regression/symex-taint-analysis/struct-copy-taint-inline/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/struct-taint-inline/main.c b/regression/symex-taint-analysis/struct-taint-inline/main.c
new file mode 100644
index 00000000000..ba15f87bb9e
--- /dev/null
+++ b/regression/symex-taint-analysis/struct-taint-inline/main.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+
+struct name{
+   int a;
+   float b;
+};
+int main(){
+
+	int x;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	struct name my_name;
+	my_name.a = x;
+
+	assert(__CPROVER_is_taint("main::1::my_name.a", "tainted"));
+
+    return 0;
+}
diff --git a/regression/symex-taint-analysis/struct-taint-inline/struct_taint.c b/regression/symex-taint-analysis/struct-taint-inline/struct_taint.c
new file mode 100644
index 00000000000..554ce7ffe3b
--- /dev/null
+++ b/regression/symex-taint-analysis/struct-taint-inline/struct_taint.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+
+struct name{
+   int a;
+   float b;
+};
+int main(){
+
+	int x;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	struct name nm;
+	nm.a = x;
+
+	assert(__CPROVER_is_taint("main::1::nm.a", "tainted"));
+
+    return 0;
+}
diff --git a/regression/symex-taint-analysis/struct-taint-inline/test.desc b/regression/symex-taint-analysis/struct-taint-inline/test.desc
new file mode 100644
index 00000000000..bd29ae0ffb0
--- /dev/null
+++ b/regression/symex-taint-analysis/struct-taint-inline/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/struct-untaint-inline/main.c b/regression/symex-taint-analysis/struct-untaint-inline/main.c
new file mode 100644
index 00000000000..446cb229152
--- /dev/null
+++ b/regression/symex-taint-analysis/struct-untaint-inline/main.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+
+struct name{
+   int a;
+   float b;
+};
+int main(){
+
+	int x;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	struct name my_name;
+	my_name.a = x;
+
+	assert(__CPROVER_is_taint("main::1::my_name.b", "untainted"));
+
+    return 0;
+}
diff --git a/regression/symex-taint-analysis/struct-untaint-inline/struct_untaint.c b/regression/symex-taint-analysis/struct-untaint-inline/struct_untaint.c
new file mode 100644
index 00000000000..38d3050aae5
--- /dev/null
+++ b/regression/symex-taint-analysis/struct-untaint-inline/struct_untaint.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+
+struct name{
+   int a;
+   float b;
+};
+int main(){
+
+	int x;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	struct name nm;
+	nm.a = x;
+
+	assert(!__CPROVER_is_taint("main::1::nm.b", "tainted"));
+
+    return 0;
+}
diff --git a/regression/symex-taint-analysis/struct-untaint-inline/test.desc b/regression/symex-taint-analysis/struct-untaint-inline/test.desc
new file mode 100644
index 00000000000..bd29ae0ffb0
--- /dev/null
+++ b/regression/symex-taint-analysis/struct-untaint-inline/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--taint simple
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/symex-taint-analysis/test2/taint.json b/regression/symex-taint-analysis/test2/taint.json
new file mode 100644
index 00000000000..d893dba1984
--- /dev/null
+++ b/regression/symex-taint-analysis/test2/taint.json
@@ -0,0 +1,6 @@
+[
+{
+       	"loc": 17,
+       	"taint": "tainted"
+}
+]
\ No newline at end of file
diff --git a/regression/symex-taint-analysis/test2/taint_test.c b/regression/symex-taint-analysis/test2/taint_test.c
new file mode 100644
index 00000000000..c59099d2610
--- /dev/null
+++ b/regression/symex-taint-analysis/test2/taint_test.c
@@ -0,0 +1,14 @@
+int func() {
+	int x;
+
+	int y = x;
+
+	int z;
+
+	int x = z;
+
+	int d;
+
+	int e = d + 1;
+}
+
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 9b9de4c06f7..6a4a56e65ee 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -133,6 +133,10 @@ void ansi_c_internal_additions(std::string &code)
     "__CPROVER_bool __CPROVER_get_must(const void *, const char *);\n"
     "__CPROVER_bool __CPROVER_get_may(const void *, const char *);\n"
 
+    "__CPROVER_bool __CPROVER_is_taint(const char *, const char *);\n"
+    "void           __CPROVER_set_taint(const char *, const char *);\n"
+    "const void *   __CPROVER_get_taint(const char *);\n"
+
     "const unsigned __CPROVER_constant_infinity_uint;\n"
     "typedef void __CPROVER_integer;\n"
     "typedef void __CPROVER_rational;\n"
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 884cf94d94d..ce2e19468f4 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2375,6 +2375,57 @@ exprt c_typecheck_baset::do_special_functions(
 
     return get_may_expr;
   }
+  else if(identifier==CPROVER_PREFIX "is_taint")
+  {
+    if(expr.arguments().size()!=2)
+    {
+      err_location(f_op);
+      error() << "is_taint expects two operands" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    exprt is_taint_expr=
+      binary_predicate_exprt(expr.arguments()[0], "is_taint", expr.arguments()[1]);
+    is_taint_expr.add_source_location()=source_location;
+
+    return is_taint_expr;
+  }
+  else if(identifier==CPROVER_PREFIX "set_taint")
+  {
+    if(expr.arguments().size()!=2)
+    {
+      err_location(f_op);
+      error() << "set_taint expects two operands" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    exprt set_taint_expr=
+      binary_predicate_exprt(expr.arguments()[0], "set_taint", expr.arguments()[1]);
+    set_taint_expr.add_source_location()=source_location;
+
+    return set_taint_expr;
+  }
+  else if(identifier==CPROVER_PREFIX "get_taint")
+  {
+    if(expr.arguments().size()!=1)
+    {
+      err_location(f_op);
+      error() << "get_taint expects one operand" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    exprt get_taint_expr=
+      unary_predicate_exprt("get_taint", expr.arguments()[0]);
+    get_taint_expr.add_source_location()=source_location;
+
+    return get_taint_expr;
+  }
   else if(identifier==CPROVER_PREFIX "invalid_pointer")
   {
     if(expr.arguments().size()!=1)
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index dc190fe9c39..826e77be601 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -4759,6 +4759,15 @@ std::string expr2ct::convert(
   else if(src.id()==ID_type)
     return convert(src.type());
 
+  else if(src.id()==ID_set_taint)
+    return convert_function(src, "__CPROVER_set_taint", precedence=16);
+
+  else if(src.id()==ID_get_taint)
+      return convert_function(src, "__CPROVER_get_taint", precedence=16);
+
+  else if(src.id()==ID_is_taint)
+      return convert_function(src, "__CPROVER_is_taint", precedence=16);
+
   // no C language expression for internal representation
   return convert_norep(src, precedence);
 }
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
index 42c92b7ed7a..a78f85055da 100644
--- a/src/ansi-c/library/cprover.h
+++ b/src/ansi-c/library/cprover.h
@@ -130,3 +130,8 @@ __CPROVER_bool __CPROVER_get_may(const void *, const char *);
 #define __CPROVER_danger_max_solution_size 1
 #define __CPROVER_danger_number_of_vars 1
 #define __CPROVER_danger_number_of_consts 1
+
+__CPROVER_bool __CPROVER_is_taint(const char *, const char *);
+void           __CPROVER_set_taint(const char *, const char *);
+const char *   __CPROVER_get_taint(const char *);
+
diff --git a/src/path-symex/Makefile b/src/path-symex/Makefile
index 918a6763ab2..8346f81a204 100644
--- a/src/path-symex/Makefile
+++ b/src/path-symex/Makefile
@@ -1,7 +1,10 @@
 SRC = locs.cpp var_map.cpp path_symex_history.cpp path_symex_state.cpp \
       path_symex.cpp build_goto_trace.cpp path_replay.cpp \
-      path_symex_state_read.cpp
-
+      path_symex_state_read.cpp \
+      path_symex_taint_data.cpp \
+      path_symex_taint_analysis.cpp \
+	  path_symex_taint_parser.cpp
+	  
 INCLUDES= -I ..
 
 include ../config.inc
diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp
index f044db53e1c..a2d6e9bc318 100644
--- a/src/path-symex/path_symex.cpp
+++ b/src/path-symex/path_symex.cpp
@@ -134,12 +134,9 @@ void path_symext::assign(
   exprt ssa_lhs=
     state.read_no_propagate(dereference_exprt(lhs_address));
 
-  // read the rhs
-  exprt ssa_rhs=state.read(rhs);
-
   // start recursion on lhs
   exprt::operandst _guard; // start with empty guard
-  assign_rec(state, _guard, ssa_lhs, ssa_rhs);
+  assign_rec(state, _guard, ssa_lhs, rhs);
 }
 
 /*******************************************************************\
@@ -306,8 +303,9 @@ void path_symext::assign_rec(
   path_symex_statet &state,
   exprt::operandst &guard, 
   const exprt &ssa_lhs, 
-  const exprt &ssa_rhs)
+  const exprt &rhs)
 {
+  const exprt ssa_rhs=state.read(rhs);
   //const typet &ssa_lhs_type=state.var_map.ns.follow(ssa_lhs.type());
   
   #ifdef DEBUG
@@ -352,6 +350,17 @@ void path_symext::assign_rec(
     {
       path_symex_statet::var_statet &var_state=state.get_var_state(var_info);
       var_state.value=nil_exprt();
+
+      if(state.taint_engine.enabled)
+      {
+        /*
+         *  If JSON specifies a rule, we enforce taint. Otherwise, we set
+         *  taint to the top most position in lattice (untaint).
+         */
+        var_state.taint=
+            (state.is_enforced_taint_json()) ?
+                state.get_enforced_taint() : taint_enginet::get_top_elem();
+      }
     }
     else
     {
@@ -377,6 +386,22 @@ void path_symext::assign_rec(
       // propagate the rhs?
       path_symex_statet::var_statet &var_state=state.get_var_state(var_info);
       var_state.value=propagate(ssa_rhs)?ssa_rhs:nil_exprt();
+
+      if (state.taint_engine.enabled) {
+
+        // Check if taint is enforced as specified in JSON file.
+        if (state.is_enforced_taint_json()){
+          var_state.taint = state.get_enforced_taint();
+        }
+        else{
+          taintt taint = state.taint_engine.get_top_elem();
+
+          // Retrieve and propagate taint state.
+          recursive_taint_extraction(state.read_no_propagate(rhs), taint,
+              state);
+          var_state.taint = taint;
+        }
+      }
     }
   }
   else if(ssa_lhs.id()==ID_member)
@@ -903,6 +928,7 @@ void path_symext::operator()(
 {
   const goto_programt::instructiont &instruction=
     *state.get_instruction();
+  loc_reft pc = state.pc();
     
   #ifdef DEBUG
   std::cout << "path_symext::operator(): "
@@ -1028,6 +1054,7 @@ void path_symext::operator()(
       if(statement==ID_expression)
       {
         // like SKIP
+        path_symex_handle_taint_expr(state, code);
       }
       else if(statement==ID_printf)
       {
@@ -1055,6 +1082,146 @@ void path_symext::operator()(
   default:
     throw "path_symext: unexpected instruction";
   }
+
+  path_symex_set_taint_via_symbols(state, pc);
+}
+
+/*******************************************************************
+ Function: recursive_taint_extraction()
+
+ Inputs: Takes a taint as a placeholder for recursion. At start,
+ needs to be the top most element in the lattice.
+
+ Outputs: The lowest taint element met by the operands.
+
+ Purpose: Finds the taint state in an expression via meet function.
+
+ \*******************************************************************/
+void path_symext::recursive_taint_extraction(const exprt &expr, taintt &taint,
+    path_symex_statet &state)
+{
+  // if taint engine is not enabled, simply return.
+  if(!state.taint_engine.enabled)
+    return;
+
+  // Check if we reached a symbol.
+  if(expr.id() == ID_symbol)
+  {
+
+    // Convert expression to symbol and perform look-up using var_map.
+    symbol_exprt symbol=to_symbol_expr(expr);
+    const irep_idt &full_identifier=symbol.get(ID_C_full_identifier);
+    var_mapt::var_infot &var_info=state.var_map[full_identifier];
+    assert(var_info.full_identifier == full_identifier);
+    path_symex_statet::var_statet &var_state=state.get_var_state(var_info);
+
+    // Get the lowest position in the lattice where the states meet.
+    taint=state.taint_engine.meet(expr.id(), taint, var_state.taint);
+  }
+
+  // Progress down the expression tree, to check operands.
+  forall_operands(it, expr)
+  {
+    recursive_taint_extraction(*it, taint, state);
+  }
+}
+
+/*******************************************************************
+ Function: path_symex_set_taint_symbols()
+
+ Inputs: Takes a path_symex state, which contains the taint engine.
+
+ Outputs: Nothing.
+
+ Purpose: Checks each rule at a given pc for symbol taint, and
+ propagates taint accordingly.
+
+ \*******************************************************************/
+
+void path_symext::path_symex_set_taint_via_symbols(path_symex_statet &state,
+    const loc_reft &pc)
+{
+  // if taint engine is not enabled, simply return.
+  if(!state.taint_engine.enabled)
+    return;
+
+  if(state.taint_engine.enabled)
+  {
+    // Loops through all symbols that need to be tainted at a given loc.
+    for (auto rule : state.taint_engine.taint_data->data[pc.loc_number])
+    {
+
+      // Check if symbol flag is set. If false, next rule is considered.
+      if(!rule.symbol_flag)
+        continue;
+
+      /*  We assume that the user provides the correct symbol name as
+       * input. This is used for looking up using the var_map.
+       */
+      var_mapt::var_infot &var_info=state.var_map[rule.symbol_name];
+      // Assert that the symbol name matches the identifier.
+      assert(var_info.full_identifier == rule.symbol_name);
+
+      path_symex_statet::var_statet &var_state=state.get_var_state(var_info);
+
+      // Force taint.
+      var_state.taint=rule.taint;
+    }
+  }
+}
+
+/*******************************************************************
+ Function: path_symex_handle_taint_set_taint_function
+
+ Inputs: Takes a path_symex state and codet.
+
+ Outputs: Nothing.
+
+ Purpose: Responsible for setting taint via the CPROVER Special Function.
+
+ \*******************************************************************/
+
+void path_symext::path_symex_handle_taint_expr(path_symex_statet &state,
+    const codet &code)
+{
+  if(!code.has_operands())
+    return;
+
+  assert(code.has_operands());
+
+  // Check if code is a set_taint CPROVER special function
+  if(code.op0().id() == ID_set_taint)
+  {
+    exprt src=code.op0();
+    assert(src.has_operands());
+
+    // Retrieve Symbol name.
+    assert(src.op0().id() == ID_address_of);
+    assert(src.op0().has_operands());
+    assert(src.op0().op0().id() == ID_index);
+    assert(src.op0().op0().has_operands());
+    assert(src.op0().op0().op0().id() == ID_string_constant);
+
+    dstring symbol_name=src.op0().op0().op0().get_string(ID_value);
+
+    // Retrieve taint state (as string).
+    assert(src.op1().id() == ID_address_of);
+    assert(src.op1().has_operands());
+    assert(src.op1().op0().id() == ID_index);
+    assert(src.op1().op0().has_operands());
+    assert(src.op1().op0().op0().id() == ID_string_constant);
+
+    // Get taint state
+    taintt taint=state.taint_engine.parse_taint(
+        src.op1().op0().op0().get_string(ID_value));
+
+    // Set taint
+    var_mapt::var_infot &var_info=state.var_map[symbol_name];
+    assert(var_info.full_identifier == symbol_name);
+    path_symex_statet::var_statet &var_state=state.get_var_state(var_info);
+
+    var_state.taint=taint;
+  }
 }
 
 /*******************************************************************\
diff --git a/src/path-symex/path_symex_class.h b/src/path-symex/path_symex_class.h
index b7128002da2..843ecdd8b1b 100644
--- a/src/path-symex/path_symex_class.h
+++ b/src/path-symex/path_symex_class.h
@@ -86,9 +86,19 @@ class path_symext
     path_symex_statet &state,
     exprt::operandst &guard, // instantiated
     const exprt &ssa_lhs, // instantiated, recursion here
-    const exprt &ssa_rhs); // instantiated
+    const exprt &rhs); // instantiated
 
   static bool propagate(const exprt &src);
+
+  void recursive_taint_extraction(
+      const exprt &expr,
+      taintt &taint,
+      path_symex_statet &state);
+
+  void path_symex_set_taint_via_symbols(path_symex_statet &state,
+  		const loc_reft &pc);
+
+  void path_symex_handle_taint_expr(path_symex_statet &state, const codet &code);
 };
 
 
diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp
index 853bf1c2475..6750a29b23e 100644
--- a/src/path-symex/path_symex_state.cpp
+++ b/src/path-symex/path_symex_state.cpp
@@ -42,9 +42,10 @@ Function: initial_state
 path_symex_statet initial_state(
   var_mapt &var_map,
   const locst &locs,
-  path_symex_historyt &path_symex_history)
+  path_symex_historyt &path_symex_history,
+  taint_enginet &taint_engine)
 {
-  path_symex_statet s(var_map, locs, path_symex_history);
+  path_symex_statet s(var_map, locs, path_symex_history, taint_engine);
   
   // create one new thread
   path_symex_statet::threadt &thread=s.add_thread();
@@ -96,6 +97,56 @@ void path_symex_statet::output(const threadt &thread, std::ostream &out) const
   out << std::endl;
 }
 
+
+/*******************************************************************
+   Function: path_symex_statet::is_enforced_taint_json
+
+	Inputs: Nothing.
+
+	Outputs: A bool that specifies whether json file enforces taint.
+
+	Purpose: Checks whether the json file enforces taint to a
+	variable.
+
+
+\*******************************************************************/
+
+bool path_symex_statet::is_enforced_taint_json()
+{
+  for (auto rule : taint_engine.taint_data->data[pc().loc_number])
+  {
+    if(!rule.symbol_flag)
+      return true;
+  }
+
+  // No set symbol flag has been found.
+  return false;
+}
+
+/*******************************************************************
+ Function: path_symex_statet::get_enforced_taint
+
+ Inputs: Nothing
+
+ Outputs: Returns the taint state to enforce.
+
+ Purpose: Gets the taint state to enforce.
+
+
+ \*******************************************************************/
+
+taintt path_symex_statet::get_enforced_taint()
+{
+  for (auto rule : taint_engine.taint_data->data[pc().loc_number])
+  {
+    if(!rule.symbol_flag)
+      return rule.taint;
+  }
+
+  throw "Taint not found.";
+}
+
+
 /*******************************************************************\
 
 Function: path_symex_statet::output
diff --git a/src/path-symex/path_symex_state.h b/src/path-symex/path_symex_state.h
index 7314ac5256f..50db53200e3 100644
--- a/src/path-symex/path_symex_state.h
+++ b/src/path-symex/path_symex_state.h
@@ -13,15 +13,18 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "var_map.h"
 #include "path_symex_history.h"
 
+#include <path-symex/path_symex_taint_data.h>
 struct path_symex_statet
 {
 public:
   inline path_symex_statet(
     var_mapt &_var_map,
     const locst &_locs,
-    path_symex_historyt &_path_symex_history):
+    path_symex_historyt &_path_symex_history,
+    taint_enginet &_taint_engine):
     var_map(_var_map),
     locs(_locs),
+    taint_engine(_taint_engine),
     inside_atomic_section(false),
     history(_path_symex_history),
     current_thread(0),
@@ -38,6 +41,8 @@ struct path_symex_statet
   var_mapt &var_map;
   const locst &locs;
 
+  taint_enginet &taint_engine;
+
   // the value of a variable
   struct var_statet
   {
@@ -45,13 +50,22 @@ struct path_symex_statet
     exprt value;
     symbol_exprt ssa_symbol;
     
+    // For recording taint.
+    taintt taint;
+
     // for uninterpreted functions or arrays we maintain an index set
     typedef std::set<exprt> index_sett;
     index_sett index_set;
 
+    // For recording taint in arrays.
+    typedef std::set<taintt> taint_index_sett;
+    taint_index_sett taint_index_set;
+
+    // taint value set to untaint by default.
     var_statet():
       value(nil_exprt()),
-      ssa_symbol(irep_idt())
+      ssa_symbol(irep_idt()),
+      taint(taint_enginet::get_top_elem())
     {
     }
   };
@@ -154,7 +168,11 @@ struct path_symex_statet
   {
     threads[current_thread].pc=new_pc;
   }
-  
+
+  // Enforce taint functions
+  bool is_enforced_taint_json();
+  taintt get_enforced_taint();
+
   // output  
   void output(std::ostream &out) const;
   void output(const threadt &thread, std::ostream &out) const;
@@ -238,6 +256,7 @@ struct path_symex_statet
 path_symex_statet initial_state(
   var_mapt &var_map,
   const locst &locs,
-  path_symex_historyt &);
+  path_symex_historyt &,
+  taint_enginet &);
   
 #endif
diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp
index 59e6ecfbcfe..075764b9aa8 100644
--- a/src/path-symex/path_symex_state_read.cpp
+++ b/src/path-symex/path_symex_state_read.cpp
@@ -347,6 +347,66 @@ exprt path_symex_statet::instantiate_rec(
     assert(src.type().id()==ID_code ||
            src.get_bool(ID_C_SSA_symbol));
   }
+  else if(src.id() == ID_is_taint)
+  {
+    // is_taint CProver special function in use.
+
+    /*
+     *  Fetch symbol name.
+     *
+     *  Note that string constants are rewritten into:
+     *    address_of -> index -> string_constant.
+     */
+    assert(src.op0().id() == ID_address_of);
+    assert(src.op0().op0().id() == ID_index);
+    assert(src.op0().op0().op0().id() == ID_string_constant);
+
+    dstring symbol_name=src.op0().op0().op0().get_string(ID_value);
+
+    // Fetch taint state query.
+    assert(src.op0().id() == ID_address_of);
+    assert(src.op0().op0().id() == ID_index);
+    assert(src.op0().op0().op0().id() == ID_string_constant);
+
+    taintt taint=taint_engine.parse_taint(
+        src.op1().op0().op0().get_string(ID_value));
+
+    // Perform look-up to get taint information.
+    var_mapt::var_infot &var_info=var_map[symbol_name];
+    assert(var_info.full_identifier == symbol_name);
+    path_symex_statet::var_statet &var_state=get_var_state(var_info);
+
+    // If tainted, return true expression. Otherwise, return false.
+    if(var_state.taint == taint)
+      return true_exprt();
+    else
+      return false_exprt();
+  }
+  else if(src.id() == ID_get_taint)
+  {
+    // get_taint CProver special function in use.
+
+    // Fetch symbol name
+    assert(src.op0().id() == ID_address_of);
+    assert(src.op0().op0().id() == ID_index);
+    assert(src.op0().op0().op0().id() == ID_string_constant);
+
+    dstring symbol_name=src.op0().op0().op0().get_string(ID_value);
+
+    // Perform look-up to get taint information.
+    var_mapt::var_infot &var_info=var_map[symbol_name];
+    assert(var_info.full_identifier == symbol_name);
+    path_symex_statet::var_statet &var_state=get_var_state(var_info);
+
+    // Get taint value as string.
+    dstring taint=taint_engine.get_taint_name(var_state.taint);
+
+    // Prepare string constant expression.
+    exprt out=src.op0();
+    out.op0().op0().set(ID_value, taint);
+
+    return out;
+  }
 
   if(!src.has_operands())
     return src;
diff --git a/src/path-symex/path_symex_taint_analysis.cpp b/src/path-symex/path_symex_taint_analysis.cpp
new file mode 100644
index 00000000000..0ad09e6920f
--- /dev/null
+++ b/src/path-symex/path_symex_taint_analysis.cpp
@@ -0,0 +1,96 @@
+/*******************************************************************
+ Module: Taint Engine Module
+
+ Author: Daniel Neville,	daniel.neville@cs.ox.ac.uk
+ John Galea,		john.galea@cs.ox.ac.uk
+
+ \*******************************************************************/
+
+#include "path_symex_taint_analysis.h"
+
+// Returns the maximal/top element of the lattice.
+const taintt path_symex_taint_analysis_enginet::get_top_elem()
+{
+  return 0;
+}
+
+const taintt path_symex_no_taint_analysis_enginet::get_bottom_elem() const
+{
+  return 0;
+}
+
+taintt path_symex_no_taint_analysis_enginet::meet(irep_idt id, taintt taint_1,
+    taintt taint_2) const
+{
+  return 0;
+}
+
+const std::string path_symex_no_taint_analysis_enginet::get_taint_analysis_name() const
+{
+  return "None";
+}
+
+taintt path_symex_no_taint_analysis_enginet::parse_taint(
+    std::string taint_name) const
+{
+  return 0;
+}
+
+std::string path_symex_no_taint_analysis_enginet::get_taint_name(
+    taintt taint) const
+{
+  return "";
+}
+
+const taintt path_symex_simple_taint_analysis_enginet::get_bottom_elem() const
+{
+  return TAINTED;
+}
+
+taintt path_symex_simple_taint_analysis_enginet::meet(irep_idt id,
+    taintt taint1, taintt taint2) const
+{
+  // Perform checks on passed taint types.
+  if(taint1 != UNTAINTED && taint1 != TAINTED)
+  {
+    throw "First taint type  passed to meet function is invalid.";
+  }
+
+  if(taint2 != UNTAINTED && taint2 != TAINTED)
+  {
+    throw "Second taint type passed to meet function is invalid.";
+  }
+
+  // If either taint state is tainted, then the result is tainted.
+  return (taint1 == TAINTED || taint2 == TAINTED) ? TAINTED : UNTAINTED;
+}
+
+const std::string path_symex_simple_taint_analysis_enginet::get_taint_analysis_name() const
+{
+  return "Simple taint domain.";
+}
+
+taintt path_symex_simple_taint_analysis_enginet::parse_taint(
+    std::string taint_name) const
+{
+  /* Parse from strings -> taint types */
+  if(taint_name == "untainted")
+    return UNTAINTED;
+  if(taint_name == "tainted")
+    return TAINTED;
+  throw "Taint type not recognised";
+}
+
+std::string path_symex_simple_taint_analysis_enginet::get_taint_name(
+    taintt taint) const
+{
+  /* Parse from taint -> strings types */
+  switch (taint)
+  {
+    case UNTAINTED:
+      return "untainted";
+    case TAINTED:
+      return "tainted";
+  }
+  throw "Taint type not recognised";
+}
diff --git a/src/path-symex/path_symex_taint_analysis.h b/src/path-symex/path_symex_taint_analysis.h
new file mode 100644
index 00000000000..8c648e03779
--- /dev/null
+++ b/src/path-symex/path_symex_taint_analysis.h
@@ -0,0 +1,123 @@
+/*******************************************************************
+ Module: Taint Engine Module
+
+ We define taint lattices to represent taint types (the domain).
+ In order to implement analysis using a new taint domain, one
+ needs to implement the path_symex_taint_analysis_enginet
+ interface.
+
+ Author: Daniel Neville,	daniel.neville@cs.ox.ac.uk
+ John Galea,				john.galea@cs.ox.ac.uk
+
+ \*******************************************************************/
+
+#ifndef CPROVER_PATH_SYMEX_TAINT_ANALYSIS_H
+#define CPROVER_PATH_SYMEX_TAINT_ANALYSIS_H
+
+#include <util/std_expr.h>
+#include "locs.h"
+#include <string>
+
+/* Future work.
+ *
+ * Consider whether a goto_check for printf not-tainted should be inserted
+ * (but under what taint engine?)
+ *
+ * Make taint JSON file syntactically 'similar' to A.I. taint file.
+ *
+ * Consider tainting function calls under some semantics.
+ */
+
+// We represent positions in a taint lattice as unsigned short value.
+typedef unsigned short taintt;
+
+class taint_datat;
+
+/**
+ * 	Interface for taint analysis, which differ in their considered domains.
+ */
+class path_symex_taint_analysis_enginet
+{
+
+public:
+
+  inline virtual ~path_symex_taint_analysis_enginet()
+  {
+  }
+
+  // Returns the maximal/top element of the lattice.
+  const static taintt get_top_elem();
+
+  // Returns the minimal/lowest element of the lattice.
+  virtual const taintt get_bottom_elem() const = 0;
+
+  // Given two taint types, the meet of the two is returned.
+  virtual taintt meet(irep_idt id, const taintt taint_1,
+      const taintt taint_2) const = 0;
+
+  // Returns the name of the taint analysis engine
+  virtual const std::string get_taint_analysis_name() const = 0;
+
+  // Returns the taint type corresponding to the string
+  virtual taintt parse_taint(const std::string taint_name) const = 0;
+
+  // Returns the name of a given taint type
+  virtual std::string get_taint_name(const taintt taint) const = 0;
+
+  // Taint Data.
+  taint_datat *taint_data;
+
+  // A flag specifying whether the taint engine is to be used.
+  bool enabled=false;
+};
+
+typedef path_symex_taint_analysis_enginet taint_enginet;
+
+class path_symex_no_taint_analysis_enginet: public taint_enginet
+{
+
+// A dummy implementation of a taint engine that performs no taint analysis.
+public:
+
+  inline ~path_symex_no_taint_analysis_enginet()
+  {
+  }
+
+  const taintt get_bottom_elem() const;
+
+  taintt meet(irep_idt id, const taintt taint_1, const taintt taint_2) const;
+
+  const std::string get_taint_analysis_name() const;
+
+  taintt parse_taint(const std::string taint_name) const;
+
+  std::string get_taint_name(const taintt taint) const;
+
+};
+
+/*
+ *  An implementation of a simple taint engine with two states (tainted
+ *	and untainted).
+ */
+class path_symex_simple_taint_analysis_enginet: public taint_enginet
+{
+public:
+  static const taintt UNTAINTED=0;
+  static const taintt TAINTED=1;
+
+  inline ~path_symex_simple_taint_analysis_enginet()
+  {
+  }
+
+  const taintt get_bottom_elem() const;
+
+  taintt meet(irep_idt id, const taintt taint_1, const taintt taint_2) const;
+
+  const std::string get_taint_analysis_name() const;
+
+  taintt parse_taint(const std::string taint_name) const;
+
+  std::string get_taint_name(const taintt taint) const;
+};
+
+#endif
diff --git a/src/path-symex/path_symex_taint_data.cpp b/src/path-symex/path_symex_taint_data.cpp
new file mode 100644
index 00000000000..7d5903bd4c3
--- /dev/null
+++ b/src/path-symex/path_symex_taint_data.cpp
@@ -0,0 +1,164 @@
+/*******************************************************************
+ Module: Taint Data Module
+
+ Author: Daniel Neville, daniel.neville@cs.ox.ac.uk
+ John Galea,		john.galea@cs.ox.ac.uk
+
+ \*******************************************************************/
+
+#include "path_symex_taint_data.h"
+
+taint_datat::taint_rulet::taint_rulet()
+{
+  loc=0;
+  // 0 = TOP element, always.
+  taint=0;
+  symbol_flag=false;
+  symbol_name="";
+}
+
+/*******************************************************************
+
+ Function: taint_datat::taint_rulet::output
+
+ Inputs: Takes Output stream and taint engine.
+
+ Outputs: Returns nothing.
+
+ Purpose: Outputs to stream the specified rule.
+
+ \*******************************************************************/
+
+void taint_datat::taint_rulet::output(taint_enginet &taint_engine,
+    std::ostream &out) const
+{
+  out << "Location: " << loc;
+  if(symbol_flag)
+    out << ", symbol name: " << symbol_name;
+
+  out << " set to " << taint_engine.get_taint_name(taint);
+}
+
+taint_datat::taint_datat()
+{
+}
+;
+
+/*******************************************************************
+
+ Function: taint_datat::add
+
+ Inputs: The location where a given taint state is introduced.
+
+ Outputs: Nothing
+
+ Purpose: Registers a taint rule, normally parsed from the JSON file.
+
+ \*******************************************************************/
+
+void taint_datat::add(unsigned loc, taintt taint, bool symbol_flag,
+    irep_idt symbol_name)
+{
+  taint_rulet rule;
+  rule.loc=loc;
+  rule.taint=taint;
+  rule.symbol_name=symbol_name;
+  rule.symbol_flag=symbol_flag;
+  data[loc].push_back(rule);
+}
+
+/*******************************************************************
+
+ Function: taint_datat::check_rules
+
+ Inputs: Takes the locs of the program.
+
+ Outputs: Returns true in case a rule is invalid
+
+ Purpose: Checks specified taint introduction rules.
+
+ This is not intended to be a complete checker of rules.
+
+ \*******************************************************************/
+
+bool taint_datat::check_rules(locst &locs, std::ostream & warning,
+    taint_enginet &taint_engine)
+{
+  if(!taint_engine.enabled)
+    return false;
+
+  for (auto rule_vector : data)
+  {
+    for (auto rule : rule_vector.second)
+    {
+      // Check whether the rule is outside program.
+      if(rule.loc >= locs.size())
+      {
+        warning << "Following rule outside program scope:" << "\n";
+        rule.output(taint_engine, warning);
+        warning << "\n";
+        return true;
+      }
+
+      // Retrieve instruction.
+      goto_programt::const_targett inst=locs.loc_vector[rule.loc].target;
+
+      // Check that the instruction is supported.
+      if(!inst->is_assign() && !inst->is_decl() && !inst->is_function_call())
+      {
+
+        warning << "Following rule refers to an unsupported op (" << inst->type
+            << ")\n";
+        rule.output(taint_engine, warning);
+        warning << "\n";
+        return true;
+
+      }
+      else if(inst->is_function_call())
+      {
+        // Need to check that the left hand side of the function call exists.
+        code_function_callt function_call=to_code_function_call(inst->code);
+
+        if(function_call.lhs().is_nil())
+        {
+          warning
+              << "Following rule refers to function call with nil left-hand side:"
+              << "\n";
+          rule.output(taint_engine, warning);
+          warning << "\n";
+          return true;
+        }
+      }
+    }
+  }
+
+  // No errors found.
+  return false;
+}
+
+/*******************************************************************
+
+ Function: taint_datat::check_rules
+
+ Inputs: Takes Output stream.
+
+ Outputs: Returns nothing.
+
+ Purpose: Outputs to stream the specified rules.
+
+ \*******************************************************************/
+
+void taint_datat::output(std::ostream &out, taint_enginet &taint_engine) const
+{
+  int i=0;
+  for (auto rule_vector : data)
+  {
+    for (auto rule : rule_vector.second)
+    {
+      out << ++i << ": ";
+      rule.output(taint_engine, out);
+      out << "\n";
+    }
+  }
+}
+
diff --git a/src/path-symex/path_symex_taint_data.h b/src/path-symex/path_symex_taint_data.h
new file mode 100644
index 00000000000..a8e5b54cb38
--- /dev/null
+++ b/src/path-symex/path_symex_taint_data.h
@@ -0,0 +1,56 @@
+/*******************************************************************
+ Module: Taint Data Module
+
+ Author: Daniel Neville,	daniel.neville@cs.ox.ac.uk
+ John Galea,		john.galea@cs.ox.ac.uk
+
+ \*******************************************************************/
+
+#ifndef PATH_SYMEX_PATH_SYMEX_TAINT_DATA_H_
+#define PATH_SYMEX_PATH_SYMEX_TAINT_DATA_H_
+
+#include <path-symex/path_symex_taint_analysis.h>
+#include <map>
+#include <util/std_expr.h>
+
+class taint_datat
+{
+public:
+
+  // Defines a taint rule.
+  class taint_rulet
+  {
+  public:
+    // The location where taint is forced.  (Redundant.)
+    unsigned int loc;
+
+    // The taint state the force.
+    taintt taint;
+
+    // Modify a symbol, or just the LHS?
+    bool symbol_flag;
+
+    // The name of the symbol to be updated.
+    irep_idt symbol_name;
+
+    // Output a rule using the taint engine.
+    void output(taint_enginet &taint_engine, std::ostream &out) const;
+    // Defaults
+    taint_rulet();
+  };
+
+  taint_datat();
+
+  typedef std::map<unsigned, std::vector<taint_rulet> > datat;
+  datat data;
+
+  void add(unsigned loc, taintt taint, bool symbol_flag, irep_idt symbol_name);
+
+  bool check_rules(locst &locs, std::ostream & warning,
+      taint_enginet &taint_engine);
+
+  void output(std::ostream &out, taint_enginet &taint_engine) const;
+
+};
+
+#endif /* PATH_SYMEX_PATH_SYMEX_TAINT_DATA_H_ */
diff --git a/src/path-symex/path_symex_taint_parser.cpp b/src/path-symex/path_symex_taint_parser.cpp
new file mode 100644
index 00000000000..1fadfeb64d6
--- /dev/null
+++ b/src/path-symex/path_symex_taint_parser.cpp
@@ -0,0 +1,105 @@
+/*******************************************************************
+ Module: Taint Parser
+
+ Author: Daniel Neville,	daniel.neville@cs.ox.ac.uk
+ John Galea,		john.galea@cs.ox.ac.uk
+
+ \*******************************************************************/
+
+#include "path_symex_taint_parser.h"
+
+/*******************************************************************
+ Function: parse_taint_file
+
+ Inputs:  Takes file name of JSON and taint engine.
+ Stores parsed rules in taint_data.
+
+ Outputs: Returns true on parsing errors
+
+ Purpose: Parses JSON file and stores rules
+
+ \*******************************************************************/
+bool parse_taint_file(const std::string &file_name,
+    message_handlert &message_handler, taint_datat &taint_data,
+    taint_enginet &taint_engine)
+{
+  /* Format of JSON File.
+   Array of Objects.
+   Each Object:
+   loc: <Program location s.t. LHS is tainted>
+   taint: <Taint value>
+   symbol: <expanded symbol> (Optional)
+   */
+
+  jsont json;
+
+  // First parse the file.
+  if(parse_json(file_name, message_handler, json))
+  {
+    messaget message(message_handler);
+    message.error() << "Taint file is not a valid json file" << messaget::eom;
+    return true;
+  }
+
+  // Perform array check.
+  if(!json.is_array())
+  {
+    messaget message(message_handler);
+    message.error() << "expecting an array in the input location file, but got "
+        << json << messaget::eom;
+    return true;
+  }
+
+  for (jsont::arrayt::const_iterator it=json.array.begin();
+      it != json.array.end(); it++)
+  {
+    if(!it->is_object())
+    {
+      messaget message(message_handler);
+      message.error()
+          << "expecting an array of objects in the input location file, but got "
+          << *it << messaget::eom;
+      return true;
+    }
+
+    const std::string taint_string=(*it)["taint"].value;
+    const std::string loc_string=(*it)["loc"].value;
+    const std::string symbol_string=(*it)["symbol"].value;
+
+    taintt taint=0;
+    unsigned int loc=0;
+    irep_idt symbol_name="";
+    bool symbol_flag=false;
+
+    try
+    {
+      // TODO: Handle catch better.
+      taint=taint_engine.parse_taint(taint_string);
+    } catch (...)
+    {
+      messaget message(message_handler);
+      message.error() << "Taint type not recognised." << messaget::eom;
+    }
+
+    if(loc_string.empty())
+    {
+      messaget message(message_handler);
+      message.error() << "location must have \"unsigned int\"" << messaget::eom;
+      return true;
+    }
+    else
+    {
+      loc=safe_string2unsigned(std::string(loc_string, 0, std::string::npos));
+    }
+
+    if(!symbol_string.empty())
+    {
+      symbol_name=symbol_string;
+      symbol_flag=true;
+    }
+
+    taint_data.add(loc, taint, symbol_flag, symbol_name);
+  }
+
+  return false;
+}
diff --git a/src/path-symex/path_symex_taint_parser.h b/src/path-symex/path_symex_taint_parser.h
new file mode 100644
index 00000000000..9dfb3e3158d
--- /dev/null
+++ b/src/path-symex/path_symex_taint_parser.h
@@ -0,0 +1,25 @@
+/*******************************************************************
+ Module: Taint Parser
+
+ Author: Daniel Neville,	daniel.neville@cs.ox.ac.uk
+ John Galea,		john.galea@cs.ox.ac.uk
+
+ \*******************************************************************/
+
+#ifndef PATH_SYMEX_PATH_SYMEX_TAINT_PARSER_H_
+#define PATH_SYMEX_PATH_SYMEX_TAINT_PARSER_H_
+
+#include <ostream>
+#include <iostream>
+
+#include <util/string2int.h>
+
+#include <json/json_parser.h>
+#include <util/message.h>
+#include <path-symex/path_symex_taint_data.h>
+
+bool parse_taint_file(const std::string &file_name,
+    message_handlert &message_handler, taint_datat &taint_data,
+    taint_enginet &taint_engine);
+
+#endif /* PATH_SYMEX_PATH_SYMEX_TAINT_PARSER_H_ */
diff --git a/src/symex/Makefile b/src/symex/Makefile
index 1f8e27ce063..8dbc1159faf 100644
--- a/src/symex/Makefile
+++ b/src/symex/Makefile
@@ -10,6 +10,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../langapi/langapi$(LIBEXT) \
        ../xmllang/xmllang$(LIBEXT) \
        ../assembler/assembler$(LIBEXT) \
+       ../json/json$(LIBEXT) \
        ../solvers/solvers$(LIBEXT) \
        ../util/util$(LIBEXT) \
        ../goto-symex/adjust_float_expressions$(OBJEXT) \
diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp
index 0ae633e2e9f..979acfb1335 100644
--- a/src/symex/path_search.cpp
+++ b/src/symex/path_search.cpp
@@ -36,10 +36,16 @@ path_searcht::resultt path_searcht::operator()(
   
   locs.build(goto_functions);
 
-  // this is the container for the history-forest  
+  // Perform a non-comprehensive check on JSON file.
+  if(taint_engine->enabled &&
+      taint_data.check_rules(locs, warning(), *taint_engine)) {
+    warning() << "Rules inconsistent." << eom;
+  }
+
+  // This is the container for the history-forest
   path_symex_historyt history;
   
-  queue.push_back(initial_state(var_map, locs, history));
+  queue.push_back(initial_state(var_map, locs, history, *taint_engine));
   
   // set up the statistics
   number_of_dropped_states=0;
@@ -240,6 +246,24 @@ void path_searcht::pick_state()
 
 /*******************************************************************\
 
+Function: path_searcht::set_taint
+
+ Inputs: The taint engine, name of JSON file, and a flag denoting
+ 	 whether the taint engine is enabled.
+
+ Outputs: Nothing
+
+ Purpose: Sets initial information to perform taint analysis
+
+\*******************************************************************/
+void path_searcht::set_taint(const bool enabled, std::string file, taint_enginet &_taint_engine) {
+  taint_file = file;
+  taint_engine = &_taint_engine;
+  taint_engine->enabled = enabled;
+}
+
+/*******************************************************************\
+
 Function: path_searcht::do_show_vcc
 
   Inputs:
diff --git a/src/symex/path_search.h b/src/symex/path_search.h
index 8115fcc9090..979323c4c94 100644
--- a/src/symex/path_search.h
+++ b/src/symex/path_search.h
@@ -16,6 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <path-symex/path_symex_state.h>
 
+#include <json/json_parser.h>
+#include <path-symex/path_symex_taint_data.h>
+
 class path_searcht:public safety_checkert
 {
 public:
@@ -27,6 +30,7 @@ class path_searcht:public safety_checkert
     context_bound_set(false),
     unwind_limit_set(false),
     branch_bound_set(false),
+    taint_file(""),
     search_heuristic(search_heuristict::DFS)
   {
   }
@@ -58,6 +62,9 @@ class path_searcht:public safety_checkert
     unwind_limit=limit;
   }
 
+
+  void set_taint(const bool enabled, std::string file, taint_enginet &_taint_engine);
+
   bool show_vcc;
   bool eager_infeasibility;
   
@@ -95,6 +102,11 @@ class path_searcht:public safety_checkert
   typedef std::map<irep_idt, property_entryt> property_mapt;
   property_mapt property_map;
 
+  taint_enginet *taint_engine;
+  // This is the taint engine that will be used throughout analysis.
+  taint_datat taint_data;
+  // This is the specified data provided in the JSON file.
+
 protected:
   typedef path_symex_statet statet;
 
@@ -132,8 +144,10 @@ class path_searcht:public safety_checkert
   unsigned branch_bound;
   unsigned unwind_limit;
   bool depth_limit_set, context_bound_set, unwind_limit_set, branch_bound_set;
+  dstring taint_file;
 
   enum class search_heuristict { DFS, BFS, LOCS } search_heuristic;
+
 };
 
 #endif
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 2fbee65e2ad..5431c18f4e2 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -42,6 +42,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cbmc/version.h>
 
 #include <path-symex/locs.h>
+#include <path-symex/path_symex_taint_parser.h>
 
 #include "path_search.h"
 #include "symex_parse_options.h"
@@ -283,6 +284,20 @@ int symex_parse_optionst::doit()
       return 0;
     }
 
+    if(cmdline.isset("taint") && cmdline.get_value("taint") != "none")
+    {
+
+      if(handle_taint_analysis_option(path_search))
+        return 0;
+
+    }
+    else
+    {
+      path_symex_no_taint_analysis_enginet taint_engine;
+      path_search.set_taint(false, cmdline.get_value("taint-file"),
+          taint_engine);
+    }
+
     path_search.eager_infeasibility=
       cmdline.isset("eager-infeasibility");
       
@@ -490,6 +505,69 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
 
 /*******************************************************************\
 
+Function:  symex_parse_optionst::handle_taint_analysis_option
+
+ Inputs: Takes Path Search object to initialise taint engine.
+
+ Outputs: Returns an exit flag
+
+ Purpose: Handles taint option set via command-line
+
+ \*******************************************************************/
+bool symex_parse_optionst::handle_taint_analysis_option(
+    path_searcht &path_search)
+{
+
+  // Find which taint engine has been selected
+  if(cmdline.get_value("taint") == "simple")
+  {
+    /*path_symex_simple_taint_analysis_enginet taint_engine;
+
+     path_search.set_taint(true, cmdline.get_value("taint-file"), taint_engine);
+     */
+
+    // QUICK FIX FOR NOW!
+    path_symex_simple_taint_analysis_enginet *taint_engine=
+        new path_symex_simple_taint_analysis_enginet();
+    path_search.set_taint(true, cmdline.get_value("taint-file"), *taint_engine);
+
+  }
+  else
+  {
+    throw "Taint engine type not recognised.";
+  }
+
+  // Parse JSON file if it has been specified.
+  if(cmdline.isset("taint-file"))
+  {
+    if(parse_taint_file(cmdline.get_value("taint-file"), *message_handler,
+        path_search.taint_data, *path_search.taint_engine))
+    {
+      throw "Taint file invalid.\n";
+    }
+  }
+
+  // Point the taint engine to the data.
+  (path_search.taint_engine)->taint_data=&path_search.taint_data;
+
+  status() << "Using taint engine: "
+      << path_search.taint_engine->get_taint_analysis_name() << "  Found "
+      << path_search.taint_data.data.size()
+      << ((path_search.taint_data.data.size() == 1) ? " rule." : " rules.")
+      << eom;
+
+  if(cmdline.isset("show-taint-data"))
+  {
+    std::cout << "Taint data from JSON file:\n";
+    path_search.taint_data.output(std::cout, *path_search.taint_engine);
+    return true;
+  }
+
+  return false;
+}
+
+/*******************************************************************\
+
 Function: symex_parse_optionst::report_properties
 
   Inputs:
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index 8d27cd31bad..a88ae8b3e8f 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language_ui.h>
 
 #include "path_search.h"
+#include <path-symex/path_symex_taint_analysis.h>
 
 class goto_functionst;
 class optionst;
@@ -41,6 +42,7 @@ class optionst;
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(show-locs)(show-vcc)(show-properties)(show-goto-functions)" \
   "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \
+  "(taint):(show-taint-data)(taint-file):" \
   "(no-simplify)(no-unwinding-assertions)(no-propagation)"
   // the last line is for CBMC-regression testing only
 
@@ -70,6 +72,8 @@ class symex_parse_optionst:
             
   void eval_verbosity();
 
+  bool handle_taint_analysis_option(path_searcht &path_search);
+
   std::string get_test(const goto_tracet &goto_trace);
 };
 
diff --git a/src/util/irep_ids.txt b/src/util/irep_ids.txt
index 47fc59d1e90..7cab20adbdb 100644
--- a/src/util/irep_ids.txt
+++ b/src/util/irep_ids.txt
@@ -732,3 +732,6 @@ verilog_array
 low
 high
 bswap
+is_taint
+set_taint
+get_taint
\ No newline at end of file

From da0fb4221b8727028100578ee2079beebd3b60bc Mon Sep 17 00:00:00 2001
From: Daniel Neville <daniel.neville@cs.ox.ac.uk>
Date: Fri, 30 Sep 2016 17:24:42 +0100
Subject: [PATCH 4/9] Initial commit.  Largely working.

---
 src/goto-programs/Makefile           |   3 +-
 src/goto-programs/remove_ternary.cpp | 247 +++++++++++++++++++++++++++
 src/goto-programs/remove_ternary.h   |  47 +++++
 3 files changed, 296 insertions(+), 1 deletion(-)
 create mode 100644 src/goto-programs/remove_ternary.cpp
 create mode 100644 src/goto-programs/remove_ternary.h

diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index 0b0119112f2..97711ed09cb 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -16,7 +16,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \
       remove_returns.cpp osx_fat_reader.cpp remove_complex.cpp \
       goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \
       graphml_goto_trace.cpp remove_virtual_functions.cpp \
-      class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp
+      class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp \
+      remove_ternary.cpp
 
 INCLUDES= -I ..
 
diff --git a/src/goto-programs/remove_ternary.cpp b/src/goto-programs/remove_ternary.cpp
new file mode 100644
index 00000000000..d20e4f9e54c
--- /dev/null
+++ b/src/goto-programs/remove_ternary.cpp
@@ -0,0 +1,247 @@
+/*******************************************************************\
+
+Module: Remove ternaries by rewritting into IFs.
+
+Author: Daniel Neville
+
+Date:   September 2016
+
+\*******************************************************************/
+
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+#include <util/i2string.h>
+#include <util/replace_expr.h>
+#include <iostream>
+
+#include "remove_ternary.h"
+
+
+/*******************************************************************\
+
+Function:
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+bool remove_ternaryt::contains_ternary(
+    exprt &expr)
+{
+  bool contains=false;
+  contains_ternary(expr, contains);
+  return contains;
+}
+
+/*******************************************************************\
+
+Function:
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+void remove_ternaryt::contains_ternary(
+    exprt &expr,
+    bool &contains)
+{
+  if(contains || !expr.has_operands())
+    return;
+
+  if(expr.id() == ID_if) {
+    contains = true;
+    return;
+  }
+
+  Forall_operands(it, expr) {
+    contains_ternary(*it, contains);
+  }
+}
+
+/*******************************************************************\
+
+Function:
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+void remove_ternaryt::replace_ternary(
+    goto_programt &goto_program,
+    goto_programt::instructionst::iterator &i_it,
+    exprt &expr)
+{
+  if(!expr.has_operands()) // Ternary MUST have operands by definition.
+    return;
+
+  if(expr.id() == ID_code) {
+    codet &code = to_code(expr);
+    if(to_code(expr).get_statement()==ID_assign) {
+      code_assignt &code_assign = to_code_assign(code);
+      replace_ternary(goto_program, i_it, code_assign.rhs());
+      return;
+    }
+    // Avoid ternary on LHS.  For now.  They are awfully unreadable anyway.
+  }
+
+  if(expr.id() == ID_if)
+  {
+    Forall_operands(it, expr)
+    {
+      if(contains_ternary(*it))
+        replace_ternary(goto_program, i_it, *it);
+    }
+
+    if_exprt &if_expr=to_if_expr(expr); // Some short hands.
+
+    /* 1  (...) cond : T : F (...)
+     ->
+     1  decl tmp_x;
+     2  if !cond GOTO false_case_x
+     3  tmp_x = T
+     4  GOTO end_x
+     6  false_case_x:  tmp_x = F
+     7  end_x: (...) tmp_x (...)
+     */
+
+    auxiliary_symbolt new_symbol;
+    symbolt *symbol_ptr;
+
+    do
+    {
+      new_symbol.base_name="tmp_ternary$" + i2string(++replaced);
+      new_symbol.name="ternary" + id2string(new_symbol.base_name);
+      new_symbol.type=if_expr.true_case().type();
+      new_symbol.location=i_it->source_location;
+    } while (symbol_table.move(new_symbol, symbol_ptr));
+
+    goto_programt::targett decl_instruction=goto_program.insert_before(i_it);
+    goto_programt::targett guarded_goto_instruction=goto_program.insert_before(
+        i_it);
+    goto_programt::targett true_instruction=goto_program.insert_before(i_it);
+    goto_programt::targett unguarded_goto_instruction=
+        goto_program.insert_before(i_it);
+    goto_programt::targett false_instruction=goto_program.insert_before(i_it);
+
+    code_declt decl;
+    decl.symbol()=symbol_ptr->symbol_expr();
+    decl.add_source_location()=i_it->source_location;
+    decl_instruction->make_decl();
+    decl_instruction->code=decl;
+
+    code_gotot guarded_goto;
+    guarded_goto_instruction->make_goto();
+    guarded_goto_instruction->code=guarded_goto;
+    guarded_goto_instruction->guard=not_exprt(if_expr.cond());
+    guarded_goto_instruction->targets.push_back(false_instruction);
+
+    code_assignt assign_true;
+    assign_true.lhs()=symbol_ptr->symbol_expr();
+    assign_true.rhs()=if_expr.true_case();
+    assign_true.add_source_location()=i_it->source_location;
+    true_instruction->make_assignment();
+    true_instruction->code=assign_true;
+
+    code_gotot unguarded_goto;
+    unguarded_goto_instruction->make_goto();
+    unguarded_goto_instruction->code=unguarded_goto;
+    unguarded_goto_instruction->guard=true_exprt();
+    unguarded_goto_instruction->targets.push_back(i_it);
+
+    code_assignt assign_false;
+    assign_false.lhs()=symbol_ptr->symbol_expr();
+    assign_false.rhs()=if_expr.false_case();
+    assign_false.add_source_location()=i_it->source_location;
+    false_instruction->make_assignment();
+    false_instruction->code=assign_false;
+
+    expr=symbol_ptr->symbol_expr();
+
+    return; // We've handled operands.
+  }
+
+  /* If it isn't an IF statement, let's look at its operands. */
+  Forall_operands(it, expr) {
+    replace_ternary(goto_program, i_it, *it);
+  }
+}
+
+/*******************************************************************\
+
+Function: remove_returnst::operator()
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+void remove_ternaryt::operator()(goto_functionst &goto_functions)
+{
+  Forall_goto_functions(f_it, goto_functions) {
+
+    goto_programt &goto_program=f_it->second.body;
+
+    if(goto_program.empty())
+    return;
+
+    Forall_goto_program_instructions(i_it, goto_program)
+        replace_ternary(goto_program, i_it, i_it->code);
+  }
+
+  goto_functions.update();
+}
+
+/*******************************************************************\
+
+Function: remove_returns
+
+Inputs:
+
+Outputs:
+
+Purpose: removes returns
+
+\*******************************************************************/
+
+void remove_ternary(
+  symbol_tablet &symbol_table,
+  goto_functionst &goto_functions)
+{
+  remove_ternaryt rt(symbol_table);
+  rt(goto_functions);
+}
+
+/*******************************************************************\
+
+Function: remove_returns
+
+Inputs:
+
+Outputs:
+
+Purpose: removes returns
+
+\*******************************************************************/
+
+void remove_ternary(goto_modelt &goto_model)
+{
+  remove_ternaryt rt(goto_model.symbol_table);
+  rt(goto_model.goto_functions);
+}
+
diff --git a/src/goto-programs/remove_ternary.h b/src/goto-programs/remove_ternary.h
new file mode 100644
index 00000000000..e41a9a3f8e7
--- /dev/null
+++ b/src/goto-programs/remove_ternary.h
@@ -0,0 +1,47 @@
+/*******************************************************************\
+
+Module: Remove function returns
+
+Author: Daniel Kroening
+
+Date:   September 2009
+
+\*******************************************************************/
+
+#ifndef CPROVER_REMOVE_TERNARY_H
+#define CPROVER_REMOVE_TERNARY_H
+
+#include <goto-programs/goto_model.h>
+
+class remove_ternaryt
+{
+public:
+  explicit remove_ternaryt(symbol_tablet &_symbol_table):
+    symbol_table(_symbol_table)
+  {
+  }
+
+  void operator()(
+    goto_functionst &goto_functions);
+
+protected:
+  symbol_tablet &symbol_table;
+
+  unsigned int replaced = 0;
+
+  void replace_ternary(
+      goto_programt &goto_program,
+      goto_programt::instructionst::iterator &i_it,
+          exprt &expr);
+
+  void contains_ternary(exprt &expr, bool &contains);
+
+  bool contains_ternary(exprt &expr);
+};
+
+
+void remove_ternary(symbol_tablet &, goto_functionst &);
+
+void remove_ternary(goto_modelt &);
+
+#endif

From 18e91d504ad29e149459af700b34ec797244681a Mon Sep 17 00:00:00 2001
From: Daniel Neville <daniel.neville@cs.ox.ac.uk>
Date: Fri, 30 Sep 2016 17:27:29 +0100
Subject: [PATCH 5/9] Re-ordered recursion.

---
 src/goto-programs/remove_ternary.cpp | 69 +++-------------------------
 1 file changed, 7 insertions(+), 62 deletions(-)

diff --git a/src/goto-programs/remove_ternary.cpp b/src/goto-programs/remove_ternary.cpp
index d20e4f9e54c..2c4de160a71 100644
--- a/src/goto-programs/remove_ternary.cpp
+++ b/src/goto-programs/remove_ternary.cpp
@@ -18,55 +18,6 @@ Date:   September 2016
 #include "remove_ternary.h"
 
 
-/*******************************************************************\
-
-Function:
-
-Inputs:
-
-Outputs:
-
-Purpose:
-
-\*******************************************************************/
-
-bool remove_ternaryt::contains_ternary(
-    exprt &expr)
-{
-  bool contains=false;
-  contains_ternary(expr, contains);
-  return contains;
-}
-
-/*******************************************************************\
-
-Function:
-
-Inputs:
-
-Outputs:
-
-Purpose:
-
-\*******************************************************************/
-
-void remove_ternaryt::contains_ternary(
-    exprt &expr,
-    bool &contains)
-{
-  if(contains || !expr.has_operands())
-    return;
-
-  if(expr.id() == ID_if) {
-    contains = true;
-    return;
-  }
-
-  Forall_operands(it, expr) {
-    contains_ternary(*it, contains);
-  }
-}
-
 /*******************************************************************\
 
 Function:
@@ -97,14 +48,15 @@ void remove_ternaryt::replace_ternary(
     // Avoid ternary on LHS.  For now.  They are awfully unreadable anyway.
   }
 
-  if(expr.id() == ID_if)
+  Forall_operands(it, expr)
   {
-    Forall_operands(it, expr)
-    {
-      if(contains_ternary(*it))
-        replace_ternary(goto_program, i_it, *it);
-    }
+      replace_ternary(goto_program, i_it, *it);
+      // Go through sub-tree first.
+  }
 
+  // If we are on an IF statement.
+  if(expr.id() == ID_if)
+  {
     if_exprt &if_expr=to_if_expr(expr); // Some short hands.
 
     /* 1  (...) cond : T : F (...)
@@ -169,13 +121,6 @@ void remove_ternaryt::replace_ternary(
     false_instruction->code=assign_false;
 
     expr=symbol_ptr->symbol_expr();
-
-    return; // We've handled operands.
-  }
-
-  /* If it isn't an IF statement, let's look at its operands. */
-  Forall_operands(it, expr) {
-    replace_ternary(goto_program, i_it, *it);
   }
 }
 

From 105850370f019290242a67d2b7c8e6e03c0eeb26 Mon Sep 17 00:00:00 2001
From: Daniel Neville <daniel.neville@cs.ox.ac.uk>
Date: Fri, 30 Sep 2016 17:27:54 +0100
Subject: [PATCH 6/9] Add hook into symex.

---
 src/symex/symex_parse_options.cpp | 5 +++++
 src/symex/symex_parse_options.h   | 1 +
 2 files changed, 6 insertions(+)

diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 5431c18f4e2..8a26ce0f948 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -32,6 +32,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/remove_ternary.h>
+
 
 #include <goto-instrument/cover.h>
 
@@ -422,6 +424,9 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     remove_vector(goto_model);
     remove_virtual_functions(goto_model);
     
+    if(cmdline.isset("remove-ternary"))
+      remove_ternary(goto_model);
+
     // recalculate numbers, etc.
     goto_model.goto_functions.update();
 
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index a88ae8b3e8f..109c36ace25 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -43,6 +43,7 @@ class optionst;
   "(show-locs)(show-vcc)(show-properties)(show-goto-functions)" \
   "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \
   "(taint):(show-taint-data)(taint-file):" \
+  "(remove-ternary)" \
   "(no-simplify)(no-unwinding-assertions)(no-propagation)"
   // the last line is for CBMC-regression testing only
 

From c2639103b2bbb2679b59a834beccf04ceae28c83 Mon Sep 17 00:00:00 2001
From: Daniel Neville <daniel.neville@cs.ox.ac.uk>
Date: Fri, 30 Sep 2016 22:06:39 +0100
Subject: [PATCH 7/9] Supports LHS ternary.

---
 src/goto-programs/remove_ternary.cpp | 44 ++++++++++++++++++++--------
 src/goto-programs/remove_ternary.h   |  3 +-
 2 files changed, 33 insertions(+), 14 deletions(-)

diff --git a/src/goto-programs/remove_ternary.cpp b/src/goto-programs/remove_ternary.cpp
index 2c4de160a71..113a56637eb 100644
--- a/src/goto-programs/remove_ternary.cpp
+++ b/src/goto-programs/remove_ternary.cpp
@@ -20,11 +20,15 @@ Date:   September 2016
 
 /*******************************************************************\
 
-Function:
+Function:  Replace ternary
 
-Inputs:
+Inputs:  Takes:
+  - A Goto Program, used to insert new instructions.
+  - A specific instruction, used to know the current location
+  in the program.
+  - The current expr, analysed recursively.
 
-Outputs:
+Outputs:  Modified instruction.
 
 Purpose:
 
@@ -33,16 +37,24 @@ Date:   September 2016
 void remove_ternaryt::replace_ternary(
     goto_programt &goto_program,
     goto_programt::instructionst::iterator &i_it,
-    exprt &expr)
+    exprt &expr,
+    bool lhs)
 {
   if(!expr.has_operands()) // Ternary MUST have operands by definition.
     return;
 
+  /* LHS handles ternary when used on the LHS of an assignment
+   * operator.  LHS = false is used whenever the ternary is simply
+   * part of an arbitrary condition.
+   */
+
   if(expr.id() == ID_code) {
     codet &code = to_code(expr);
     if(to_code(expr).get_statement()==ID_assign) {
       code_assignt &code_assign = to_code_assign(code);
-      replace_ternary(goto_program, i_it, code_assign.rhs());
+
+      replace_ternary(goto_program, i_it, code_assign.lhs(), true);
+      replace_ternary(goto_program, i_it, code_assign.rhs(), false);
       return;
     }
     // Avoid ternary on LHS.  For now.  They are awfully unreadable anyway.
@@ -50,7 +62,7 @@ void remove_ternaryt::replace_ternary(
 
   Forall_operands(it, expr)
   {
-      replace_ternary(goto_program, i_it, *it);
+      replace_ternary(goto_program, i_it, *it, lhs);
       // Go through sub-tree first.
   }
 
@@ -77,6 +89,8 @@ void remove_ternaryt::replace_ternary(
       new_symbol.base_name="tmp_ternary$" + i2string(++replaced);
       new_symbol.name="ternary" + id2string(new_symbol.base_name);
       new_symbol.type=if_expr.true_case().type();
+      if(lhs)
+        new_symbol.type=pointer_typet(new_symbol.type);
       new_symbol.location=i_it->source_location;
     } while (symbol_table.move(new_symbol, symbol_ptr));
 
@@ -105,7 +119,6 @@ void remove_ternaryt::replace_ternary(
     assign_true.rhs()=if_expr.true_case();
     assign_true.add_source_location()=i_it->source_location;
     true_instruction->make_assignment();
-    true_instruction->code=assign_true;
 
     code_gotot unguarded_goto;
     unguarded_goto_instruction->make_goto();
@@ -121,6 +134,15 @@ void remove_ternaryt::replace_ternary(
     false_instruction->code=assign_false;
 
     expr=symbol_ptr->symbol_expr();
+
+    if(lhs) {
+      expr=dereference_exprt(expr);
+      assign_true.rhs()=address_of_exprt(assign_true.rhs());
+      assign_false.rhs()=address_of_exprt(assign_false.rhs());
+    }
+
+    true_instruction->code=assign_true;
+    false_instruction->code=assign_false;
   }
 }
 
@@ -139,14 +161,10 @@ Function: remove_returnst::operator()
 void remove_ternaryt::operator()(goto_functionst &goto_functions)
 {
   Forall_goto_functions(f_it, goto_functions) {
-
-    goto_programt &goto_program=f_it->second.body;
-
-    if(goto_program.empty())
-    return;
+   goto_programt &goto_program=f_it->second.body;
 
     Forall_goto_program_instructions(i_it, goto_program)
-        replace_ternary(goto_program, i_it, i_it->code);
+        replace_ternary(goto_program, i_it, i_it->code, false);
   }
 
   goto_functions.update();
diff --git a/src/goto-programs/remove_ternary.h b/src/goto-programs/remove_ternary.h
index e41a9a3f8e7..8545dcae1e2 100644
--- a/src/goto-programs/remove_ternary.h
+++ b/src/goto-programs/remove_ternary.h
@@ -32,7 +32,8 @@ class remove_ternaryt
   void replace_ternary(
       goto_programt &goto_program,
       goto_programt::instructionst::iterator &i_it,
-          exprt &expr);
+          exprt &expr,
+          bool lhs);
 
   void contains_ternary(exprt &expr, bool &contains);
 

From 063d2ef194cf107a352ba67a0ceadd50833a3ced Mon Sep 17 00:00:00 2001
From: John Galea <john.galea.10@gmail.com>
Date: Mon, 3 Oct 2016 14:36:11 +0100
Subject: [PATCH 8/9] Comment Refactor

---
 .../ternary-taint-inline/main.c               | 24 +++++++++++++++++++
 .../ternary-untaint-inline/main.c             | 24 +++++++++++++++++++
 src/goto-programs/remove_ternary.cpp          | 16 +++++++------
 src/goto-programs/remove_ternary.h            |  4 +---
 4 files changed, 58 insertions(+), 10 deletions(-)
 create mode 100644 regression/symex-taint-analysis/ternary-taint-inline/main.c
 create mode 100644 regression/symex-taint-analysis/ternary-untaint-inline/main.c

diff --git a/regression/symex-taint-analysis/ternary-taint-inline/main.c b/regression/symex-taint-analysis/ternary-taint-inline/main.c
new file mode 100644
index 00000000000..0248c654815
--- /dev/null
+++ b/regression/symex-taint-analysis/ternary-taint-inline/main.c
@@ -0,0 +1,24 @@
+#include <assert.h>
+
+struct name{
+   int a;
+   float b;
+};
+int main(){
+
+	int x;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	int y = 1;
+
+	int z = 0;
+
+	int c =  (z != y) ? x : y;
+
+	assert(__CPROVER_is_taint("main::1::c", "tainted"));
+	assert(__CPROVER_is_taint("main::1::x", "tainted"));
+	assert(__CPROVER_is_taint("main::1::y", "untainted"));
+
+    return 0;
+}
diff --git a/regression/symex-taint-analysis/ternary-untaint-inline/main.c b/regression/symex-taint-analysis/ternary-untaint-inline/main.c
new file mode 100644
index 00000000000..97aba192546
--- /dev/null
+++ b/regression/symex-taint-analysis/ternary-untaint-inline/main.c
@@ -0,0 +1,24 @@
+#include <assert.h>
+
+struct name{
+   int a;
+   float b;
+};
+int main(){
+
+	int x;
+
+	__CPROVER_set_taint("main::1::x", "tainted");
+
+	int y = 1;
+
+	int z = 0;
+
+	int c =  (z == y) ? x : y;
+
+	assert(__CPROVER_is_taint("main::1::c", "untainted"));
+	assert(__CPROVER_is_taint("main::1::c", "untainted"));
+	assert(__CPROVER_is_taint("main::1::y", "untainted"));
+
+    return 0;
+}
diff --git a/src/goto-programs/remove_ternary.cpp b/src/goto-programs/remove_ternary.cpp
index 113a56637eb..cdaa7162290 100644
--- a/src/goto-programs/remove_ternary.cpp
+++ b/src/goto-programs/remove_ternary.cpp
@@ -40,7 +40,9 @@ void remove_ternaryt::replace_ternary(
     exprt &expr,
     bool lhs)
 {
-  if(!expr.has_operands()) // Ternary MUST have operands by definition.
+
+  // Ternary MUST have operands by definition.
+  if(!expr.has_operands())
     return;
 
   /* LHS handles ternary when used on the LHS of an assignment
@@ -57,7 +59,6 @@ void remove_ternaryt::replace_ternary(
       replace_ternary(goto_program, i_it, code_assign.rhs(), false);
       return;
     }
-    // Avoid ternary on LHS.  For now.  They are awfully unreadable anyway.
   }
 
   Forall_operands(it, expr)
@@ -148,7 +149,7 @@ void remove_ternaryt::replace_ternary(
 
 /*******************************************************************\
 
-Function: remove_returnst::operator()
+Function: remove_ternaryt::operator()(goto_functionst &goto_functions)
 
 Inputs:
 
@@ -172,13 +173,14 @@ void remove_ternaryt::operator()(goto_functionst &goto_functions)
 
 /*******************************************************************\
 
-Function: remove_returns
+Function: remove_ternary(symbol_tablet &symbol_table,
+goto_functionst &goto_functions)
 
 Inputs:
 
 Outputs:
 
-Purpose: removes returns
+Purpose:
 
 \*******************************************************************/
 
@@ -192,13 +194,13 @@ void remove_ternary(
 
 /*******************************************************************\
 
-Function: remove_returns
+Function: remove_ternary(goto_modelt &goto_model)
 
 Inputs:
 
 Outputs:
 
-Purpose: removes returns
+Purpose:
 
 \*******************************************************************/
 
diff --git a/src/goto-programs/remove_ternary.h b/src/goto-programs/remove_ternary.h
index 8545dcae1e2..293503481aa 100644
--- a/src/goto-programs/remove_ternary.h
+++ b/src/goto-programs/remove_ternary.h
@@ -21,8 +21,7 @@ class remove_ternaryt
   {
   }
 
-  void operator()(
-    goto_functionst &goto_functions);
+  void operator()(goto_functionst &goto_functions);
 
 protected:
   symbol_tablet &symbol_table;
@@ -40,7 +39,6 @@ class remove_ternaryt
   bool contains_ternary(exprt &expr);
 };
 
-
 void remove_ternary(symbol_tablet &, goto_functionst &);
 
 void remove_ternary(goto_modelt &);

From fc743bb08d91a308ad9cb27038736f7c74e4619c Mon Sep 17 00:00:00 2001
From: Daniel Neville <daniel.neville@cs.ox.ac.uk>
Date: Tue, 4 Oct 2016 12:49:23 +0100
Subject: [PATCH 9/9] Comments.

---
 src/goto-programs/remove_ternary.cpp | 130 +++++++++++++--------------
 1 file changed, 65 insertions(+), 65 deletions(-)

diff --git a/src/goto-programs/remove_ternary.cpp b/src/goto-programs/remove_ternary.cpp
index cdaa7162290..4af295c10ca 100644
--- a/src/goto-programs/remove_ternary.cpp
+++ b/src/goto-programs/remove_ternary.cpp
@@ -1,12 +1,13 @@
-/*******************************************************************\
+/*******************************************************************
 
-Module: Remove ternaries by rewritting into IFs.
+ Module: Remove ternaries by rewritting into IFs.
 
-Author: Daniel Neville
+ Author: Daniel Neville.
+         John Galea.
 
-Date:   September 2016
+ Date:   September 2016
 
-\*******************************************************************/
+ \*******************************************************************/
 
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
@@ -17,54 +18,56 @@ Date:   September 2016
 
 #include "remove_ternary.h"
 
+/*******************************************************************
+ Function:  Replace ternary
 
-/*******************************************************************\
+ Inputs:  Takes:
+ - A Goto Program, used to insert new instructions.
+ - A specific instruction, used to know the current location
+ in the program.  This is handled using pointer introduction.
+ - Ternaries on the LHS are generally of poor readability and
+ are avoided by many developers.
+ - The current expr, analysed recursively.
 
-Function:  Replace ternary
+ Outputs:  Modified instruction.
 
-Inputs:  Takes:
-  - A Goto Program, used to insert new instructions.
-  - A specific instruction, used to know the current location
-  in the program.
-  - The current expr, analysed recursively.
+ Purpose:
 
-Outputs:  Modified instruction.
+ \*******************************************************************/
 
-Purpose:
-
-\*******************************************************************/
-
-void remove_ternaryt::replace_ternary(
-    goto_programt &goto_program,
-    goto_programt::instructionst::iterator &i_it,
-    exprt &expr,
-    bool lhs)
+void remove_ternaryt::replace_ternary(goto_programt &goto_program,
+    goto_programt::instructionst::iterator &i_it, exprt &expr, bool lhs)
 {
 
-  // Ternary MUST have operands by definition.
+  // Ternary must have operands by definition.
   if(!expr.has_operands())
     return;
 
   /* LHS handles ternary when used on the LHS of an assignment
-   * operator.  LHS = false is used whenever the ternary is simply
-   * part of an arbitrary condition.
+   * operator.
+   * LHS = false is used whenever the ternary is simply
+   * part of an arbitrary condition (including all RHS)
    */
 
-  if(expr.id() == ID_code) {
-    codet &code = to_code(expr);
-    if(to_code(expr).get_statement()==ID_assign) {
-      code_assignt &code_assign = to_code_assign(code);
+  if(expr.id() == ID_code)
+  {
+    codet &code=to_code(expr);
+    if(to_code(expr).get_statement() == ID_assign)
+    {
+      code_assignt &code_assign=to_code_assign(code);
 
       replace_ternary(goto_program, i_it, code_assign.lhs(), true);
       replace_ternary(goto_program, i_it, code_assign.rhs(), false);
+
       return;
     }
   }
 
   Forall_operands(it, expr)
   {
-      replace_ternary(goto_program, i_it, *it, lhs);
-      // Go through sub-tree first.
+    // Go through sub-tree first.
+    // This allows parsing the expr-tree leaf first.
+    replace_ternary(goto_program, i_it, *it, lhs);
   }
 
   // If we are on an IF statement.
@@ -73,13 +76,13 @@ void remove_ternaryt::replace_ternary(
     if_exprt &if_expr=to_if_expr(expr); // Some short hands.
 
     /* 1  (...) cond : T : F (...)
-     ->
+     -> (where x is some integer)
      1  decl tmp_x;
      2  if !cond GOTO false_case_x
      3  tmp_x = T
      4  GOTO end_x
      6  false_case_x:  tmp_x = F
-     7  end_x: (...) tmp_x (...)
+     7  end_x: (...) tmp_x (...) // replace ternary with tmp_x
      */
 
     auxiliary_symbolt new_symbol;
@@ -136,7 +139,8 @@ void remove_ternaryt::replace_ternary(
 
     expr=symbol_ptr->symbol_expr();
 
-    if(lhs) {
+    if(lhs)
+    {
       expr=dereference_exprt(expr);
       assign_true.rhs()=address_of_exprt(assign_true.rhs());
       assign_false.rhs()=address_of_exprt(assign_false.rhs());
@@ -147,62 +151,58 @@ void remove_ternaryt::replace_ternary(
   }
 }
 
-/*******************************************************************\
+/*******************************************************************
+ Function: remove_ternaryt::operator()(goto_functionst &goto_functions)
 
-Function: remove_ternaryt::operator()(goto_functionst &goto_functions)
+ Inputs:
 
-Inputs:
+ Outputs:
 
-Outputs:
+ Purpose:
 
-Purpose:
-
-\*******************************************************************/
+ \*******************************************************************/
 
 void remove_ternaryt::operator()(goto_functionst &goto_functions)
 {
-  Forall_goto_functions(f_it, goto_functions) {
-   goto_programt &goto_program=f_it->second.body;
-
-    Forall_goto_program_instructions(i_it, goto_program)
-        replace_ternary(goto_program, i_it, i_it->code, false);
-  }
+  Forall_goto_functions(f_it, goto_functions){
+  goto_programt &goto_program=f_it->second.body;
 
-  goto_functions.update();
+  Forall_goto_program_instructions(i_it, goto_program)
+  replace_ternary(goto_program, i_it, i_it->code, false);
 }
 
-/*******************************************************************\
+goto_functions.update();
+}
 
-Function: remove_ternary(symbol_tablet &symbol_table,
-goto_functionst &goto_functions)
+/*******************************************************************
+ Function: remove_ternary(symbol_tablet &symbol_table,
+ goto_functionst &goto_functions)
 
-Inputs:
+ Inputs:
 
-Outputs:
+ Outputs:
 
-Purpose:
+ Purpose:
 
-\*******************************************************************/
+ \*******************************************************************/
 
-void remove_ternary(
-  symbol_tablet &symbol_table,
-  goto_functionst &goto_functions)
+void remove_ternary(symbol_tablet &symbol_table,
+    goto_functionst &goto_functions)
 {
   remove_ternaryt rt(symbol_table);
   rt(goto_functions);
 }
 
-/*******************************************************************\
-
-Function: remove_ternary(goto_modelt &goto_model)
+/*******************************************************************
+ Function: remove_ternary(goto_modelt &goto_model)
 
-Inputs:
+ Inputs:
 
-Outputs:
+ Outputs:
 
-Purpose:
+ Purpose:
 
-\*******************************************************************/
+ \*******************************************************************/
 
 void remove_ternary(goto_modelt &goto_model)
 {