Add test case for branching on unions for union-map-domain.

goblint · Nov 28, 2023 · e58e7f6 · e58e7f6
1 parent ae1204d
commit e58e7f6
Showing 1 changed file with 28 additions and 0 deletions.
diff --git a/tests/regression/27-inv_invariants/20-union-map-domain-float-int.c b/tests/regression/27-inv_invariants/20-union-map-domain-float-int.c
@@ -0,0 +1,28 @@
+// PARAM: --enable ana.float.interval --set ana.base.unions.domain map
+#include <goblint.h>
+union u {
+	int x;
+	float f;
+};
+
+int main(){
+	union u a;
+	union u b;
+
+	a.x = 12;
+	b.f = 129.0;
+
+	int i = 0;
+	if(a.x == b.x){
+		i++;
+	}
+	// Should not be dead after if
+	__goblint_check(1);
+
+	if(a.f == b.f){
+		i++;
+	}
+	// Should not be dead after if
+	__goblint_check(1);
+	return 0;
+}