Narrowing test (not working though, but should)

tests/regression/77-lin2vareq/28-narrowing.c → tests/regression/77-lin2vareq/28-narrowing-on-steroids.c

@@ -1,26 +1,31 @@
-// SKIP PARAM: --set ana.activated[+] lin2vareq --enable ana.int.interval
+// SKIP PARAM: --set ana.activated[+] lin2vareq --enable ana.int.interval  --set sem.int.signed_overflow assume_none
 #include <assert.h>
 
-int g = 0;
-
 int main() {
+  int a;
+  a = a % 10;
+  int b;
+  int c;
+  b = a + 1;
+  c = a + 2;
   int x;
 
   for (x = 0; x < 50; x++) {
-    g = 1;
+    a = 1;
   }
 
   if (x > 50) { 
 
     for (int i = 0; i <= 0; i--) {
-      g = 57;
+      c = 57;
 
       int y;
 
       for (y = 0; y < x; y++) { 
-        g = 42;
+        b = 42;
       }
     }
-    assert(1); // NOWARN (unreachable)
+    assert(0); // NOWARN (unreachable)
   }
+  assert(b + 1 == c);// SUCCESS 
 }

tests/regression/77-lin2vareq/cast-to-short2.c

@@ -0,0 +1,27 @@
+// SKIP PARAM: --set ana.activated[+] lin2vareq --set sem.int.signed_overflow assume_none
+
+#include <stdio.h>
+int main() {
+
+  unsigned int allbits = -255 - 25; // choose a value which is not representable in short
+  int signedallbits = allbits;
+  short unsignedtosigned = allbits;
+  unsigned short unsignedtounsigned = allbits;
+
+  printf("allbits: %u\n", allbits);
+  printf("signedallbits: %d\n", signedallbits);
+  printf("unsignedtosigned: %hd\n", unsignedtosigned);
+  printf("unsignedtounsigned: %hu\n", unsignedtounsigned);
+
+  if (unsignedtounsigned == 4294967295) {
+//    __goblint_check(0); // NOWARN (unreachable)
+    return (-1);
+  }
+  if (allbits == 4294967295 && signedallbits == -1 && unsignedtosigned == -1 &&
+      unsignedtounsigned == 65535) {
+ //   __goblint_check(1); // reachable
+    return (-1);
+  }
+ // __goblint_check(0); // NOWARN (unreachable)
+  return (0);
+}