udpate expected

UQ-PAC · Nov 28, 2023 · 678e3d3 · 678e3d3
1 parent c04a1f1
commit 678e3d3
Show file tree

Hide file tree

Showing 349 changed files with 7,386 additions and 5,021 deletions.
diff --git a/src/test/correct/arrays_simple/clang/arrays_simple.expected b/src/test/correct/arrays_simple/clang/arrays_simple.expected
@@ -194,5 +194,11 @@ procedure main()
     assume {:captureState "%000008b7"} true;
     R0, Gamma_R0 := 0bv64, true;
     R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/arrays_simple/clang_O2/arrays_simple.expected b/src/test/correct/arrays_simple/clang_O2/arrays_simple.expected
@@ -157,5 +157,11 @@ procedure main()
   lmain:
     assume {:captureState "lmain"} true;
     R0, Gamma_R0 := 0bv64, true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/arrays_simple/clang_no_plt_no_pic/arrays_simple.expected b/src/test/correct/arrays_simple/clang_no_plt_no_pic/arrays_simple.expected
@@ -194,5 +194,11 @@ procedure main()
     assume {:captureState "%000008b7"} true;
     R0, Gamma_R0 := 0bv64, true;
     R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/arrays_simple/clang_pic/arrays_simple.expected b/src/test/correct/arrays_simple/clang_pic/arrays_simple.expected
@@ -194,5 +194,11 @@ procedure main()
     assume {:captureState "%000008b7"} true;
     R0, Gamma_R0 := 0bv64, true;
     R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/arrays_simple/gcc_O2/arrays_simple.expected b/src/test/correct/arrays_simple/gcc_O2/arrays_simple.expected
@@ -157,5 +157,11 @@ procedure main()
   lmain:
     assume {:captureState "lmain"} true;
     R0, Gamma_R0 := 0bv64, true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_read/clang/basic_arrays_read.expected b/src/test/correct/basic_arrays_read/clang/basic_arrays_read.expected
@@ -203,5 +203,11 @@ procedure main()
     call rely();
     R0, Gamma_R0 := zero_extend32_32(memory_load32_le(mem, bvadd64(R8, 52bv64))), (gamma_load32(Gamma_mem, bvadd64(R8, 52bv64)) || L(mem, bvadd64(R8, 52bv64)));
     R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_read/clang_O2/basic_arrays_read.expected b/src/test/correct/basic_arrays_read/clang_O2/basic_arrays_read.expected
@@ -187,5 +187,11 @@ procedure main()
     mem, Gamma_mem := memory_store32_le(mem, bvadd64(R8, 52bv64), 0bv32), gamma_store32(Gamma_mem, bvadd64(R8, 52bv64), true);
     assert true;
     assume {:captureState "%000002c9"} true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_read/clang_no_plt_no_pic/basic_arrays_read.expected b/src/test/correct/basic_arrays_read/clang_no_plt_no_pic/basic_arrays_read.expected
@@ -203,5 +203,11 @@ procedure main()
     call rely();
     R0, Gamma_R0 := zero_extend32_32(memory_load32_le(mem, bvadd64(R8, 52bv64))), (gamma_load32(Gamma_mem, bvadd64(R8, 52bv64)) || L(mem, bvadd64(R8, 52bv64)));
     R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_read/clang_pic/basic_arrays_read.expected b/src/test/correct/basic_arrays_read/clang_pic/basic_arrays_read.expected
@@ -237,5 +237,11 @@ procedure main()
     call rely();
     R0, Gamma_R0 := zero_extend32_32(memory_load32_le(mem, R8)), (gamma_load32(Gamma_mem, R8) || L(mem, R8));
     R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_read/gcc/basic_arrays_read.expected b/src/test/correct/basic_arrays_read/gcc/basic_arrays_read.expected
@@ -194,5 +194,11 @@ procedure main()
     R0, Gamma_R0 := bvadd64(R0, 24bv64), Gamma_R0;
     call rely();
     R0, Gamma_R0 := zero_extend32_32(memory_load32_le(mem, R0)), (gamma_load32(Gamma_mem, R0) || L(mem, R0));
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_read/gcc_O2/basic_arrays_read.expected b/src/test/correct/basic_arrays_read/gcc_O2/basic_arrays_read.expected
@@ -187,5 +187,11 @@ procedure main()
     mem, Gamma_mem := memory_store32_le(mem, bvadd64(R1, 24bv64), 0bv32), gamma_store32(Gamma_mem, bvadd64(R1, 24bv64), true);
     assert true;
     assume {:captureState "%000001b7"} true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_read/gcc_no_plt_no_pic/basic_arrays_read.expected b/src/test/correct/basic_arrays_read/gcc_no_plt_no_pic/basic_arrays_read.expected
