Merge pull request #1699 from goblint/issue_1697b

Relational: Assert type bounds after `assign` & Fix loop tests

Author: michael-schwarz

src/analyses/apron/relationAnalysis.apron.ml

@@ -256,8 +256,9 @@ struct
             if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pretty v d_exp e' d_plainexp e';
             if M.tracing then M.trace "relation" "st: %a" RD.pretty apr';
             let r = RD.assign_exp ask apr' (RV.local v) e' (no_overflow ask simplified_e) in
-            if M.tracing then M.traceu "relation" "-> %a" RD.pretty r;
-            r
+            let r' = assert_type_bounds ask r v in
+            if M.tracing then M.traceu "relation" "-> %a" RD.pretty r';
+            r'
           )
       )
     in

tests/regression/24-octagon/18-dead.c

@@ -0,0 +1,23 @@
+//SKIP PARAM: --enable ana.int.interval --set ana.activated[+] apron
+// NOCRASH (was arithmetic on bottom)
+int main(void)
+{
+    int a;
+    unsigned short b;
+    int tmp;
+
+    b = (unsigned short )a;
+
+    if ((int )b + (int )b < (int )b) {
+
+        tmp = (int )b;
+        b += 1;
+
+        if (! tmp) {
+           tmp = 1;
+        }
+
+    }
+
+    return 0;
+}

tests/regression/78-termination/01-simple-loop-terminating.c

@@ -3,7 +3,7 @@
 
 int main()
 {
-  int i = 1;
+  unsigned int i = 1;
 
   while (i <= 10)
   {

tests/regression/78-termination/03-nested-loop-terminating.c

@@ -3,9 +3,9 @@
 
 int main()
 {
-  int rows = 3;
-  int columns = 4;
-  int i = 1;
+  unsigned int rows = 3;
+  unsigned int columns = 4;
+  unsigned int i = 1;
 
   // Outer while loop for rows
   while (i <= rows)

tests/regression/78-termination/04-nested-loop-nonterminating.c

@@ -7,7 +7,7 @@ int main()
 
   while (outerCount <= 3)
   {
-    int innerCount = 1;
+    unsigned int innerCount = 1;
 
     while (1) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop
     {

tests/regression/78-termination/05-for-loop-terminating.c

@@ -3,7 +3,7 @@
 
 int main()
 {
-  int i;
+  unsigned int i;
 
   for (i = 1; i <= 10; i++)
   {

tests/regression/78-termination/07-nested-for-loop-terminating.c

@@ -3,8 +3,8 @@
 
 int main()
 {
-  int rows = 3;
-  int columns = 4;
+  unsigned int rows = 3;
+  unsigned int columns = 4;
 
   // Nested loop to iterate over rows and columns
   for (int i = 1; i <= rows; i++)

tests/regression/78-termination/08-nested-for-loop-nonterminating.c

@@ -3,7 +3,7 @@
 
 int main()
 {
-  int outerCount, innerCount;
+  unsigned int outerCount, innerCount;
 
   for (outerCount = 1; outerCount <= 3; outerCount++)
   {

tests/regression/78-termination/09-complex-for-loop-terminating.c

@@ -3,7 +3,7 @@
 #include <stdio.h>
 
 int loops0(){
-  int i, j, k;
+  unsigned int i, j, k;
 
   // Outer loop
   for (i = 1; i <= 5; i++)
@@ -36,7 +36,7 @@ int loops0(){
 }
 
 int loops1(){
-  int i, j, k;
+  unsigned int i, j, k;
 
   // Loop with conditions
   for (i = 1; i <= 10; i++)
@@ -81,7 +81,7 @@ int loops1(){
   printf("\n");
 
   // Loop with multiple variables
-  int a, b, c;
+  unsigned int a, b, c;
   for (a = 1, b = 2, c = 3; a <= 10; a++, b += 2, c += 3)
   {
     printf("%d %d %d\n", a, b, c);

tests/regression/78-termination/10-complex-loop-terminating.c

@@ -3,9 +3,9 @@
 #include <stdio.h>
 
 int loops0(){
-  int i = 1;
-  int j = 1;
-  int k = 5;
+  unsigned int i = 1;
+  unsigned int j = 1;
+  unsigned int k = 5;
 
   // Outer while loop
   while (i <= 5)
@@ -84,9 +84,9 @@ int loops0(){
 
 int loops1()
 {
-  int i = 1;
-  int j = 1;
-  int k = 5;
+  unsigned int i = 1;
+  unsigned int j = 1;
+  unsigned int k = 5;
 
   // Outer while loop
   while (i <= 5)
@@ -145,9 +145,9 @@ int loops1()
 }
 
 int loops2(){
-  int i = 1;
-  int j = 1;
-  int k = 5;
+  unsigned int i = 1;
+  unsigned int j = 1;
+  unsigned int k = 5;
 
   // Loop with nested conditions
   i = 1;
@@ -197,9 +197,9 @@ int loops2(){
   printf("\n");
 
   // Loop with multiple variables
-  int a = 1;
-  int b = 2;
-  int c = 3;
+  unsigned int a = 1;
+  unsigned int b = 2;
+  unsigned int c = 3;
   while (a <= 10)
   {
     printf("%d %d %d\n", a, b, c);
@@ -215,4 +215,4 @@ int main(){
   loops1();
   loops2();
   return 0;
-}
+}