Split overflow tests (#611)

ultimate-pa · Feb 28, 2024 · e7be01e · e7be01e
1 parent 76333b4
commit e7be01e
Show file tree

Hide file tree

Showing 29 changed files with 438 additions and 438 deletions.
diff --git a/...erflow/regression/Abs_false-no-overflow.c → ...ow/regression/all/Abs_false-no-overflow.c b/...erflow/regression/Abs_false-no-overflow.c → ...ow/regression/all/Abs_false-no-overflow.c
@@ -1,14 +1,14 @@
-// Author: heizmann@informatik.uni-freiburg.de
-// Date: 2022-11-16
-//
-// We assume sizeof(int)=4.
-
-#include <stdio.h>
-#include <stdlib.h>
-
-int main() {
-	int minInt = -2147483647 - 1;
-	int x = abs(minInt);
-	printf("%d\n", x);
-	return 0;
-}
+// Author: heizmann@informatik.uni-freiburg.de
+// Date: 2022-11-16
+//
+// We assume sizeof(int)=4.
+
+#include <stdio.h>
+#include <stdlib.h>
+
+int main() {
+	int minInt = -2147483647 - 1;
+	int x = abs(minInt);
+	printf("%d\n", x);
+	return 0;
+}
diff --git a/...verflow/regression/Abs_true-no-overflow.c → ...low/regression/all/Abs_true-no-overflow.c b/...verflow/regression/Abs_true-no-overflow.c → ...low/regression/all/Abs_true-no-overflow.c
@@ -1,14 +1,14 @@
-// Author: heizmann@informatik.uni-freiburg.de
-// Date: 2022-11-16
-//
-// We assume sizeof(int)=4.
-
-#include <stdio.h>
-#include <stdlib.h>
-
-int main() {
-	int smallNumber = -2147483647;
-	int x = abs(smallNumber);
-	printf("%d\n", x);
-	return 0;
-}
+// Author: heizmann@informatik.uni-freiburg.de
+// Date: 2022-11-16
+//
+// We assume sizeof(int)=4.
+
+#include <stdio.h>
+#include <stdlib.h>
+
+int main() {
+	int smallNumber = -2147483647;
+	int x = abs(smallNumber);
+	printf("%d\n", x);
+	return 0;
+}
diff --git a/...ession/AdditionIntMax_false-no-overflow.c → ...on/all/AdditionIntMax_false-no-overflow.c b/...ession/AdditionIntMax_false-no-overflow.c → ...on/all/AdditionIntMax_false-no-overflow.c
@@ -1,12 +1,12 @@
-// Author: heizmann@informatik.uni-freiburg.de
-// Date: 2015-09-01
-//
-// We assume sizeof(int)=4.
-
-#include <stdio.h>
-
-int main() {
-	int x = (2147483647 + 1) - 23;
-	printf("%d\n", x);
-	return 0;
-}
+// Author: heizmann@informatik.uni-freiburg.de
+// Date: 2015-09-01
+//
+// We assume sizeof(int)=4.
+
+#include <stdio.h>
+
+int main() {
+	int x = (2147483647 + 1) - 23;
+	printf("%d\n", x);
+	return 0;
+}
diff --git a/...ession/AdditionIntMin_false-no-overflow.c → ...on/all/AdditionIntMin_false-no-overflow.c b/...ession/AdditionIntMin_false-no-overflow.c → ...on/all/AdditionIntMin_false-no-overflow.c
@@ -1,13 +1,13 @@
-// Author: heizmann@informatik.uni-freiburg.de
-// Date: 2015-09-01
-//
-// We assume sizeof(int)=4.
-
-#include <stdio.h>
-
-int main() {
-	int minInt = -2147483647 - 1;
-	int x = (minInt + -1) + 23;
-	printf("%d\n", x);
-	return 0;
-}
+// Author: heizmann@informatik.uni-freiburg.de
+// Date: 2015-09-01
+//
+// We assume sizeof(int)=4.
+
+#include <stdio.h>
+
+int main() {
+	int minInt = -2147483647 - 1;
+	int x = (minInt + -1) + 23;
+	printf("%d\n", x);
+	return 0;
+}
diff --git a/...AutomizerC-SignedIntegerOverflowCheck.epf → ...AutomizerC-SignedIntegerOverflowCheck.epf b/...AutomizerC-SignedIntegerOverflowCheck.epf → ...AutomizerC-SignedIntegerOverflowCheck.epf
@@ -1,20 +1,20 @@
-#Mon Sep 07 12:50:17 CEST 2015
-@de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=0.0.1
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ absence\ of\ signed\ integer\ overflows=true
-#Mon Sep 07 12:50:17 CEST 2015
-file_export_version=3.0
-#Wed Jan 15 21:36:24 CET 2014
-file_export_version=3.0
-@de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=0.0.1
-\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=true
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/SMT\ solver=External_ModelsAndUnsatCoreMode
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ strategy=FIXED_PREFERENCES
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -t\:12000
-
-#Fri Mar 07 12:08:07 CET 2014
-/instance/de.uni_freiburg.informatik.ultimate.core/Log\ Level\ for\ Controller\ Plugin=INFO
-/instance/de.uni_freiburg.informatik.ultimate.core/Log\ Level\ for\ Core\ Plugin=INFO
-/instance/de.uni_freiburg.informatik.ultimate.core/Log\ Level\ for\ External\ Tools=INFO
-/instance/de.uni_freiburg.informatik.ultimate.core/Root\ Log\ Level=INFO
-/instance/de.uni_freiburg.informatik.ultimate.core/Log\ Level\ for\ Plugins=INFO
+#Mon Sep 07 12:50:17 CEST 2015
+@de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=0.0.1
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ absence\ of\ signed\ integer\ overflows=true
+#Mon Sep 07 12:50:17 CEST 2015
+file_export_version=3.0
+#Wed Jan 15 21:36:24 CET 2014
+file_export_version=3.0
+@de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=0.0.1
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/SMT\ solver=External_ModelsAndUnsatCoreMode
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ strategy=FIXED_PREFERENCES
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -t\:12000
+
+#Fri Mar 07 12:08:07 CET 2014
+/instance/de.uni_freiburg.informatik.ultimate.core/Log\ Level\ for\ Controller\ Plugin=INFO
+/instance/de.uni_freiburg.informatik.ultimate.core/Log\ Level\ for\ Core\ Plugin=INFO
+/instance/de.uni_freiburg.informatik.ultimate.core/Log\ Level\ for\ External\ Tools=INFO
+/instance/de.uni_freiburg.informatik.ultimate.core/Root\ Log\ Level=INFO
+/instance/de.uni_freiburg.informatik.ultimate.core/Log\ Level\ for\ Plugins=INFO
diff --git a/.../ConversionToSignedInt_true-no-overflow.c → .../ConversionToSignedInt_true-no-overflow.c b/.../ConversionToSignedInt_true-no-overflow.c → .../ConversionToSignedInt_true-no-overflow.c
@@ -1,17 +1,17 @@
-// Author: heizmann@informatik.uni-freiburg.de
-// Date: 2015-09-09
-//
-// We assume sizeof(int)=4 and sizeof(long)>4.
-
-#include <stdio.h>
-
-int main() {
-	// The literal of type long on the right-hand side is exactly INT_MAX+1 and will 
-	// be converted to int.
-	// Paragraph 6.3.1.3.3 of C11 says that if "[..] the new type is signed and the 
-	// value cannot be represented in it; either the result is implementation-defined 
-	// or an implementation-defined signal is raised."
-	int x = 2147483648L;
-	printf("%d\n", x);
-	return 0;
-}
+// Author: heizmann@informatik.uni-freiburg.de
+// Date: 2015-09-09
+//
+// We assume sizeof(int)=4 and sizeof(long)>4.
+
+#include <stdio.h>
+
+int main() {
+	// The literal of type long on the right-hand side is exactly INT_MAX+1 and will 
+	// be converted to int.
+	// Paragraph 6.3.1.3.3 of C11 says that if "[..] the new type is signed and the 
+	// value cannot be represented in it; either the result is implementation-defined 
+	// or an implementation-defined signal is raised."
+	int x = 2147483648L;
+	printf("%d\n", x);
+	return 0;
+}
diff --git a/...w/regression/Division_false-no-overflow.c → ...gression/all/Division_false-no-overflow.c b/...w/regression/Division_false-no-overflow.c → ...gression/all/Division_false-no-overflow.c
@@ -1,13 +1,13 @@
-// Author: heizmann@informatik.uni-freiburg.de
-// Date: 2015-09-01
-//
-// We assume sizeof(int)=4.
-
-#include <stdio.h>
-
-int main() {
-	int minInt = -2147483647 - 1;
-	int x = (minInt / -1 ) - 1;
-	printf("%d\n", x);
-	return 0;
-}
+// Author: heizmann@informatik.uni-freiburg.de
+// Date: 2015-09-01
+//
+// We assume sizeof(int)=4.
+
+#include <stdio.h>
+
+int main() {
+	int minInt = -2147483647 - 1;
+	int x = (minInt / -1 ) - 1;
+	printf("%d\n", x);
+	return 0;
+}
diff --git a/...ssion/IntegerPromotion_true-no-overflow.c → ...n/all/IntegerPromotion_true-no-overflow.c b/...ssion/IntegerPromotion_true-no-overflow.c → ...n/all/IntegerPromotion_true-no-overflow.c
@@ -1,18 +1,18 @@
-// Author: heizmann@informatik.uni-freiburg.de
-// Date: 2015-09-01
-
-#include <stdio.h>
-
-int main() {
-	// we assume sizeof(short)=2 and sizeof(int)=4
-	// assume SHRT_MAX=32768
-	short a = 32767;
-	// "Surprisingly", there is no overflow here. During the usual arithmetic
-	// conversions, the operands of + are promoted to int.
-	// The right-hand side of the assignment is converted to unsigned short
-	// which is defined in 6.3.1.3.2 of C11
-	// http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf
-	unsigned short b = a + a + a;
-	printf("value %u",b);
-	return 0;
-}
+// Author: heizmann@informatik.uni-freiburg.de
+// Date: 2015-09-01
+
+#include <stdio.h>
+
+int main() {
+	// we assume sizeof(short)=2 and sizeof(int)=4
+	// assume SHRT_MAX=32768
+	short a = 32767;
+	// "Surprisingly", there is no overflow here. During the usual arithmetic
+	// conversions, the operands of + are promoted to int.
+	// The right-hand side of the assignment is converted to unsigned short
+	// which is defined in 6.3.1.3.2 of C11
+	// http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf
+	unsigned short b = a + a + a;
+	printf("value %u",b);
+	return 0;
+}
diff --git a/...gerOverflow/regression/Multiplication03.c → ...verflow/regression/all/Multiplication03.c b/...gerOverflow/regression/Multiplication03.c → ...verflow/regression/all/Multiplication03.c
@@ -1,19 +1,19 @@
-// #Unsafe
-// Author: heizmann@informatik.uni-freiburg.de
-// Date: 2022-11-20
-//
-// We assume sizeof(int)=4.
-
-#include <limits.h>
-#include <stdio.h>
-
-
-int main() {
-	int x = 2147483647;
-	int y = 2147483647;
-	// Although the value is assigned to a long long
-	// the result of the multiplication has type int
-	long long z = x * y;
-	printf("%lld\n", z);
-	return 0;
-}
+// #Unsafe
+// Author: heizmann@informatik.uni-freiburg.de
+// Date: 2022-11-20
+//
+// We assume sizeof(int)=4.
+
+#include <limits.h>
+#include <stdio.h>
+
+
+int main() {
+	int x = 2147483647;
+	int y = 2147483647;
+	// Although the value is assigned to a long long
+	// the result of the multiplication has type int
+	long long z = x * y;
+	printf("%lld\n", z);
+	return 0;
+}
diff --git a/...gerOverflow/regression/Multiplication04.c → ...verflow/regression/all/Multiplication04.c b/...gerOverflow/regression/Multiplication04.c → ...verflow/regression/all/Multiplication04.c
@@ -1,17 +1,17 @@
-// #Safe
-// Author: heizmann@informatik.uni-freiburg.de
-// Date: 2022-11-20
-//
-// We assume sizeof(int)=4.
-
-#include <limits.h>
-#include <stdio.h>
-
-
-int main() {
-	long long x = 2147483647;
-	long long y = 2147483647;
-	long long z = x * y;
-	printf("%lld\n", z);
-	return 0;
-}
+// #Safe
+// Author: heizmann@informatik.uni-freiburg.de
+// Date: 2022-11-20
+//
+// We assume sizeof(int)=4.
+
+#include <limits.h>
+#include <stdio.h>
+
+
+int main() {
+	long long x = 2147483647;
+	long long y = 2147483647;
+	long long z = x * y;
+	printf("%lld\n", z);
+	return 0;
+}
diff --git a/...gerOverflow/regression/Multiplication05.c → ...verflow/regression/all/Multiplication05.c b/...gerOverflow/regression/Multiplication05.c → ...verflow/regression/all/Multiplication05.c
@@ -1,18 +1,18 @@
-// #Safe
-// Author: heizmann@informatik.uni-freiburg.de
-// Date: 2022-11-20
-//
-// We assume sizeof(int)=4.
-
-#include <limits.h>
-#include <stdio.h>
-
-
-int main() {
-	long long x = -2147483648LL;
-	long long y = -2147483648LL;
-	// size of long long is sufficient -2^31*-2^31=2^62
-	long long z = x * y;
-	printf("%lld\n", z);
-	return 0;
-}
+// #Safe
+// Author: heizmann@informatik.uni-freiburg.de
+// Date: 2022-11-20
+//
+// We assume sizeof(int)=4.
+
+#include <limits.h>
+#include <stdio.h>
+
+
+int main() {
+	long long x = -2147483648LL;
+	long long y = -2147483648LL;
+	// size of long long is sufficient -2^31*-2^31=2^62
+	long long z = x * y;
+	printf("%lld\n", z);
+	return 0;
+}
diff --git a/...ession/Multiplication_false-no-overflow.c → ...on/all/Multiplication_false-no-overflow.c b/...ession/Multiplication_false-no-overflow.c → ...on/all/Multiplication_false-no-overflow.c
@@ -1,12 +1,12 @@
-// Author: heizmann@informatik.uni-freiburg.de
-// Date: 2015-09-01
-//
-// We assume sizeof(int)=4.
-
-#include <stdio.h>
-
-int main() {
-	int x = (65536 * 32768) - 1;
-	printf("%d\n", x);
-	return 0;
-}
+// Author: heizmann@informatik.uni-freiburg.de
+// Date: 2015-09-01
+//
+// We assume sizeof(int)=4.
+
+#include <stdio.h>
+
+int main() {
+	int x = (65536 * 32768) - 1;
+	printf("%d\n", x);
+	return 0;
+}