Darksea's bitwise termination bechmarks used in aplas21 paper.

c/termination-bwb/Makefile

@@ -0,0 +1,14 @@
+# SPDX-FileCopyrightText: 2015-2016 Daniel Liew <[email protected]>
+# SPDX-FileCopyrightText: 2015-2020 The SV-Benchmarks Community
+# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+LEVEL := ../
+
+CC.Arch := 64
+
+COMMON_WARNINGS := \
+	-Wno-error=return-type \
+
+include $(LEVEL)/Makefile.config

c/termination-bwb/and-01-false.c

@@ -0,0 +1,22 @@
+// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/*
+ * Date: 2021-06-21
+ * Author: [email protected]
+ */
+
+
+int __VERIFIER_nondet();
+
+int main (){
+  int a, x;
+  x = __VERIFIER_nondet();
+  a = 34;
+  while (x==0){
+    a--;
+    x=x&a;
+  }
+  return 0;
+}

c/termination-bwb/and-01-false.yml

@@ -0,0 +1,12 @@
+# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+#
+# 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

c/termination-bwb/and-01.c

@@ -0,0 +1,25 @@
+// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/*
+ * Date: 2021-06-21
+ * Author: [email protected]
+ */
+
+
+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;
+}

c/termination-bwb/and-01.yml

@@ -0,0 +1,12 @@
+# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+#
+# 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

c/termination-bwb/and-02-false.c

@@ -0,0 +1,28 @@
+// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/*
+ * Date: 2021-06-21
+ * Author: [email protected]
+ */
+
+
+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;
+}

c/termination-bwb/and-02-false.yml

@@ -0,0 +1,12 @@
+# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+#
+# 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

c/termination-bwb/and-02.c

@@ -0,0 +1,28 @@
+// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/*
+ * Date: 2021-06-21
+ * Author: [email protected]
+ */
+
+
+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;
+}

c/termination-bwb/and-02.yml

@@ -0,0 +1,12 @@
+# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+#
+# 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

c/termination-bwb/and-03-false.c

@@ -0,0 +1,26 @@
+// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/*
+ * Date: 2021-06-21
+ * Author: [email protected]
+ */
+
+
+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;
+}

c/termination-bwb/and-03-false.yml

@@ -0,0 +1,12 @@
+# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+#
+# 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

c/termination-bwb/and-03.c

@@ -0,0 +1,26 @@
+// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/*
+ * Date: 2021-06-21
+ * Author: [email protected]
+ */
+
+
+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;
+}

c/termination-bwb/and-03.yml

@@ -0,0 +1,12 @@
+# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+#
+# 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

c/termination-bwb/and-04-false.c

@@ -0,0 +1,25 @@
+// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/*
+ * Date: 2021-06-21
+ * Author: [email protected]
+ */
+
+
+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;
+}

c/termination-bwb/and-04-false.yml

@@ -0,0 +1,12 @@
+# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+#
+# 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

c/termination-bwb/and-04.c

@@ -0,0 +1,25 @@
+// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/*
+ * Date: 2021-06-21
+ * Author: [email protected]
+ */
+
+
+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;
+}

c/termination-bwb/and-04.yml

@@ -0,0 +1,12 @@
+# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+#
+# 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

c/termination-bwb/and-05-false.c

@@ -0,0 +1,21 @@
+// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/*
+ * Date: 2021-06-21
+ * Author: [email protected]
+ */
+
+
+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;
+}

c/termination-bwb/and-05-false.yml

@@ -0,0 +1,12 @@
+# SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+#
+# 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

c/termination-bwb/and-05.c

@@ -0,0 +1,21 @@
+// SPDX-FileCopyrightText: 2021 Y. Cyrus Liu <[email protected]>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/*
+ * Date: 2021-06-21
+ * Author: [email protected]
+ */
+
+
+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;
+}