enable assertions in is_threadedt

Author: danpoe

regression/goto-analyzer/constant_propagation_01/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/constant_propagation_01/test.desc

@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_02/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/constant_propagation_02/test.desc

@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_03/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/constant_propagation_04/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/constant_propagation_05/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/constant_propagation_06/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/constant_propagation_06/test.desc

@@ -3,6 +3,6 @@ main.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 12 function main, assertion i<51: Unknown$
+^\[main.assertion.1\] file main.c line 11 function main, assertion i\s*<\s*51: Unknown$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_07/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   signed int i;

regression/goto-analyzer/constant_propagation_08/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int a[2];

regression/goto-analyzer/constant_propagation_09/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int a[2]={0,0};

regression/goto-analyzer/constant_propagation_10/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int a[2]={0,0};

regression/goto-analyzer/constant_propagation_11/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int a[2]={0,0};

regression/goto-analyzer/constant_propagation_12/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int i=0, y;

regression/goto-analyzer/constant_propagation_13/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int i=0, y;

regression/goto-analyzer/constant_propagation_14/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int a[2]={0,0};

regression/goto-analyzer/constant_propagation_15/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 int main()
 {
   int a[2]={0,0};

regression/goto-analyzer/constant_propagation_17/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<50) 
+  {
+    i++;
+    j++;
+  }
+  assert(i<51);
+}
+

regression/goto-analyzer/constant_propagation_17/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--constants --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file main.c line 12 function main, assertion i\s*<\s*51: (Unknown|Failure \(if reachable\))$
+--
+^warning: ignoring

regression/goto-analyzer/intervals_01/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/intervals_01/test.desc

@@ -3,13 +3,13 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 8 function main, assertion i>=10: Success$
-^\[main.assertion.2\] file main.c line 11 function main, assertion i!=30: Success$
-^\[main.assertion.3\] file main.c line 14 function main, assertion i!=15: Unknown$
-^\[main.assertion.4\] file main.c line 17 function main, assertion 0: Success$
-^\[main.assertion.5\] file main.c line 20 function main, assertion j>=10: Success$
-^\[main.assertion.6\] file main.c line 23 function main, assertion i>=j: Unknown$
-^\[main.assertion.7\] file main.c line 26 function main, assertion i>=11: Success$
-^\[main.assertion.8\] file main.c line 29 function main, assertion j<100: Success$
+^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: Success$
+^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: Success$
+^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: Unknown$
+^\[main.assertion.4\] file main.c line 16 function main, assertion 0: Success$
+^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: Success$
+^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: Unknown$
+^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: Success$
+^\[main.assertion.8]\ file main.c line 28 function main, assertion j\s*<\s*100: Success$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_02/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main(){
   int x;

regression/goto-analyzer/intervals_03/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main(){
   int x;

regression/goto-analyzer/intervals_04/main.c

@@ -1,4 +1,3 @@
-//#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/intervals_05/main.c

@@ -1,4 +1,3 @@
-//#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/intervals_06/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main(){
   int x;

regression/goto-analyzer/intervals_07/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main(){
   int x;

regression/goto-analyzer/intervals_08/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main(){
   int x;

regression/goto-analyzer/intervals_09/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/intervals_10/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/intervals_11/main.c

@@ -1,4 +1,4 @@
-#include <assert.h>
+
 const int xLen = 10;
 const int Alen = 2;
 const int Blen = 1;

regression/goto-analyzer/intervals_12/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main (void) {
   int i;

regression/goto-analyzer/intervals_13/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/intervals_13/test.desc

@@ -3,13 +3,13 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 8 function main, assertion i>=10: Success$
-^\[main.assertion.2\] file main.c line 11 function main, assertion i!=30: Success$
-^\[main.assertion.3\] file main.c line 14 function main, assertion i!=15: Unknown$
-^\[main.assertion.4\] file main.c line 17 function main, assertion 0: Success$
-^\[main.assertion.5\] file main.c line 20 function main, assertion j>=10: Success$
-^\[main.assertion.6\] file main.c line 23 function main, assertion i>=j: Unknown$
-^\[main.assertion.7\] file main.c line 26 function main, assertion i>=11: Success$
-^\[main.assertion.8\] file main.c line 29 function main, assertion j<100: Success$
+^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: Success$
+^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: Success$
+^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: Unknown$
+^\[main.assertion.4\] file main.c line 16 function main, assertion 0: Success$
+^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: Success$
+^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: Unknown$
+^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: Success$
+^\[main.assertion.8\] file main.c line 28 function main, assertion j\s*<\s*100: Success$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_14/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/intervals_15/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 
 int main()
 {

regression/goto-analyzer/intervals_15/test.desc

@@ -3,6 +3,6 @@ main.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file main.c line 12 function main, assertion j<52: Unknown$
+^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: Unknown$
 --
 ^warning: ignoring

regression/goto-analyzer/intervals_16/main.c

@@ -0,0 +1,13 @@
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<=50) 
+  {
+    i++;
+    j++;
+  }
+  assert(j<52);
+}
+

regression/goto-analyzer/intervals_16/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: (Unknown|Failure \(if reachable\))$
+--
+^warning: ignoring

src/analyses/is_threaded.cpp

@@ -29,10 +29,7 @@ class is_threaded_domaint:public ai_domain_baset
     locationt from,
     locationt to)
   {
-    // assert(src.reachable);
-
-    if(!src.reachable)
-      return false;
+    assert(src.reachable);
 
     bool old_reachable=reachable;
     bool old_is_threaded=is_threaded;
@@ -50,10 +47,7 @@ class is_threaded_domaint:public ai_domain_baset
     ai_baset &ai,
     const namespacet &ns) final override
   {
-    // assert(reachable);
-
-    if(!reachable)
-      return;
+    assert(reachable);
 
     if(from->is_start_thread())
       is_threaded=true;