@@ -194,5 +194,11 @@ procedure main()
     R0, Gamma_R0 := bvadd64(R0, 24bv64), Gamma_R0;
     call rely();
     R0, Gamma_R0 := zero_extend32_32(memory_load32_le(mem, R0)), (gamma_load32(Gamma_mem, R0) || L(mem, R0));
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_read/gcc_pic/basic_arrays_read.expected b/src/test/correct/basic_arrays_read/gcc_pic/basic_arrays_read.expected
@@ -228,5 +228,11 @@ procedure main()
     R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R0, 4080bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4080bv64)) || L(mem, bvadd64(R0, 4080bv64)));
     call rely();
     R0, Gamma_R0 := zero_extend32_32(memory_load32_le(mem, R0)), (gamma_load32(Gamma_mem, R0) || L(mem, R0));
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_write/clang/basic_arrays_write.expected b/src/test/correct/basic_arrays_write/clang/basic_arrays_write.expected
@@ -209,5 +209,11 @@ procedure main()
     assume {:captureState "%000002f4"} true;
     R0, Gamma_R0 := 0bv64, true;
     R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_write/clang_O2/basic_arrays_write.expected b/src/test/correct/basic_arrays_write/clang_O2/basic_arrays_write.expected
@@ -194,5 +194,11 @@ procedure main()
     mem, Gamma_mem := memory_store32_le(mem, bvadd64(R9, 56bv64), R8[32:0]), gamma_store32(Gamma_mem, bvadd64(R9, 56bv64), Gamma_R8);
     assert (arr$0_old == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
     assume {:captureState "%000002d4"} true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_write/clang_no_plt_no_pic/basic_arrays_write.expected b/src/test/correct/basic_arrays_write/clang_no_plt_no_pic/basic_arrays_write.expected
@@ -209,5 +209,11 @@ procedure main()
     assume {:captureState "%0000089f"} true;
     R0, Gamma_R0 := 0bv64, true;
     R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_write/clang_pic/basic_arrays_write.expected b/src/test/correct/basic_arrays_write/clang_pic/basic_arrays_write.expected
@@ -242,5 +242,11 @@ procedure main()
     assume {:captureState "%000002f5"} true;
     R0, Gamma_R0 := 0bv64, true;
     R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_write/gcc/basic_arrays_write.expected b/src/test/correct/basic_arrays_write/gcc/basic_arrays_write.expected
@@ -207,5 +207,11 @@ procedure main()
     assume {:captureState "%000002f4"} true;
     R0, Gamma_R0 := 0bv64, true;
     R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_write/gcc_O2/basic_arrays_write.expected b/src/test/correct/basic_arrays_write/gcc_O2/basic_arrays_write.expected
@@ -194,5 +194,11 @@ procedure main()
     mem, Gamma_mem := memory_store32_le(mem, bvadd64(R1, 28bv64), R2[32:0]), gamma_store32(Gamma_mem, bvadd64(R1, 28bv64), Gamma_R2);
     assert (arr$0_old == memory_load32_le(mem, bvadd64($arr_addr, 0bv64)));
     assume {:captureState "%000001be"} true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_write/gcc_no_plt_no_pic/basic_arrays_write.expected b/src/test/correct/basic_arrays_write/gcc_no_plt_no_pic/basic_arrays_write.expected
@@ -207,5 +207,11 @@ procedure main()
     assume {:captureState "%0000089f"} true;
     R0, Gamma_R0 := 0bv64, true;
     R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_arrays_write/gcc_pic/basic_arrays_write.expected b/src/test/correct/basic_arrays_write/gcc_pic/basic_arrays_write.expected
@@ -240,5 +240,11 @@ procedure main()
     assume {:captureState "%000002f5"} true;
     R0, Gamma_R0 := 0bv64, true;
     R31, Gamma_R31 := bvadd64(R31, 16bv64), Gamma_R31;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_assign_assign/clang/basic_assign_assign.expected b/src/test/correct/basic_assign_assign/clang/basic_assign_assign.expected
@@ -194,5 +194,11 @@ procedure main()
     assert ((memory_load32_le(mem, $x_addr) == x_old) || (memory_load32_le(mem, $x_addr) == 5bv32));
     assume {:captureState "%000002ce"} true;
     R0, Gamma_R0 := 0bv64, true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_assign_assign/clang_O2/basic_assign_assign.expected b/src/test/correct/basic_assign_assign/clang_O2/basic_assign_assign.expected
@@ -194,5 +194,11 @@ procedure main()
     mem, Gamma_mem := memory_store32_le(mem, bvadd64(R8, 52bv64), R9[32:0]), gamma_store32(Gamma_mem, bvadd64(R8, 52bv64), Gamma_R9);
     assert ((memory_load32_le(mem, $x_addr) == x_old) || (memory_load32_le(mem, $x_addr) == 5bv32));
     assume {:captureState "%000002d3"} true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_assign_assign/clang_no_plt_no_pic/basic_assign_assign.expected b/src/test/correct/basic_assign_assign/clang_no_plt_no_pic/basic_assign_assign.expected
@@ -194,5 +194,11 @@ procedure main()
     assert ((memory_load32_le(mem, $x_addr) == x_old) || (memory_load32_le(mem, $x_addr) == 5bv32));
     assume {:captureState "%00000845"} true;
     R0, Gamma_R0 := 0bv64, true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_assign_assign/clang_pic/basic_assign_assign.expected b/src/test/correct/basic_assign_assign/clang_pic/basic_assign_assign.expected
@@ -228,5 +228,11 @@ procedure main()
     assert ((memory_load32_le(mem, $x_addr) == x_old) || (memory_load32_le(mem, $x_addr) == 5bv32));
     assume {:captureState "%000002d9"} true;
     R0, Gamma_R0 := 0bv64, true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_assign_assign/gcc/basic_assign_assign.expected b/src/test/correct/basic_assign_assign/gcc/basic_assign_assign.expected
@@ -193,5 +193,11 @@ procedure main()
     assert ((memory_load32_le(mem, $x_addr) == x_old) || (memory_load32_le(mem, $x_addr) == 5bv32));
     assume {:captureState "%000002d8"} true;
     R0, Gamma_R0 := 0bv64, true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_assign_assign/gcc_O2/basic_assign_assign.expected b/src/test/correct/basic_assign_assign/gcc_O2/basic_assign_assign.expected
@@ -194,5 +194,11 @@ procedure main()
     mem, Gamma_mem := memory_store32_le(mem, bvadd64(R1, 20bv64), R2[32:0]), gamma_store32(Gamma_mem, bvadd64(R1, 20bv64), Gamma_R2);
     assert ((memory_load32_le(mem, $x_addr) == x_old) || (memory_load32_le(mem, $x_addr) == 5bv32));
     assume {:captureState "%000001bd"} true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_assign_assign/gcc_no_plt_no_pic/basic_assign_assign.expected b/src/test/correct/basic_assign_assign/gcc_no_plt_no_pic/basic_assign_assign.expected
@@ -193,5 +193,11 @@ procedure main()
     assert ((memory_load32_le(mem, $x_addr) == x_old) || (memory_load32_le(mem, $x_addr) == 5bv32));
     assume {:captureState "%0000085b"} true;
     R0, Gamma_R0 := 0bv64, true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_assign_assign/gcc_pic/basic_assign_assign.expected b/src/test/correct/basic_assign_assign/gcc_pic/basic_assign_assign.expected
@@ -226,5 +226,11 @@ procedure main()
     assert ((memory_load32_le(mem, $x_addr) == x_old) || (memory_load32_le(mem, $x_addr) == 5bv32));
     assume {:captureState "%000002d9"} true;
     R0, Gamma_R0 := 0bv64, true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_assign_increment/clang/basic_assign_increment.expected b/src/test/correct/basic_assign_increment/clang/basic_assign_increment.expected
@@ -202,5 +202,11 @@ procedure main()
     assert (((memory_load32_le(mem, $x_addr) == x_old) || (memory_load32_le(mem, $x_addr) == 1bv32)) || (memory_load32_le(mem, $x_addr) == 6bv32));
     assume {:captureState "%000002da"} true;
     R0, Gamma_R0 := 0bv64, true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_assign_increment/clang_O2/basic_assign_increment.expected b/src/test/correct/basic_assign_increment/clang_O2/basic_assign_increment.expected
@@ -202,5 +202,11 @@ procedure main()
     mem, Gamma_mem := memory_store32_le(mem, bvadd64(R8, 52bv64), R9[32:0]), gamma_store32(Gamma_mem, bvadd64(R8, 52bv64), Gamma_R9);
     assert (((memory_load32_le(mem, $x_addr) == x_old) || (memory_load32_le(mem, $x_addr) == 1bv32)) || (memory_load32_le(mem, $x_addr) == 6bv32));
     assume {:captureState "%000002df"} true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_assign_increment/clang_no_plt_no_pic/basic_assign_increment.expected b/src/test/correct/basic_assign_increment/clang_no_plt_no_pic/basic_assign_increment.expected
@@ -202,5 +202,11 @@ procedure main()
     assert (((memory_load32_le(mem, $x_addr) == x_old) || (memory_load32_le(mem, $x_addr) == 1bv32)) || (memory_load32_le(mem, $x_addr) == 6bv32));
     assume {:captureState "%0000085f"} true;
     R0, Gamma_R0 := 0bv64, true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
diff --git a/src/test/correct/basic_assign_increment/clang_pic/basic_assign_increment.expected b/src/test/correct/basic_assign_increment/clang_pic/basic_assign_increment.expected
@@ -236,5 +236,11 @@ procedure main()
     assert (((memory_load32_le(mem, $x_addr) == x_old) || (memory_load32_le(mem, $x_addr) == 1bv32)) || (memory_load32_le(mem, $x_addr) == 6bv32));
     assume {:captureState "%000002e5"} true;
     R0, Gamma_R0 := 0bv64, true;
+    goto main_return;
+  terminate:
+    assume {:captureState "terminate"} true;
+    goto terminate;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }