Coverage

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

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

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

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

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

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]);
+  }
+}

regression/cbmc-cover/condition1/test.desc

@@ -3,16 +3,16 @@ main.c
 --cover condition
 ^EXIT=0$
 ^SIGNAL=0$
+^\[coverage.1] file main.c line 8 condition .* false: SATISFIED
+^\[coverage.2] file main.c line 8 condition .* true: SATISFIED
 ^\[main.coverage.1] file main.c line 8 function main condition .* false: SATISFIED
 ^\[main.coverage.2] file main.c line 8 function main condition .* true: SATISFIED
-^\[main.coverage.3] file main.c line 8 function main condition .* false: SATISFIED
-^\[main.coverage.4] file main.c line 8 function main condition .* true: SATISFIED
-^\[main.coverage.5] file main.c line 11 function main condition .* false: SATISFIED
-^\[main.coverage.6] file main.c line 11 function main condition .* true: SATISFIED
-^\[main.coverage.7] file main.c line 14 function main condition .* false: SATISFIED
-^\[main.coverage.8] file main.c line 14 function main condition .* true: SATISFIED
-^\[main.coverage.9] file main.c line 16 function main condition .* false: FAILED
-^\[main.coverage.10] file main.c line 16 function main condition .* true: SATISFIED
+^\[main.coverage.3] file main.c line 11 function main condition .* false: SATISFIED
+^\[main.coverage.4] file main.c line 11 function main condition .* true: SATISFIED
+^\[main.coverage.5] file main.c line 14 function main condition .* false: SATISFIED
+^\[main.coverage.6] file main.c line 14 function main condition .* true: SATISFIED
+^\[main.coverage.7] file main.c line 16 function main condition .* false: FAILED
+^\[main.coverage.8] file main.c line 16 function main condition .* true: SATISFIED
 ^\*\* 9 of 10 covered (90.0%)
 --
 ^warning: ignoring

regression/cbmc-cover/consider_goals1/if_icmp1.java

@@ -0,0 +1,31 @@
+class if_icmp1
+{
+  private static void f() {
+    int i = 10;
+    int j = 11;
+    if (i == j) {
+      assert false;
+    }
+    if (i >= j) {
+      assert false;
+    }
+    if (j > i) {
+      assert true;
+    } else {
+      assert false;
+    }
+    if (j <= i) {
+      assert false;
+    }
+    if (j < i) {
+      assert false;
+    } else {
+      assert true;
+    }
+  }
+
+  public static void main(String[] args)
+  {
+    f();
+  }
+}

regression/cbmc-cover/consider_goals1/test.desc

@@ -0,0 +1,8 @@
+CORE
+if_icmp1.class
+--cover location --no-trivial-tests
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 12 of 27 covered (44.4%)
+--
+^warning: ignoring