diff --git a/c/termination-bwb/Makefile b/c/termination-bwb/Makefile new file mode 100644 index 00000000000..2894dd346e5 --- /dev/null +++ b/c/termination-bwb/Makefile @@ -0,0 +1,14 @@ +# SPDX-FileCopyrightText: 2015-2016 Daniel Liew +# SPDX-FileCopyrightText: 2015-2020 The SV-Benchmarks Community +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +LEVEL := ../ + +CC.Arch := 64 + +COMMON_WARNINGS := \ + -Wno-error=return-type \ + +include $(LEVEL)/Makefile.config diff --git a/c/termination-bwb/and-01-false.c b/c/termination-bwb/and-01-false.c new file mode 100644 index 00000000000..b5ccc560c19 --- /dev/null +++ b/c/termination-bwb/and-01-false.c @@ -0,0 +1,22 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet(); + +int main (){ + int a, x; + x = __VERIFIER_nondet(); + a = 34; + while (x==0){ + a--; + x=x&a; + } + return 0; +} diff --git a/c/termination-bwb/and-01-false.yml b/c/termination-bwb/and-01-false.yml new file mode 100644 index 00000000000..1c555c14094 --- /dev/null +++ b/c/termination-bwb/and-01-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'and-01-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/and-01.c b/c/termination-bwb/and-01.c new file mode 100644 index 00000000000..0e359339991 --- /dev/null +++ b/c/termination-bwb/and-01.c @@ -0,0 +1,25 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet(); +extern void __VERIFIER_assume() __attribute__ ((__noreturn__)); + +int main (){ + int a, x; + x = __VERIFIER_nondet(); + a = __VERIFIER_nondet(); + __VERIFIER_assume(a>0); + + while (x>0){ + a--; + x=x&a; + } + return 0; +} diff --git a/c/termination-bwb/and-01.yml b/c/termination-bwb/and-01.yml new file mode 100644 index 00000000000..eac3e75490e --- /dev/null +++ b/c/termination-bwb/and-01.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'and-01.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/and-02-false.c b/c/termination-bwb/and-02-false.c new file mode 100644 index 00000000000..80654a1a34e --- /dev/null +++ b/c/termination-bwb/and-02-false.c @@ -0,0 +1,28 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); +//unsigned int __VERIFIER_nondet_int(); +int main (){ + int a; + int x; + x = __VERIFIER_nondet_int(); + a = 16; + while (x==0){ + a--; + if (x >= 0){ + x = x&a; + } + else { + x++; + } + } + return 0; +} diff --git a/c/termination-bwb/and-02-false.yml b/c/termination-bwb/and-02-false.yml new file mode 100644 index 00000000000..c31fbac5715 --- /dev/null +++ b/c/termination-bwb/and-02-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'and-02-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/and-02.c b/c/termination-bwb/and-02.c new file mode 100644 index 00000000000..79cedc4f1b5 --- /dev/null +++ b/c/termination-bwb/and-02.c @@ -0,0 +1,28 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); +//unsigned int __VERIFIER_nondet_int(); +int main (){ + int a; + int x; + x = __VERIFIER_nondet_int(); + a = 16; + while (x!=0){ + a--; + if (x > 0){ + x = x&a; + } + else { + x++; + } + } + return 0; +} diff --git a/c/termination-bwb/and-02.yml b/c/termination-bwb/and-02.yml new file mode 100644 index 00000000000..83027222480 --- /dev/null +++ b/c/termination-bwb/and-02.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'and-02.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/and-03-false.c b/c/termination-bwb/and-03-false.c new file mode 100644 index 00000000000..c918ebd9b4e --- /dev/null +++ b/c/termination-bwb/and-03-false.c @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); +//unsigned int __VERIFIER_nondet_int(); +int main (){ + int x; + x = __VERIFIER_nondet_int(); + while (x==0){ + + if (x >= 0 ){ + x = x&(x-1); + } + else { + x++; + } + } + return 0; +} diff --git a/c/termination-bwb/and-03-false.yml b/c/termination-bwb/and-03-false.yml new file mode 100644 index 00000000000..9490b22b2fb --- /dev/null +++ b/c/termination-bwb/and-03-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'and-03-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/and-03.c b/c/termination-bwb/and-03.c new file mode 100644 index 00000000000..2776744487a --- /dev/null +++ b/c/termination-bwb/and-03.c @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); +//unsigned int __VERIFIER_nondet_int(); +int main (){ + int x; + x = __VERIFIER_nondet_int(); + while (x!=0){ + + if (x > 0 ){ + x = x&(x-1); + } + else { + x++; + } + } + return 0; +} diff --git a/c/termination-bwb/and-03.yml b/c/termination-bwb/and-03.yml new file mode 100644 index 00000000000..189baad2f16 --- /dev/null +++ b/c/termination-bwb/and-03.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'and-03.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/and-04-false.c b/c/termination-bwb/and-04-false.c new file mode 100644 index 00000000000..ccfaeb20369 --- /dev/null +++ b/c/termination-bwb/and-04-false.c @@ -0,0 +1,25 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); +//unsigned int __VERIFIER_nondet_int(); +int main (){ + int x; + x = __VERIFIER_nondet_int(); + while (x < 8){ + if (x == 0 ){ + x = x&(x-1); + } + else { + x = x-1; + } + } + return 0; +} diff --git a/c/termination-bwb/and-04-false.yml b/c/termination-bwb/and-04-false.yml new file mode 100644 index 00000000000..637d58aa645 --- /dev/null +++ b/c/termination-bwb/and-04-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'and-04-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/and-04.c b/c/termination-bwb/and-04.c new file mode 100644 index 00000000000..543a2fb0fce --- /dev/null +++ b/c/termination-bwb/and-04.c @@ -0,0 +1,25 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); +//unsigned int __VERIFIER_nondet_int(); +int main (){ + int x; + x = __VERIFIER_nondet_int(); + while (x>5){ + if (x != 10 ){ + x = x&(x-1); + } + else { + x = x-1; + } + } + return 0; +} diff --git a/c/termination-bwb/and-04.yml b/c/termination-bwb/and-04.yml new file mode 100644 index 00000000000..0ef21f1f5f4 --- /dev/null +++ b/c/termination-bwb/and-04.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'and-04.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/and-05-false.c b/c/termination-bwb/and-05-false.c new file mode 100644 index 00000000000..185d1d07646 --- /dev/null +++ b/c/termination-bwb/and-05-false.c @@ -0,0 +1,21 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); +//unsigned int __VERIFIER_nondet_int(); +int main (){ + int x, y, res; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + while (x<=y && y > 0){ + x = (x-1)&y; + } + return 0; +} diff --git a/c/termination-bwb/and-05-false.yml b/c/termination-bwb/and-05-false.yml new file mode 100644 index 00000000000..292e0c066da --- /dev/null +++ b/c/termination-bwb/and-05-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'and-05-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/and-05.c b/c/termination-bwb/and-05.c new file mode 100644 index 00000000000..b342dfd0620 --- /dev/null +++ b/c/termination-bwb/and-05.c @@ -0,0 +1,21 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); +//unsigned int __VERIFIER_nondet_int(); +int main (){ + int x, y, res; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + while (x>=y && y > 0){ + x = (x-1)&y; + } + return 0; +} diff --git a/c/termination-bwb/and-05.yml b/c/termination-bwb/and-05.yml new file mode 100644 index 00000000000..530d4f3fac0 --- /dev/null +++ b/c/termination-bwb/and-05.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'and-05.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/and-06.c b/c/termination-bwb/and-06.c new file mode 100644 index 00000000000..cd2404184c8 --- /dev/null +++ b/c/termination-bwb/and-06.c @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet(); + +int main (){ + int a, x; + x = __VERIFIER_nondet(); + a = __VERIFIER_nondet(); + while (x>0){ + a--; + if (a>0){ + x=x&a; + } else { + x = x&(x-1); + } + } + return 0; +} diff --git a/c/termination-bwb/and-06.yml b/c/termination-bwb/and-06.yml new file mode 100644 index 00000000000..6be0ef52887 --- /dev/null +++ b/c/termination-bwb/and-06.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'and-06.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/and-assme.c b/c/termination-bwb/and-assme.c new file mode 100644 index 00000000000..ba8efdf757c --- /dev/null +++ b/c/termination-bwb/and-assme.c @@ -0,0 +1,25 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet(); +void __VERIFIER_assume(); + +int main (){ + int a, x; + x = __VERIFIER_nondet(); + a = __VERIFIER_nondet(); + /* a = 34; */ + __VERIFIER_assume(a>0); + while (x>0){ + a--; + x=x&a; + } + return 0; +} diff --git a/c/termination-bwb/and-assme.yml b/c/termination-bwb/and-assme.yml new file mode 100644 index 00000000000..ddf83ab68b3 --- /dev/null +++ b/c/termination-bwb/and-assme.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'and-assme.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/consecutive-zero-bits-trailing.c b/c/termination-bwb/consecutive-zero-bits-trailing.c new file mode 100644 index 00000000000..d6514066692 --- /dev/null +++ b/c/termination-bwb/consecutive-zero-bits-trailing.c @@ -0,0 +1,56 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + + +#include +#define CHAR_BIT 8; +extern unsigned int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); + +unsigned int v; // 32-bit word input to count zero bits on right +unsigned int c; // c will be the number of zero bits on the right, + // so if v is 1101000 (base 2), then c will be 3 + +int z, y; +int main(){ + // NOTE: if 0 == v, then c = 31. + if (v & 0x1) + { + // special case for odd v (assumed to happen half of the time) + c = 0; + } + else + { + c = 1; + if ((v & 0xffff) == 0) + { + v >>= 16; + c += 16; + } + if ((v & 0xff) == 0) + { + v >>= 8; + c += 8; + } + if ((v & 0xf) == 0) + { + v >>= 4; + c += 4; + } + if ((v & 0x3) == 0) + { + v >>= 2; + c += 2; + } + c -= v & 0x1; + } + y=c+1; +// return (void*) z; + return 0; +} diff --git a/c/termination-bwb/consecutive-zero-bits-trailing.i b/c/termination-bwb/consecutive-zero-bits-trailing.i new file mode 100644 index 00000000000..657fb5b1c0c --- /dev/null +++ b/c/termination-bwb/consecutive-zero-bits-trailing.i @@ -0,0 +1,41 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +extern unsigned int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); +unsigned int v; +unsigned int c; +int z, y; +int main(){ + if (v & 0x1) + { + c = 0; + } + else + { + c = 1; + if ((v & 0xffff) == 0) + { + v >>= 16; + c += 16; + } + if ((v & 0xff) == 0) + { + v >>= 8; + c += 8; + } + if ((v & 0xf) == 0) + { + v >>= 4; + c += 4; + } + if ((v & 0x3) == 0) + { + v >>= 2; + c += 2; + } + c -= v & 0x1; + } + y=c+1; + return 0; +} diff --git a/c/termination-bwb/consecutive-zero-bits-trailing.yml b/c/termination-bwb/consecutive-zero-bits-trailing.yml new file mode 100644 index 00000000000..f61889af436 --- /dev/null +++ b/c/termination-bwb/consecutive-zero-bits-trailing.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'consecutive-zero-bits-trailing.i' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/counting-bits-BK.c b/c/termination-bwb/counting-bits-BK.c new file mode 100644 index 00000000000..09d9a682e33 --- /dev/null +++ b/c/termination-bwb/counting-bits-BK.c @@ -0,0 +1,33 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + + +#include + +extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); + +int v; // count the number of bits set in v +unsigned int c; // c accumulates the total bits set in v +int z, y; // word value to compute the parity of + +int main(){ + y = __VERIFIER_nondet_int(); + v= __VERIFIER_nondet_int(); + if (v>=0){ + for (c = 0; v; c++) { + /* v &= v - 1; // clear the least significant bit set */ + v = v&(v - 1); // clear the least significant bit set + } + y = 1; + } else { + y = -1; + } + return z; +} diff --git a/c/termination-bwb/counting-bits-BK.i b/c/termination-bwb/counting-bits-BK.i new file mode 100644 index 00000000000..1dc18db7039 --- /dev/null +++ b/c/termination-bwb/counting-bits-BK.i @@ -0,0 +1,21 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); +int v; +unsigned int c; +int z, y; +int main(){ + y = __VERIFIER_nondet_int(); + v= __VERIFIER_nondet_int(); + if (v>=0){ + for (c = 0; v; c++) { + v = v&(v - 1); + } + y = 1; + } else { + y = -1; + } + return z; +} diff --git a/c/termination-bwb/counting-bits-BK.yml b/c/termination-bwb/counting-bits-BK.yml new file mode 100644 index 00000000000..bb30f66b6cc --- /dev/null +++ b/c/termination-bwb/counting-bits-BK.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'counting-bits-BK.i' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/counting-bits-BK1.c b/c/termination-bwb/counting-bits-BK1.c new file mode 100644 index 00000000000..5f3d9ab9ca7 --- /dev/null +++ b/c/termination-bwb/counting-bits-BK1.c @@ -0,0 +1,32 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + + +#include + +extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); + +int v; // count the number of bits set in v +int c; // c accumulates the total bits set in v +int z, y; // word value to compute the parity of + +void main(){ + y = __VERIFIER_nondet_int(); + v= __VERIFIER_nondet_int(); + c=0; + while (v>0) + { + v = v&(v - 1); // clear the least significant bit set + c++; + } + y=1; +// return (void*) z +return 0; +} diff --git a/c/termination-bwb/counting-bits-BK1.i b/c/termination-bwb/counting-bits-BK1.i new file mode 100644 index 00000000000..1c25b28b819 --- /dev/null +++ b/c/termination-bwb/counting-bits-BK1.i @@ -0,0 +1,20 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); +int v; +int c; +int z, y; +int main(){ + y = __VERIFIER_nondet_int(); + v= __VERIFIER_nondet_int(); + c=0; + while (v>0) + { + v = v&(v - 1); + c++; + } + y=1; + return 0; +} diff --git a/c/termination-bwb/counting-bits-BK1.yml b/c/termination-bwb/counting-bits-BK1.yml new file mode 100644 index 00000000000..bf543167275 --- /dev/null +++ b/c/termination-bwb/counting-bits-BK1.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'counting-bits-BK1.i' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/counting-bits-set.c b/c/termination-bwb/counting-bits-set.c new file mode 100644 index 00000000000..0844c040e1f --- /dev/null +++ b/c/termination-bwb/counting-bits-set.c @@ -0,0 +1,35 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + + +#include + +extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); + +int v; // count the number of bits set in v +unsigned int c, z; // c accumulates the total bits set in v +int y; // word value to compute the parity of + +int main(){ + y = __VERIFIER_nondet_int(); + v = __VERIFIER_nondet_int(); + if (v>=0){ + for (c = 0; v; v >>= 1) + { + z = v & 1; + c = c+z; + } + y = z+1; + } else { + y=1; + } +// return (void*) z; +return 0; +} diff --git a/c/termination-bwb/counting-bits-set.i b/c/termination-bwb/counting-bits-set.i new file mode 100644 index 00000000000..22e33e763f7 --- /dev/null +++ b/c/termination-bwb/counting-bits-set.i @@ -0,0 +1,23 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); +int v; +unsigned int c, z; +int y; +int main(){ + y = __VERIFIER_nondet_int(); + v = __VERIFIER_nondet_int(); + if (v>=0){ + for (c = 0; v; v >>= 1) + { + z = v & 1; + c = c+z; + } + y = z+1; + } else { + y=1; + } + return 0; +} diff --git a/c/termination-bwb/counting-bits-set.yml b/c/termination-bwb/counting-bits-set.yml new file mode 100644 index 00000000000..892f6854f87 --- /dev/null +++ b/c/termination-bwb/counting-bits-set.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'counting-bits-set.i' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/display-bit.c b/c/termination-bwb/display-bit.c new file mode 100644 index 00000000000..13552d458e9 --- /dev/null +++ b/c/termination-bwb/display-bit.c @@ -0,0 +1,46 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + + +#include + +void displayBits(unsigned int value); +unsigned int number1= 65535; +int mask = 1; +unsigned int x; +int c = 1; +int y; +int main(void) { + /* printf("%s", "Engter a nonnegative int:"); */ + /* scanf("%u", &x); */ + + displayBits(mask); + displayBits(number1); + displayBits(number1 & mask); + y= c+mask; + return y; +} + +void displayBits(unsigned int value) { + unsigned int displayMask = 1<<31; + printf("%10u = ", value); + + while (c<=32) { + putchar(value & displayMask ? '1' : '0'); + value <<=1; //shift left by 1 + if (c % 8 == 0) { + putchar(' '); + } + mask = mask & 1; + c=c+mask; + } + putchar('\n'); + +} diff --git a/c/termination-bwb/display-bit.i b/c/termination-bwb/display-bit.i new file mode 100644 index 00000000000..884613686f4 --- /dev/null +++ b/c/termination-bwb/display-bit.i @@ -0,0 +1,295 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +typedef long unsigned int size_t; +typedef __builtin_va_list __gnuc_va_list; +typedef unsigned char __u_char; +typedef unsigned short int __u_short; +typedef unsigned int __u_int; +typedef unsigned long int __u_long; +typedef signed char __int8_t; +typedef unsigned char __uint8_t; +typedef signed short int __int16_t; +typedef unsigned short int __uint16_t; +typedef signed int __int32_t; +typedef unsigned int __uint32_t; +typedef signed long int __int64_t; +typedef unsigned long int __uint64_t; +typedef __int8_t __int_least8_t; +typedef __uint8_t __uint_least8_t; +typedef __int16_t __int_least16_t; +typedef __uint16_t __uint_least16_t; +typedef __int32_t __int_least32_t; +typedef __uint32_t __uint_least32_t; +typedef __int64_t __int_least64_t; +typedef __uint64_t __uint_least64_t; +typedef long int __quad_t; +typedef unsigned long int __u_quad_t; +typedef long int __intmax_t; +typedef unsigned long int __uintmax_t; +typedef unsigned long int __dev_t; +typedef unsigned int __uid_t; +typedef unsigned int __gid_t; +typedef unsigned long int __ino_t; +typedef unsigned long int __ino64_t; +typedef unsigned int __mode_t; +typedef unsigned long int __nlink_t; +typedef long int __off_t; +typedef long int __off64_t; +typedef int __pid_t; +typedef struct { int __val[2]; } __fsid_t; +typedef long int __clock_t; +typedef unsigned long int __rlim_t; +typedef unsigned long int __rlim64_t; +typedef unsigned int __id_t; +typedef long int __time_t; +typedef unsigned int __useconds_t; +typedef long int __suseconds_t; +typedef int __daddr_t; +typedef int __key_t; +typedef int __clockid_t; +typedef void * __timer_t; +typedef long int __blksize_t; +typedef long int __blkcnt_t; +typedef long int __blkcnt64_t; +typedef unsigned long int __fsblkcnt_t; +typedef unsigned long int __fsblkcnt64_t; +typedef unsigned long int __fsfilcnt_t; +typedef unsigned long int __fsfilcnt64_t; +typedef long int __fsword_t; +typedef long int __ssize_t; +typedef long int __syscall_slong_t; +typedef unsigned long int __syscall_ulong_t; +typedef __off64_t __loff_t; +typedef char *__caddr_t; +typedef long int __intptr_t; +typedef unsigned int __socklen_t; +typedef int __sig_atomic_t; +typedef struct +{ + int __count; + union + { + unsigned int __wch; + char __wchb[4]; + } __value; +} __mbstate_t; +typedef struct _G_fpos_t +{ + __off_t __pos; + __mbstate_t __state; +} __fpos_t; +typedef struct _G_fpos64_t +{ + __off64_t __pos; + __mbstate_t __state; +} __fpos64_t; +struct _IO_FILE; +typedef struct _IO_FILE __FILE; +struct _IO_FILE; +typedef struct _IO_FILE FILE; +struct _IO_FILE; +struct _IO_marker; +struct _IO_codecvt; +struct _IO_wide_data; +typedef void _IO_lock_t; +struct _IO_FILE +{ + int _flags; + char *_IO_read_ptr; + char *_IO_read_end; + char *_IO_read_base; + char *_IO_write_base; + char *_IO_write_ptr; + char *_IO_write_end; + char *_IO_buf_base; + char *_IO_buf_end; + char *_IO_save_base; + char *_IO_backup_base; + char *_IO_save_end; + struct _IO_marker *_markers; + struct _IO_FILE *_chain; + int _fileno; + int _flags2; + __off_t _old_offset; + unsigned short _cur_column; + signed char _vtable_offset; + char _shortbuf[1]; + _IO_lock_t *_lock; + __off64_t _offset; + struct _IO_codecvt *_codecvt; + struct _IO_wide_data *_wide_data; + struct _IO_FILE *_freeres_list; + void *_freeres_buf; + size_t __pad5; + int _mode; + char _unused2[15 * sizeof (int) - 4 * sizeof (void *) - sizeof (size_t)]; +}; +typedef __gnuc_va_list va_list; +typedef __off_t off_t; +typedef __ssize_t ssize_t; +typedef __fpos_t fpos_t; +extern FILE *stdin; +extern FILE *stdout; +extern FILE *stderr; +extern int remove (const char *__filename) __attribute__ ((__nothrow__ , __leaf__)); +extern int rename (const char *__old, const char *__new) __attribute__ ((__nothrow__ , __leaf__)); +extern int renameat (int __oldfd, const char *__old, int __newfd, + const char *__new) __attribute__ ((__nothrow__ , __leaf__)); +extern FILE *tmpfile (void) ; +extern char *tmpnam (char *__s) __attribute__ ((__nothrow__ , __leaf__)) ; +extern char *tmpnam_r (char *__s) __attribute__ ((__nothrow__ , __leaf__)) ; +extern char *tempnam (const char *__dir, const char *__pfx) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ; +extern int fclose (FILE *__stream); +extern int fflush (FILE *__stream); +extern int fflush_unlocked (FILE *__stream); +extern FILE *fopen (const char *__restrict __filename, + const char *__restrict __modes) ; +extern FILE *freopen (const char *__restrict __filename, + const char *__restrict __modes, + FILE *__restrict __stream) ; +extern FILE *fdopen (int __fd, const char *__modes) __attribute__ ((__nothrow__ , __leaf__)) ; +extern FILE *fmemopen (void *__s, size_t __len, const char *__modes) + __attribute__ ((__nothrow__ , __leaf__)) ; +extern FILE *open_memstream (char **__bufloc, size_t *__sizeloc) __attribute__ ((__nothrow__ , __leaf__)) ; +extern void setbuf (FILE *__restrict __stream, char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__)); +extern int setvbuf (FILE *__restrict __stream, char *__restrict __buf, + int __modes, size_t __n) __attribute__ ((__nothrow__ , __leaf__)); +extern void setbuffer (FILE *__restrict __stream, char *__restrict __buf, + size_t __size) __attribute__ ((__nothrow__ , __leaf__)); +extern void setlinebuf (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)); +extern int fprintf (FILE *__restrict __stream, + const char *__restrict __format, ...); +extern int printf (const char *__restrict __format, ...); +extern int sprintf (char *__restrict __s, + const char *__restrict __format, ...) __attribute__ ((__nothrow__)); +extern int vfprintf (FILE *__restrict __s, const char *__restrict __format, + __gnuc_va_list __arg); +extern int vprintf (const char *__restrict __format, __gnuc_va_list __arg); +extern int vsprintf (char *__restrict __s, const char *__restrict __format, + __gnuc_va_list __arg) __attribute__ ((__nothrow__)); +extern int snprintf (char *__restrict __s, size_t __maxlen, + const char *__restrict __format, ...) + __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 4))); +extern int vsnprintf (char *__restrict __s, size_t __maxlen, + const char *__restrict __format, __gnuc_va_list __arg) + __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 0))); +extern int vdprintf (int __fd, const char *__restrict __fmt, + __gnuc_va_list __arg) + __attribute__ ((__format__ (__printf__, 2, 0))); +extern int dprintf (int __fd, const char *__restrict __fmt, ...) + __attribute__ ((__format__ (__printf__, 2, 3))); +extern int fscanf (FILE *__restrict __stream, + const char *__restrict __format, ...) ; +extern int scanf (const char *__restrict __format, ...) ; +extern int sscanf (const char *__restrict __s, + const char *__restrict __format, ...) __attribute__ ((__nothrow__ , __leaf__)); +extern int fscanf (FILE *__restrict __stream, const char *__restrict __format, ...) __asm__ ("" "__isoc99_fscanf") ; +extern int scanf (const char *__restrict __format, ...) __asm__ ("" "__isoc99_scanf") ; +extern int sscanf (const char *__restrict __s, const char *__restrict __format, ...) __asm__ ("" "__isoc99_sscanf") __attribute__ ((__nothrow__ , __leaf__)); +extern int vfscanf (FILE *__restrict __s, const char *__restrict __format, + __gnuc_va_list __arg) + __attribute__ ((__format__ (__scanf__, 2, 0))) ; +extern int vscanf (const char *__restrict __format, __gnuc_va_list __arg) + __attribute__ ((__format__ (__scanf__, 1, 0))) ; +extern int vsscanf (const char *__restrict __s, + const char *__restrict __format, __gnuc_va_list __arg) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__format__ (__scanf__, 2, 0))); +extern int vfscanf (FILE *__restrict __s, const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vfscanf") + __attribute__ ((__format__ (__scanf__, 2, 0))) ; +extern int vscanf (const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vscanf") + __attribute__ ((__format__ (__scanf__, 1, 0))) ; +extern int vsscanf (const char *__restrict __s, const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vsscanf") __attribute__ ((__nothrow__ , __leaf__)) + __attribute__ ((__format__ (__scanf__, 2, 0))); +extern int fgetc (FILE *__stream); +extern int getc (FILE *__stream); +extern int getchar (void); +extern int getc_unlocked (FILE *__stream); +extern int getchar_unlocked (void); +extern int fgetc_unlocked (FILE *__stream); +extern int fputc (int __c, FILE *__stream); +extern int putc (int __c, FILE *__stream); +extern int putchar (int __c); +extern int fputc_unlocked (int __c, FILE *__stream); +extern int putc_unlocked (int __c, FILE *__stream); +extern int putchar_unlocked (int __c); +extern int getw (FILE *__stream); +extern int putw (int __w, FILE *__stream); +extern char *fgets (char *__restrict __s, int __n, FILE *__restrict __stream) + ; +extern __ssize_t __getdelim (char **__restrict __lineptr, + size_t *__restrict __n, int __delimiter, + FILE *__restrict __stream) ; +extern __ssize_t getdelim (char **__restrict __lineptr, + size_t *__restrict __n, int __delimiter, + FILE *__restrict __stream) ; +extern __ssize_t getline (char **__restrict __lineptr, + size_t *__restrict __n, + FILE *__restrict __stream) ; +extern int fputs (const char *__restrict __s, FILE *__restrict __stream); +extern int puts (const char *__s); +extern int ungetc (int __c, FILE *__stream); +extern size_t fread (void *__restrict __ptr, size_t __size, + size_t __n, FILE *__restrict __stream) ; +extern size_t fwrite (const void *__restrict __ptr, size_t __size, + size_t __n, FILE *__restrict __s); +extern size_t fread_unlocked (void *__restrict __ptr, size_t __size, + size_t __n, FILE *__restrict __stream) ; +extern size_t fwrite_unlocked (const void *__restrict __ptr, size_t __size, + size_t __n, FILE *__restrict __stream); +extern int fseek (FILE *__stream, long int __off, int __whence); +extern long int ftell (FILE *__stream) ; +extern void rewind (FILE *__stream); +extern int fseeko (FILE *__stream, __off_t __off, int __whence); +extern __off_t ftello (FILE *__stream) ; +extern int fgetpos (FILE *__restrict __stream, fpos_t *__restrict __pos); +extern int fsetpos (FILE *__stream, const fpos_t *__pos); +extern void clearerr (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)); +extern int feof (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern int ferror (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern void clearerr_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)); +extern int feof_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern int ferror_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern void perror (const char *__s); +extern int sys_nerr; +extern const char *const sys_errlist[]; +extern int fileno (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern int fileno_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern FILE *popen (const char *__command, const char *__modes) ; +extern int pclose (FILE *__stream); +extern char *ctermid (char *__s) __attribute__ ((__nothrow__ , __leaf__)); +extern void flockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)); +extern int ftrylockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern void funlockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)); +extern int __uflow (FILE *); +extern int __overflow (FILE *, int); + +void displayBits(unsigned int value); +unsigned int number1= 65535; +int mask = 1; +unsigned int x; +int c = 1; +int y; +int main(void) { + displayBits(mask); + displayBits(number1); + displayBits(number1 & mask); + y= c+mask; + return y; +} +void displayBits(unsigned int value) { + unsigned int displayMask = 1<<31; + printf("%10u = ", value); + while (c<=32) { + putchar(value & displayMask ? '1' : '0'); + value <<=1; + if (c % 8 == 0) { + putchar(' '); + } + mask = mask & 1; + c=c+mask; + } + putchar('\n'); +} diff --git a/c/termination-bwb/display-bit.yml b/c/termination-bwb/display-bit.yml new file mode 100644 index 00000000000..0ad9dca1ec4 --- /dev/null +++ b/c/termination-bwb/display-bit.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'display-bit.i' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/display-bit1.c b/c/termination-bwb/display-bit1.c new file mode 100644 index 00000000000..c2412a07276 --- /dev/null +++ b/c/termination-bwb/display-bit1.c @@ -0,0 +1,36 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + + +#include + +void displayBits(unsigned int value); +unsigned int number1= 65535; +int mask = 1; +unsigned int x; +int c = 1; +int y; +int main(void) { + /* printf("%s", "Engter a nonnegative int:"); */ + /* scanf("%u", &x); */ + unsigned int displayMask = 1<<31; + while (c<=32) { + /* putchar(number1 & displayMask ? '1' : '0'); */ + number1 <<=1; //shift left by 1 + if (c % 8 == 0) { + putchar(' '); + } + mask = mask & 1; + c=c+mask; + } + /* putchar('\n'); */ + y= 1; + return 0; +} diff --git a/c/termination-bwb/display-bit1.i b/c/termination-bwb/display-bit1.i new file mode 100644 index 00000000000..8d269cd74de --- /dev/null +++ b/c/termination-bwb/display-bit1.i @@ -0,0 +1,287 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +typedef long unsigned int size_t; +typedef __builtin_va_list __gnuc_va_list; +typedef unsigned char __u_char; +typedef unsigned short int __u_short; +typedef unsigned int __u_int; +typedef unsigned long int __u_long; +typedef signed char __int8_t; +typedef unsigned char __uint8_t; +typedef signed short int __int16_t; +typedef unsigned short int __uint16_t; +typedef signed int __int32_t; +typedef unsigned int __uint32_t; +typedef signed long int __int64_t; +typedef unsigned long int __uint64_t; +typedef __int8_t __int_least8_t; +typedef __uint8_t __uint_least8_t; +typedef __int16_t __int_least16_t; +typedef __uint16_t __uint_least16_t; +typedef __int32_t __int_least32_t; +typedef __uint32_t __uint_least32_t; +typedef __int64_t __int_least64_t; +typedef __uint64_t __uint_least64_t; +typedef long int __quad_t; +typedef unsigned long int __u_quad_t; +typedef long int __intmax_t; +typedef unsigned long int __uintmax_t; +typedef unsigned long int __dev_t; +typedef unsigned int __uid_t; +typedef unsigned int __gid_t; +typedef unsigned long int __ino_t; +typedef unsigned long int __ino64_t; +typedef unsigned int __mode_t; +typedef unsigned long int __nlink_t; +typedef long int __off_t; +typedef long int __off64_t; +typedef int __pid_t; +typedef struct { int __val[2]; } __fsid_t; +typedef long int __clock_t; +typedef unsigned long int __rlim_t; +typedef unsigned long int __rlim64_t; +typedef unsigned int __id_t; +typedef long int __time_t; +typedef unsigned int __useconds_t; +typedef long int __suseconds_t; +typedef int __daddr_t; +typedef int __key_t; +typedef int __clockid_t; +typedef void * __timer_t; +typedef long int __blksize_t; +typedef long int __blkcnt_t; +typedef long int __blkcnt64_t; +typedef unsigned long int __fsblkcnt_t; +typedef unsigned long int __fsblkcnt64_t; +typedef unsigned long int __fsfilcnt_t; +typedef unsigned long int __fsfilcnt64_t; +typedef long int __fsword_t; +typedef long int __ssize_t; +typedef long int __syscall_slong_t; +typedef unsigned long int __syscall_ulong_t; +typedef __off64_t __loff_t; +typedef char *__caddr_t; +typedef long int __intptr_t; +typedef unsigned int __socklen_t; +typedef int __sig_atomic_t; +typedef struct +{ + int __count; + union + { + unsigned int __wch; + char __wchb[4]; + } __value; +} __mbstate_t; +typedef struct _G_fpos_t +{ + __off_t __pos; + __mbstate_t __state; +} __fpos_t; +typedef struct _G_fpos64_t +{ + __off64_t __pos; + __mbstate_t __state; +} __fpos64_t; +struct _IO_FILE; +typedef struct _IO_FILE __FILE; +struct _IO_FILE; +typedef struct _IO_FILE FILE; +struct _IO_FILE; +struct _IO_marker; +struct _IO_codecvt; +struct _IO_wide_data; +typedef void _IO_lock_t; +struct _IO_FILE +{ + int _flags; + char *_IO_read_ptr; + char *_IO_read_end; + char *_IO_read_base; + char *_IO_write_base; + char *_IO_write_ptr; + char *_IO_write_end; + char *_IO_buf_base; + char *_IO_buf_end; + char *_IO_save_base; + char *_IO_backup_base; + char *_IO_save_end; + struct _IO_marker *_markers; + struct _IO_FILE *_chain; + int _fileno; + int _flags2; + __off_t _old_offset; + unsigned short _cur_column; + signed char _vtable_offset; + char _shortbuf[1]; + _IO_lock_t *_lock; + __off64_t _offset; + struct _IO_codecvt *_codecvt; + struct _IO_wide_data *_wide_data; + struct _IO_FILE *_freeres_list; + void *_freeres_buf; + size_t __pad5; + int _mode; + char _unused2[15 * sizeof (int) - 4 * sizeof (void *) - sizeof (size_t)]; +}; +typedef __gnuc_va_list va_list; +typedef __off_t off_t; +typedef __ssize_t ssize_t; +typedef __fpos_t fpos_t; +extern FILE *stdin; +extern FILE *stdout; +extern FILE *stderr; +extern int remove (const char *__filename) __attribute__ ((__nothrow__ , __leaf__)); +extern int rename (const char *__old, const char *__new) __attribute__ ((__nothrow__ , __leaf__)); +extern int renameat (int __oldfd, const char *__old, int __newfd, + const char *__new) __attribute__ ((__nothrow__ , __leaf__)); +extern FILE *tmpfile (void) ; +extern char *tmpnam (char *__s) __attribute__ ((__nothrow__ , __leaf__)) ; +extern char *tmpnam_r (char *__s) __attribute__ ((__nothrow__ , __leaf__)) ; +extern char *tempnam (const char *__dir, const char *__pfx) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ; +extern int fclose (FILE *__stream); +extern int fflush (FILE *__stream); +extern int fflush_unlocked (FILE *__stream); +extern FILE *fopen (const char *__restrict __filename, + const char *__restrict __modes) ; +extern FILE *freopen (const char *__restrict __filename, + const char *__restrict __modes, + FILE *__restrict __stream) ; +extern FILE *fdopen (int __fd, const char *__modes) __attribute__ ((__nothrow__ , __leaf__)) ; +extern FILE *fmemopen (void *__s, size_t __len, const char *__modes) + __attribute__ ((__nothrow__ , __leaf__)) ; +extern FILE *open_memstream (char **__bufloc, size_t *__sizeloc) __attribute__ ((__nothrow__ , __leaf__)) ; +extern void setbuf (FILE *__restrict __stream, char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__)); +extern int setvbuf (FILE *__restrict __stream, char *__restrict __buf, + int __modes, size_t __n) __attribute__ ((__nothrow__ , __leaf__)); +extern void setbuffer (FILE *__restrict __stream, char *__restrict __buf, + size_t __size) __attribute__ ((__nothrow__ , __leaf__)); +extern void setlinebuf (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)); +extern int fprintf (FILE *__restrict __stream, + const char *__restrict __format, ...); +extern int printf (const char *__restrict __format, ...); +extern int sprintf (char *__restrict __s, + const char *__restrict __format, ...) __attribute__ ((__nothrow__)); +extern int vfprintf (FILE *__restrict __s, const char *__restrict __format, + __gnuc_va_list __arg); +extern int vprintf (const char *__restrict __format, __gnuc_va_list __arg); +extern int vsprintf (char *__restrict __s, const char *__restrict __format, + __gnuc_va_list __arg) __attribute__ ((__nothrow__)); +extern int snprintf (char *__restrict __s, size_t __maxlen, + const char *__restrict __format, ...) + __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 4))); +extern int vsnprintf (char *__restrict __s, size_t __maxlen, + const char *__restrict __format, __gnuc_va_list __arg) + __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 0))); +extern int vdprintf (int __fd, const char *__restrict __fmt, + __gnuc_va_list __arg) + __attribute__ ((__format__ (__printf__, 2, 0))); +extern int dprintf (int __fd, const char *__restrict __fmt, ...) + __attribute__ ((__format__ (__printf__, 2, 3))); +extern int fscanf (FILE *__restrict __stream, + const char *__restrict __format, ...) ; +extern int scanf (const char *__restrict __format, ...) ; +extern int sscanf (const char *__restrict __s, + const char *__restrict __format, ...) __attribute__ ((__nothrow__ , __leaf__)); +extern int fscanf (FILE *__restrict __stream, const char *__restrict __format, ...) __asm__ ("" "__isoc99_fscanf") ; +extern int scanf (const char *__restrict __format, ...) __asm__ ("" "__isoc99_scanf") ; +extern int sscanf (const char *__restrict __s, const char *__restrict __format, ...) __asm__ ("" "__isoc99_sscanf") __attribute__ ((__nothrow__ , __leaf__)); +extern int vfscanf (FILE *__restrict __s, const char *__restrict __format, + __gnuc_va_list __arg) + __attribute__ ((__format__ (__scanf__, 2, 0))) ; +extern int vscanf (const char *__restrict __format, __gnuc_va_list __arg) + __attribute__ ((__format__ (__scanf__, 1, 0))) ; +extern int vsscanf (const char *__restrict __s, + const char *__restrict __format, __gnuc_va_list __arg) + __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__format__ (__scanf__, 2, 0))); +extern int vfscanf (FILE *__restrict __s, const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vfscanf") + __attribute__ ((__format__ (__scanf__, 2, 0))) ; +extern int vscanf (const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vscanf") + __attribute__ ((__format__ (__scanf__, 1, 0))) ; +extern int vsscanf (const char *__restrict __s, const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vsscanf") __attribute__ ((__nothrow__ , __leaf__)) + __attribute__ ((__format__ (__scanf__, 2, 0))); +extern int fgetc (FILE *__stream); +extern int getc (FILE *__stream); +extern int getchar (void); +extern int getc_unlocked (FILE *__stream); +extern int getchar_unlocked (void); +extern int fgetc_unlocked (FILE *__stream); +extern int fputc (int __c, FILE *__stream); +extern int putc (int __c, FILE *__stream); +extern int putchar (int __c); +extern int fputc_unlocked (int __c, FILE *__stream); +extern int putc_unlocked (int __c, FILE *__stream); +extern int putchar_unlocked (int __c); +extern int getw (FILE *__stream); +extern int putw (int __w, FILE *__stream); +extern char *fgets (char *__restrict __s, int __n, FILE *__restrict __stream) + ; +extern __ssize_t __getdelim (char **__restrict __lineptr, + size_t *__restrict __n, int __delimiter, + FILE *__restrict __stream) ; +extern __ssize_t getdelim (char **__restrict __lineptr, + size_t *__restrict __n, int __delimiter, + FILE *__restrict __stream) ; +extern __ssize_t getline (char **__restrict __lineptr, + size_t *__restrict __n, + FILE *__restrict __stream) ; +extern int fputs (const char *__restrict __s, FILE *__restrict __stream); +extern int puts (const char *__s); +extern int ungetc (int __c, FILE *__stream); +extern size_t fread (void *__restrict __ptr, size_t __size, + size_t __n, FILE *__restrict __stream) ; +extern size_t fwrite (const void *__restrict __ptr, size_t __size, + size_t __n, FILE *__restrict __s); +extern size_t fread_unlocked (void *__restrict __ptr, size_t __size, + size_t __n, FILE *__restrict __stream) ; +extern size_t fwrite_unlocked (const void *__restrict __ptr, size_t __size, + size_t __n, FILE *__restrict __stream); +extern int fseek (FILE *__stream, long int __off, int __whence); +extern long int ftell (FILE *__stream) ; +extern void rewind (FILE *__stream); +extern int fseeko (FILE *__stream, __off_t __off, int __whence); +extern __off_t ftello (FILE *__stream) ; +extern int fgetpos (FILE *__restrict __stream, fpos_t *__restrict __pos); +extern int fsetpos (FILE *__stream, const fpos_t *__pos); +extern void clearerr (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)); +extern int feof (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern int ferror (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern void clearerr_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)); +extern int feof_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern int ferror_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern void perror (const char *__s); +extern int sys_nerr; +extern const char *const sys_errlist[]; +extern int fileno (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern int fileno_unlocked (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern FILE *popen (const char *__command, const char *__modes) ; +extern int pclose (FILE *__stream); +extern char *ctermid (char *__s) __attribute__ ((__nothrow__ , __leaf__)); +extern void flockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)); +extern int ftrylockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)) ; +extern void funlockfile (FILE *__stream) __attribute__ ((__nothrow__ , __leaf__)); +extern int __uflow (FILE *); +extern int __overflow (FILE *, int); + +void displayBits(unsigned int value); +unsigned int number1= 65535; +int mask = 1; +unsigned int x; +int c = 1; +int y; +int main(void) { + unsigned int displayMask = 1<<31; + while (c<=32) { + number1 <<=1; + if (c % 8 == 0) { + putchar(' '); + } + mask = mask & 1; + c=c+mask; + } + y= 1; + return 0; +} diff --git a/c/termination-bwb/display-bit1.yml b/c/termination-bwb/display-bit1.yml new file mode 100644 index 00000000000..bca696d9b99 --- /dev/null +++ b/c/termination-bwb/display-bit1.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'display-bit1.i' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/not-01.c b/c/termination-bwb/not-01.c new file mode 100644 index 00000000000..b528f706611 --- /dev/null +++ b/c/termination-bwb/not-01.c @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); + +int main(){ + int a, x; + x = __VERIFIER_nondet_int(); + a = __VERIFIER_nondet_int(); + while (x>0){ + a = ~a; + if (a>0){ + x = x - a; + } + else { + x = x + a; + } + } +} diff --git a/c/termination-bwb/not-01.yml b/c/termination-bwb/not-01.yml new file mode 100644 index 00000000000..db4cfd4d8a4 --- /dev/null +++ b/c/termination-bwb/not-01.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'not-01.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/not-02-false.c b/c/termination-bwb/not-02-false.c new file mode 100644 index 00000000000..fb5c8d44900 --- /dev/null +++ b/c/termination-bwb/not-02-false.c @@ -0,0 +1,23 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); + +int main(){ + int a, x, y; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + a = 1; + while (x<0){ + y = ~a; + x = y; + + } +} diff --git a/c/termination-bwb/not-02-false.yml b/c/termination-bwb/not-02-false.yml new file mode 100644 index 00000000000..e4d8a428eb3 --- /dev/null +++ b/c/termination-bwb/not-02-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'not-02-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/not-02.c b/c/termination-bwb/not-02.c new file mode 100644 index 00000000000..13ced38bd16 --- /dev/null +++ b/c/termination-bwb/not-02.c @@ -0,0 +1,23 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); + +int main(){ + int a, x, y; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + a = 1; + while (x!=0 && y!=0){ + a =x; + x = y; + y = ~a; + } +} diff --git a/c/termination-bwb/not-02.yml b/c/termination-bwb/not-02.yml new file mode 100644 index 00000000000..f00d5341012 --- /dev/null +++ b/c/termination-bwb/not-02.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'not-02.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/not-03-false.c b/c/termination-bwb/not-03-false.c new file mode 100644 index 00000000000..762b1e79ae7 --- /dev/null +++ b/c/termination-bwb/not-03-false.c @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); + +int main(){ + int a, x, y; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + + while (x > 0 && y < 0){ + if (x > y){ + y = ~x; + } else { + x = x-1; + } + } + return 0; +} diff --git a/c/termination-bwb/not-03-false.yml b/c/termination-bwb/not-03-false.yml new file mode 100644 index 00000000000..e021d41a8bd --- /dev/null +++ b/c/termination-bwb/not-03-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'not-03-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/not-03.c b/c/termination-bwb/not-03.c new file mode 100644 index 00000000000..dad25135a3f --- /dev/null +++ b/c/termination-bwb/not-03.c @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); + +int main(){ + int a, x, y; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + + while (x > 0 && y > 0){ + if (x > y){ + y = ~x; + } else { + x = x-1; + } + } + return 0; +} diff --git a/c/termination-bwb/not-03.yml b/c/termination-bwb/not-03.yml new file mode 100644 index 00000000000..4b87364c372 --- /dev/null +++ b/c/termination-bwb/not-03.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'not-03.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/not-04-false.c b/c/termination-bwb/not-04-false.c new file mode 100644 index 00000000000..2244104108f --- /dev/null +++ b/c/termination-bwb/not-04-false.c @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); + +int main(){ + int a, x, y; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + a = 0; + while (x<0){ + if (x < 0 && y>= 0){ + x = ~y; + } else { + x = x-1; + } + } + return 0; +} diff --git a/c/termination-bwb/not-04-false.yml b/c/termination-bwb/not-04-false.yml new file mode 100644 index 00000000000..0245f3b3a23 --- /dev/null +++ b/c/termination-bwb/not-04-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'not-04-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/not-04.c b/c/termination-bwb/not-04.c new file mode 100644 index 00000000000..82b3eeffac9 --- /dev/null +++ b/c/termination-bwb/not-04.c @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); + +int main(){ + int a, x, y; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + a = 0; + while (y != 0){ + if (x <= 0 || y<= 0){ + y = 0; + } else { + x = ~y; + } + } + return 0; +} diff --git a/c/termination-bwb/not-04.yml b/c/termination-bwb/not-04.yml new file mode 100644 index 00000000000..e8adee34686 --- /dev/null +++ b/c/termination-bwb/not-04.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'not-04.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/not-05-false.c b/c/termination-bwb/not-05-false.c new file mode 100644 index 00000000000..96b92b13c85 --- /dev/null +++ b/c/termination-bwb/not-05-false.c @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); + +int main(){ + int a, x, y; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + a = 0; + while (y > 0){ + if (x < 0 ){ + y = ~x ; + } else { + y = y -1; + } + } + return 0; +} diff --git a/c/termination-bwb/not-05-false.yml b/c/termination-bwb/not-05-false.yml new file mode 100644 index 00000000000..e32693af9b0 --- /dev/null +++ b/c/termination-bwb/not-05-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'not-05-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/not-05.c b/c/termination-bwb/not-05.c new file mode 100644 index 00000000000..eb50881dac9 --- /dev/null +++ b/c/termination-bwb/not-05.c @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); + +int main(){ + int a, x, y; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + a = 0; + while (y > 0){ + if (x > 0 ){ + y = ~x ; + } else { + y = y -1; + } + } + return 0; +} diff --git a/c/termination-bwb/not-05.yml b/c/termination-bwb/not-05.yml new file mode 100644 index 00000000000..d939d8e8c2f --- /dev/null +++ b/c/termination-bwb/not-05.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'not-05.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/or-01-false.c b/c/termination-bwb/or-01-false.c new file mode 100644 index 00000000000..47b17d92542 --- /dev/null +++ b/c/termination-bwb/or-01-false.c @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + + +int __VERIFIER_nondet_int(); + +int main (){ + int a, b; + int x; + a = 16; + b = 30; + x = __VERIFIER_nondet_int(); + + while (x>=0){ + b = b|a; + x= x+b; + } + return 0; +} diff --git a/c/termination-bwb/or-01-false.yml b/c/termination-bwb/or-01-false.yml new file mode 100644 index 00000000000..3ffe8ae875b --- /dev/null +++ b/c/termination-bwb/or-01-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'or-01-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/or-01.c b/c/termination-bwb/or-01.c new file mode 100644 index 00000000000..492015849af --- /dev/null +++ b/c/termination-bwb/or-01.c @@ -0,0 +1,27 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + + +int __VERIFIER_nondet_int(); + +int main (){ + int a, b; + int x; + a = 16; + b = 30; + x = __VERIFIER_nondet_int(); + + while (x>0){ + a++; + b = b|a; + x= x-b; + } + return 0; +} diff --git a/c/termination-bwb/or-01.yml b/c/termination-bwb/or-01.yml new file mode 100644 index 00000000000..7e8196da144 --- /dev/null +++ b/c/termination-bwb/or-01.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'or-01.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/or-02-false.c b/c/termination-bwb/or-02-false.c new file mode 100644 index 00000000000..f493fd37586 --- /dev/null +++ b/c/termination-bwb/or-02-false.c @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + + +int __VERIFIER_nondet_int(); + +int main (){ + int b; + int x; + b = 30; + x = __VERIFIER_nondet_int(); + + while (x>0){ + b= b+1; + b = b|1; + x= x+b; + } + return 0; +} diff --git a/c/termination-bwb/or-02-false.yml b/c/termination-bwb/or-02-false.yml new file mode 100644 index 00000000000..286bfb22c48 --- /dev/null +++ b/c/termination-bwb/or-02-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'or-02-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/or-02.c b/c/termination-bwb/or-02.c new file mode 100644 index 00000000000..3290fdcb5ac --- /dev/null +++ b/c/termination-bwb/or-02.c @@ -0,0 +1,25 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + + +int __VERIFIER_nondet_int(); + +int main (){ + int b; + int x; + b = 30; + x = __VERIFIER_nondet_int(); + + while (x>0){ + b= b|(b+1); + x= x-b; + } + return 0; +} diff --git a/c/termination-bwb/or-02.yml b/c/termination-bwb/or-02.yml new file mode 100644 index 00000000000..b76327de070 --- /dev/null +++ b/c/termination-bwb/or-02.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'or-02.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/or-03.c b/c/termination-bwb/or-03.c new file mode 100644 index 00000000000..ac9ac768ae1 --- /dev/null +++ b/c/termination-bwb/or-03.c @@ -0,0 +1,25 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +//unsigned int __VERIFIER_nondet_int(); + +int __VERIFIER_nondet_int(); + +int main (){ + int y; + int x; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + while (x >= y && y>0){ + y = x|(x+1); + x = x-y; + } + return 0; +} diff --git a/c/termination-bwb/or-03.yml b/c/termination-bwb/or-03.yml new file mode 100644 index 00000000000..4cfd4504e3a --- /dev/null +++ b/c/termination-bwb/or-03.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'or-03.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/or-04.c b/c/termination-bwb/or-04.c new file mode 100644 index 00000000000..952ba39a7bc --- /dev/null +++ b/c/termination-bwb/or-04.c @@ -0,0 +1,33 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +//unsigned int __VERIFIER_nondet_int(); + +int __VERIFIER_nondet_int(); + +int main (){ + int y; + int x; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + while (x >= y && y>0){ + while (y!=0){ + if (y>0) { + y = y|(y+1); + y = x-y; + } + else { + y= y+1; + x= x+1; + } + } + } + return 0; +} diff --git a/c/termination-bwb/or-04.yml b/c/termination-bwb/or-04.yml new file mode 100644 index 00000000000..cc00e8a0305 --- /dev/null +++ b/c/termination-bwb/or-04.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'or-04.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/or-05-false.c b/c/termination-bwb/or-05-false.c new file mode 100644 index 00000000000..fce5d1fecd3 --- /dev/null +++ b/c/termination-bwb/or-05-false.c @@ -0,0 +1,30 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +//unsigned int __VERIFIER_nondet_int(); + +int __VERIFIER_nondet_int(); + +int main (){ + int y; + int x; + x = __VERIFIER_nondet_int(); + y = 0; + while (x>0){ + if (y==1){ + x=y|(y+1); + x=x+y; + } else { + y=1; + x = x+y; + } + } + return 0; +} diff --git a/c/termination-bwb/or-05-false.yml b/c/termination-bwb/or-05-false.yml new file mode 100644 index 00000000000..87e7c3bfb51 --- /dev/null +++ b/c/termination-bwb/or-05-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'or-05-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/or-05.c b/c/termination-bwb/or-05.c new file mode 100644 index 00000000000..28196f9bac2 --- /dev/null +++ b/c/termination-bwb/or-05.c @@ -0,0 +1,31 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +//unsigned int __VERIFIER_nondet_int(); + +int __VERIFIER_nondet_int(); + +int main (){ + int y; + int x; + x = __VERIFIER_nondet_int(); + y = 0; + while (x>0){ + if (y==1){ + x=y|(y+1); + x=x-y; + } + else { + y=1; + x = x-y; + } + } + return 0; +} diff --git a/c/termination-bwb/or-05.yml b/c/termination-bwb/or-05.yml new file mode 100644 index 00000000000..ebd04bdd0aa --- /dev/null +++ b/c/termination-bwb/or-05.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'or-05.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/or-06.c b/c/termination-bwb/or-06.c new file mode 100644 index 00000000000..a0c048af4a4 --- /dev/null +++ b/c/termination-bwb/or-06.c @@ -0,0 +1,25 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +//unsigned int __VERIFIER_nondet_int(); + +int __VERIFIER_nondet_int(); + +int main (){ + int y; + int x; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + while (x >= y && y>0){ + x = y|(y+1); + y = y-x; + } + return 0; +} diff --git a/c/termination-bwb/or-06.yml b/c/termination-bwb/or-06.yml new file mode 100644 index 00000000000..f7193a97cdd --- /dev/null +++ b/c/termination-bwb/or-06.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'or-06.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/parity.c b/c/termination-bwb/parity.c new file mode 100644 index 00000000000..c21524613e2 --- /dev/null +++ b/c/termination-bwb/parity.c @@ -0,0 +1,37 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +#include + +extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); + +int v, y, parity; // word value to compute the parity of +/* bool parity; // parity will be the parity of v */ +int main(){ + /* parity = false; */ + void* z; + z = (void*)0; + parity = 0; + y= __VERIFIER_nondet_int(); + v = __VERIFIER_nondet_int(); + + while (v>0) + { + /* parity = !parity; */ + parity = 1-parity; + v = v & (v - 1); + } + if (v>=0){ + y = v+1; + } else { + y = 1; + } + return 0; +} diff --git a/c/termination-bwb/parity.i b/c/termination-bwb/parity.i new file mode 100644 index 00000000000..6580cb831d8 --- /dev/null +++ b/c/termination-bwb/parity.i @@ -0,0 +1,24 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); +int v, y, parity; +int main(){ + void* z; + z = (void*)0; + parity = 0; + y= __VERIFIER_nondet_int(); + v = __VERIFIER_nondet_int(); + while (v>0) + { + parity = 1-parity; + v = v & (v - 1); + } + if (v>=0){ + y = v+1; + } else { + y = 1; + } + return 0; +} diff --git a/c/termination-bwb/parity.yml b/c/termination-bwb/parity.yml new file mode 100644 index 00000000000..98ace4f432a --- /dev/null +++ b/c/termination-bwb/parity.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'parity.i' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/parity1.c b/c/termination-bwb/parity1.c new file mode 100644 index 00000000000..fcba891e39e --- /dev/null +++ b/c/termination-bwb/parity1.c @@ -0,0 +1,36 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + + +#include + +extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +int v, y, parity; // word value to compute the parity of + +/* bool parity; // parity will be the parity of v */ +int main(){ + /* parity = false; */ + + void* z; + z = (void*)0; + parity = 0; + y= __VERIFIER_nondet_int(); + v= __VERIFIER_nondet_int(); + + if (v<0) v= (-1)*v; + while (v>0) + { + parity++; + v = v & (v - 1); + } + + return 0; +} diff --git a/c/termination-bwb/parity1.i b/c/termination-bwb/parity1.i new file mode 100644 index 00000000000..2404a33627a --- /dev/null +++ b/c/termination-bwb/parity1.i @@ -0,0 +1,21 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +int v, y, parity; +int main(){ + void* z; + z = (void*)0; + parity = 0; + y= __VERIFIER_nondet_int(); + v= __VERIFIER_nondet_int(); + if (v<0) v= (-1)*v; + while (v>0) + { + parity++; + v = v & (v - 1); + } + return 0; +} diff --git a/c/termination-bwb/parity1.yml b/c/termination-bwb/parity1.yml new file mode 100644 index 00000000000..b22e1e7c541 --- /dev/null +++ b/c/termination-bwb/parity1.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'parity1.i' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/readme.md b/c/termination-bwb/readme.md new file mode 100644 index 00000000000..fc5ba555796 --- /dev/null +++ b/c/termination-bwb/readme.md @@ -0,0 +1,14 @@ + + +The benchmarks in this directory were submitted by Yuandong Cyrus Liu(yliu195@stevens.edu). + +C programs with bitvector operations for termination analysis with bitwise braching, part of practical code snippets adopted from +[bithacks optimization](https://graphics.stanford.edu/~seander/bithacks.html), these benchmarks were used in the `DarkSea` work: + +- Yuandong Cyrus Liu, Chengbin Pang, Daniel Dietsch, Eric Koskinen, Ton-Chanh Le, Georgios Portokalidis, and Jun Xu. Proving LTL Properties of Bitvector Programs and Decompiled Binaries. The 19th Asian Symposium on Programming Languages and Systems (APLAS), 2021. + +You may use and redistribute them according to the license that is shipped with these examples. diff --git a/c/termination-bwb/reverse-bits1.c b/c/termination-bwb/reverse-bits1.c new file mode 100644 index 00000000000..619b7535fe4 --- /dev/null +++ b/c/termination-bwb/reverse-bits1.c @@ -0,0 +1,48 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +#include + +extern unsigned int __VERIFIER_nondet_unsigned() __attribute__ ((__noreturn__)); +extern int __VERIFIER_nondet_int () __attribute__ ((__noreturn__)); + +int v; // input bits to be reversed +int r; // r will be reversed bits of v; first get LSB of v +/* int s = sizeof(v) * CHAR_BIT - 1; // extra shift needed at end */ +int s = sizeof(v) * 8 - 1; // extra shift needed at end + +int z, y, x, n; // word value to compute the parity of + +int main(){ + v = __VERIFIER_nondet_int(); + n = __VERIFIER_nondet_int(); + z = __VERIFIER_nondet_int(); + x = __VERIFIER_nondet_int(); + r = v; + y = v-1; + while (x&(v-y-1)) { + y=1; + } + v >>= 1; + while (v>0) { + r <<= 1; + z = v&1; + r = r|z ; + s--; + v >>= 1; + } + + n=-1; + + if (s>=0){ + r <<= s; // shift when v's highest bits are zero + } + return 0; +} diff --git a/c/termination-bwb/reverse-bits1.i b/c/termination-bwb/reverse-bits1.i new file mode 100644 index 00000000000..bda5436cf04 --- /dev/null +++ b/c/termination-bwb/reverse-bits1.i @@ -0,0 +1,34 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +extern unsigned int __VERIFIER_nondet_unsigned() __attribute__ ((__noreturn__)); +extern int __VERIFIER_nondet_int () __attribute__ ((__noreturn__)); +int v; +int r; +int s = sizeof(v) * 8 - 1; +int z, y, x, n; +int main(){ + v = __VERIFIER_nondet_int(); + n = __VERIFIER_nondet_int(); + z = __VERIFIER_nondet_int(); + x = __VERIFIER_nondet_int(); + r = v; + y = v-1; + while (x&(v-y-1)) { + y=1; + } + v >>= 1; + while (v>0) { + r <<= 1; + z = v&1; + r = r|z ; + s--; + v >>= 1; + } + n=-1; + if (s>=0){ + r <<= s; + } + return 0; +} diff --git a/c/termination-bwb/reverse-bits1.yml b/c/termination-bwb/reverse-bits1.yml new file mode 100644 index 00000000000..abeff87a7b9 --- /dev/null +++ b/c/termination-bwb/reverse-bits1.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'reverse-bits1.i' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/xor-01-false.c b/c/termination-bwb/xor-01-false.c new file mode 100644 index 00000000000..352e170c727 --- /dev/null +++ b/c/termination-bwb/xor-01-false.c @@ -0,0 +1,31 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); + +int main (){ + int a, b, x; + a = __VERIFIER_nondet_int(); + x = __VERIFIER_nondet_int(); + b = 0; + while (x>0){ + if (a >= 0){ + /* a++; */ + a = 0^1; + x= x+a; + } + else { + x = x-1; + a =1; + } + } + return 0; +} + diff --git a/c/termination-bwb/xor-01-false.yml b/c/termination-bwb/xor-01-false.yml new file mode 100644 index 00000000000..21bf024b6c6 --- /dev/null +++ b/c/termination-bwb/xor-01-false.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'xor-01-false.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: false +options: + language: C + data_model: LP64 diff --git a/c/termination-bwb/xor-01.c b/c/termination-bwb/xor-01.c new file mode 100644 index 00000000000..5f868ebbc89 --- /dev/null +++ b/c/termination-bwb/xor-01.c @@ -0,0 +1,30 @@ +// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +// +// SPDX-License-Identifier: Apache-2.0 + +/* + * Date: 2021-06-21 + * Author: yliu195@stevens.edu + */ + + +int __VERIFIER_nondet_int(); + +int main (){ + int a, b, x; + a = __VERIFIER_nondet_int(); + x = __VERIFIER_nondet_int(); + b = 0; + while (x>0){ + if (a >= 0){ + /* a++; */ + a = 0^1; + x= x-a; + } + else { + x = x-1; + } + } + return 0; +} + diff --git a/c/termination-bwb/xor-01.yml b/c/termination-bwb/xor-01.yml new file mode 100644 index 00000000000..a6a8871be57 --- /dev/null +++ b/c/termination-bwb/xor-01.yml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu +# +# SPDX-License-Identifier: Apache-2.0 + +format_version: '2.0' +input_files: 'xor-01.c' +properties: + - property_file: ../properties/termination.prp + expected_verdict: true +options: + language: C + data_model: LP64