-
Notifications
You must be signed in to change notification settings - Fork 41
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
29 changed files
with
438 additions
and
438 deletions.
There are no files selected for viewing
28 changes: 14 additions & 14 deletions
28
...erflow/regression/Abs_false-no-overflow.c → ...ow/regression/all/Abs_false-no-overflow.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,14 +1,14 @@ | ||
| // Author: [email protected] | ||
| // 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: [email protected] | ||
| // 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; | ||
| } |
28 changes: 14 additions & 14 deletions
28
...verflow/regression/Abs_true-no-overflow.c → ...low/regression/all/Abs_true-no-overflow.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,14 +1,14 @@ | ||
| // Author: [email protected] | ||
| // 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: [email protected] | ||
| // 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; | ||
| } |
24 changes: 12 additions & 12 deletions
24
...ession/AdditionIntMax_false-no-overflow.c → ...on/all/AdditionIntMax_false-no-overflow.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,12 +1,12 @@ | ||
| // Author: [email protected] | ||
| // 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: [email protected] | ||
| // 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; | ||
| } |
26 changes: 13 additions & 13 deletions
26
...ession/AdditionIntMin_false-no-overflow.c → ...on/all/AdditionIntMin_false-no-overflow.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,13 +1,13 @@ | ||
| // Author: [email protected] | ||
| // 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: [email protected] | ||
| // 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; | ||
| } |
40 changes: 20 additions & 20 deletions
40
...AutomizerC-SignedIntegerOverflowCheck.epf → ...AutomizerC-SignedIntegerOverflowCheck.epf
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
34 changes: 17 additions & 17 deletions
34
.../ConversionToSignedInt_true-no-overflow.c → .../ConversionToSignedInt_true-no-overflow.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,17 +1,17 @@ | ||
| // Author: [email protected] | ||
| // 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: [email protected] | ||
| // 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; | ||
| } |
26 changes: 13 additions & 13 deletions
26
...w/regression/Division_false-no-overflow.c → ...gression/all/Division_false-no-overflow.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,13 +1,13 @@ | ||
| // Author: [email protected] | ||
| // 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: [email protected] | ||
| // 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; | ||
| } |
36 changes: 18 additions & 18 deletions
36
...ssion/IntegerPromotion_true-no-overflow.c → ...n/all/IntegerPromotion_true-no-overflow.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,18 +1,18 @@ | ||
| // Author: [email protected] | ||
| // 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: [email protected] | ||
| // 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; | ||
| } |
38 changes: 19 additions & 19 deletions
38
...gerOverflow/regression/Multiplication03.c → ...verflow/regression/all/Multiplication03.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,19 +1,19 @@ | ||
| // #Unsafe | ||
| // Author: [email protected] | ||
| // 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: [email protected] | ||
| // 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; | ||
| } |
34 changes: 17 additions & 17 deletions
34
...gerOverflow/regression/Multiplication04.c → ...verflow/regression/all/Multiplication04.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,17 +1,17 @@ | ||
| // #Safe | ||
| // Author: [email protected] | ||
| // 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: [email protected] | ||
| // 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; | ||
| } |
36 changes: 18 additions & 18 deletions
36
...gerOverflow/regression/Multiplication05.c → ...verflow/regression/all/Multiplication05.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,18 +1,18 @@ | ||
| // #Safe | ||
| // Author: [email protected] | ||
| // 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: [email protected] | ||
| // 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; | ||
| } |
24 changes: 12 additions & 12 deletions
24
...ession/Multiplication_false-no-overflow.c → ...on/all/Multiplication_false-no-overflow.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,12 +1,12 @@ | ||
| // Author: [email protected] | ||
| // 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: [email protected] | ||
| // 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; | ||
| } |
Oops, something went wrong.