Add test case for cast.

goblint · Nov 20, 2023 · 4f7eb52 · 4f7eb52
1 parent 631f4fc
commit 4f7eb52
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/tests/regression/29-svcomp/32-no-ov.c b/tests/regression/29-svcomp/32-no-ov.c
@@ -0,0 +1,7 @@
+// PARAM: --enable ana.int.interval --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )"
+
+int main(){
+	// This is not an overflow, just implementation defined behavior on a cast
+	int data = ((int)(rand() & 1 ? (((unsigned)rand()<<30) ^ ((unsigned)rand()<<15) ^ rand()) : -(((unsigned)rand()<<30) ^ ((unsigned)rand()<<15) ^ rand()) - 1));
+	return 0;
+}