update expected

UQ-PAC · Feb 3, 2025 · 6ead689 · 6ead689
1 parent deb7cf5
commit 6ead689
Show file tree

Hide file tree

Showing 185 changed files with 1,937 additions and 1,937 deletions.
diff --git a/src/test/correct/arrays_simple/clang/arrays_simple.expected b/src/test/correct/arrays_simple/clang/arrays_simple.expected
@@ -79,8 +79,8 @@ implementation main()
 {
   var $load$18: bv32;
   var Gamma_$load$18: bool;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R31, Gamma_R31 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
     R8, Gamma_R8 := 3bv64, true;
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 20bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 20bv64), Gamma_R8);

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
@@ -92,8 +92,8 @@ implementation main()
 {
   var $load$18: bv32;
   var Gamma_$load$18: bool;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R31, Gamma_R31 := bvadd64(R31, 18446744073709551600bv64), Gamma_R31;
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 12bv64), 0bv32), gamma_store32(Gamma_stack, bvadd64(R31, 12bv64), true);
     assume {:captureState "%000002d1"} true;

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
@@ -101,8 +101,8 @@ implementation main()
   var $load$19: bv32;
   var Gamma_$load$18: bool;
   var Gamma_$load$19: bool;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R31, Gamma_R31 := bvadd64(R31, 18446744073709551600bv64), Gamma_R31;
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 12bv64), 0bv32), gamma_store32(Gamma_stack, bvadd64(R31, 12bv64), true);
     assume {:captureState "%000002d5"} true;

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
@@ -84,8 +84,8 @@ implementation main()
 {
   var $load$18: bv32;
   var Gamma_$load$18: bool;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R0, Gamma_R0 := 69632bv64, true;
     R0, Gamma_R0 := bvadd64(R0, 24bv64), Gamma_R0;
     call rely();

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
@@ -95,8 +95,8 @@ implementation main()
   var Gamma_$load$18: bool;
   var Gamma_$load$19: bool;
   var Gamma_$load$20: bool;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R0, Gamma_R0 := 65536bv64, true;
     call rely();
     $load$18, Gamma_$load$18 := memory_load64_le(mem, bvadd64(R0, 4080bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4080bv64)) || L(mem, bvadd64(R0, 4080bv64)));

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
@@ -96,8 +96,8 @@ implementation main()
   var $load$18: bv32;
   var Gamma_$load$18: bool;
   var arr$0_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R31, Gamma_R31 := bvadd64(R31, 18446744073709551600bv64), Gamma_R31;
     R9, Gamma_R9 := 69632bv64, true;
     R9, Gamma_R9 := bvadd64(R9, 52bv64), Gamma_R9;

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
@@ -84,8 +84,8 @@ procedure main();
 implementation main()
 {
   var arr$0_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R8, Gamma_R8 := zero_extend32_32(R0[32:0]), Gamma_R0;
     R9, Gamma_R9 := 69632bv64, true;
     R0, Gamma_R0 := 0bv64, true;

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
@@ -105,8 +105,8 @@ implementation main()
   var Gamma_$load$18: bool;
   var Gamma_$load$19: bool;
   var arr$0_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R31, Gamma_R31 := bvadd64(R31, 18446744073709551600bv64), Gamma_R31;
     R9, Gamma_R9 := 65536bv64, true;
     call rely();

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
@@ -94,8 +94,8 @@ implementation main()
   var $load$18: bv32;
   var Gamma_$load$18: bool;
   var arr$0_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R31, Gamma_R31 := bvadd64(R31, 18446744073709551600bv64), Gamma_R31;
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 12bv64), R0[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 12bv64), Gamma_R0);
     assume {:captureState "%000002da"} true;

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
@@ -84,8 +84,8 @@ procedure main();
 implementation main()
 {
   var arr$0_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R1, Gamma_R1 := 69632bv64, true;
     R2, Gamma_R2 := zero_extend32_32(R0[32:0]), Gamma_R0;
     R0, Gamma_R0 := 0bv64, true;

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
@@ -103,8 +103,8 @@ implementation main()
   var Gamma_$load$18: bool;
   var Gamma_$load$19: bool;
   var arr$0_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R31, Gamma_R31 := bvadd64(R31, 18446744073709551600bv64), Gamma_R31;
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 12bv64), R0[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 12bv64), Gamma_R0);
     assume {:captureState "%000002da"} true;

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
@@ -84,8 +84,8 @@ procedure main();
 implementation main()
 {
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R9, Gamma_R9 := 69632bv64, true;
     R8, Gamma_R8 := 5bv64, true;
     call rely();

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
@@ -93,8 +93,8 @@ implementation main()
   var $load$18: bv64;
   var Gamma_$load$18: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R9, Gamma_R9 := 65536bv64, true;
     call rely();
     $load$18, Gamma_$load$18 := memory_load64_le(mem, bvadd64(R9, 4040bv64)), (gamma_load64(Gamma_mem, bvadd64(R9, 4040bv64)) || L(mem, bvadd64(R9, 4040bv64)));

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
@@ -82,8 +82,8 @@ procedure main();
 implementation main()
 {
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R0, Gamma_R0 := 69632bv64, true;
     R0, Gamma_R0 := bvadd64(R0, 20bv64), Gamma_R0;
     R1, Gamma_R1 := 5bv64, true;

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
@@ -84,8 +84,8 @@ procedure main();
 implementation main()
 {
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R1, Gamma_R1 := 69632bv64, true;
     R2, Gamma_R2 := 5bv64, true;
     R0, Gamma_R0 := 0bv64, true;

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
@@ -91,8 +91,8 @@ implementation main()
   var $load$18: bv64;
   var Gamma_$load$18: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R0, Gamma_R0 := 65536bv64, true;
     call rely();
     $load$18, Gamma_$load$18 := memory_load64_le(mem, bvadd64(R0, 4064bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4064bv64)) || L(mem, bvadd64(R0, 4064bv64)));

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
@@ -92,8 +92,8 @@ implementation main()
   var $load$18: bv32;
   var Gamma_$load$18: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R9, Gamma_R9 := 69632bv64, true;
     call rely();
     $load$18, Gamma_$load$18 := memory_load32_le(mem, bvadd64(R9, 52bv64)), (gamma_load32(Gamma_mem, bvadd64(R9, 52bv64)) || L(mem, bvadd64(R9, 52bv64)));

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
@@ -101,8 +101,8 @@ implementation main()
   var Gamma_$load$18: bool;
   var Gamma_$load$19: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R9, Gamma_R9 := 65536bv64, true;
     call rely();
     $load$18, Gamma_$load$18 := memory_load64_le(mem, bvadd64(R9, 4040bv64)), (gamma_load64(Gamma_mem, bvadd64(R9, 4040bv64)) || L(mem, bvadd64(R9, 4040bv64)));

diff --git a/src/test/correct/basic_assign_increment/gcc/basic_assign_increment.expected b/src/test/correct/basic_assign_increment/gcc/basic_assign_increment.expected
@@ -90,8 +90,8 @@ implementation main()
   var $load$18: bv32;
   var Gamma_$load$18: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R0, Gamma_R0 := 69632bv64, true;
     R0, Gamma_R0 := bvadd64(R0, 20bv64), Gamma_R0;
     call rely();

diff --git a/src/test/correct/basic_assign_increment/gcc_O2/basic_assign_increment.expected b/src/test/correct/basic_assign_increment/gcc_O2/basic_assign_increment.expected
@@ -92,8 +92,8 @@ implementation main()
   var $load$18: bv32;
   var Gamma_$load$18: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R2, Gamma_R2 := 69632bv64, true;
     R0, Gamma_R0 := 0bv64, true;
     call rely();

diff --git a/src/test/correct/basic_assign_increment/gcc_pic/basic_assign_increment.expected b/src/test/correct/basic_assign_increment/gcc_pic/basic_assign_increment.expected
@@ -101,8 +101,8 @@ implementation main()
   var Gamma_$load$19: bool;
   var Gamma_$load$20: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R0, Gamma_R0 := 65536bv64, true;
     call rely();
     $load$18, Gamma_$load$18 := memory_load64_le(mem, bvadd64(R0, 4064bv64)), (gamma_load64(Gamma_mem, bvadd64(R0, 4064bv64)) || L(mem, bvadd64(R0, 4064bv64)));

diff --git a/src/test/correct/basic_function_call_caller/clang/basic_function_call_caller.expected b/src/test/correct/basic_function_call_caller/clang/basic_function_call_caller.expected
@@ -129,8 +129,8 @@ implementation main()
   var Gamma_$load$20: bool;
   var Gamma_y_old: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R31, Gamma_R31 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
     #4, Gamma_#4 := bvadd64(R31, 16bv64), Gamma_R31;
     stack, Gamma_stack := memory_store64_le(stack, #4, R29), gamma_store64(Gamma_stack, #4, Gamma_R29);
@@ -142,9 +142,9 @@ implementation main()
     assume {:captureState "%00000318"} true;
     R30, Gamma_R30 := 1840bv64, true;
     call zero();
-    goto l00000321;
-  l00000321:
-    assume {:captureState "l00000321"} true;
+    goto $00000321;
+  $00000321:
+    assume {:captureState "$00000321"} true;
     R8, Gamma_R8 := 69632bv64, true;
     call rely();
     assert (L(mem, bvadd64(R8, 52bv64)) ==> Gamma_R0);
@@ -196,8 +196,8 @@ procedure zero();
 
 implementation zero()
 {
-  lzero:
-    assume {:captureState "lzero"} true;
+  $zero:
+    assume {:captureState "$zero"} true;
     R0, Gamma_R0 := 0bv64, true;
     goto zero_basil_return;
   zero_basil_return:

diff --git a/src/test/correct/basic_function_call_caller/clang_O2/basic_function_call_caller.expected b/src/test/correct/basic_function_call_caller/clang_O2/basic_function_call_caller.expected
@@ -97,8 +97,8 @@ implementation main()
 {
   var Gamma_y_old: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R8, Gamma_R8 := zero_extend32_32(R0[32:0]), Gamma_R0;
     R0, Gamma_R0 := 0bv64, true;
     R9, Gamma_R9 := 69632bv64, true;

diff --git a/src/test/correct/basic_function_call_caller/clang_pic/basic_function_call_caller.expected b/src/test/correct/basic_function_call_caller/clang_pic/basic_function_call_caller.expected
@@ -139,8 +139,8 @@ implementation main()
   var Gamma_$load$22: bool;
   var Gamma_y_old: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R31, Gamma_R31 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
     #4, Gamma_#4 := bvadd64(R31, 16bv64), Gamma_R31;
     stack, Gamma_stack := memory_store64_le(stack, #4, R29), gamma_store64(Gamma_stack, #4, Gamma_R29);
@@ -152,9 +152,9 @@ implementation main()
     assume {:captureState "%00000320"} true;
     R30, Gamma_R30 := 1904bv64, true;
     call zero();
-    goto l00000329;
-  l00000329:
-    assume {:captureState "l00000329"} true;
+    goto $00000329;
+  $00000329:
+    assume {:captureState "$00000329"} true;
     R8, Gamma_R8 := 65536bv64, true;
     call rely();
     $load$18, Gamma_$load$18 := memory_load64_le(mem, bvadd64(R8, 4032bv64)), (gamma_load64(Gamma_mem, bvadd64(R8, 4032bv64)) || L(mem, bvadd64(R8, 4032bv64)));
@@ -216,8 +216,8 @@ procedure zero();
 
 implementation zero()
 {
-  lzero:
-    assume {:captureState "lzero"} true;
+  $zero:
+    assume {:captureState "$zero"} true;
     R0, Gamma_R0 := 0bv64, true;
     goto zero_basil_return;
   zero_basil_return:

diff --git a/src/test/correct/basic_function_call_caller/gcc/basic_function_call_caller.expected b/src/test/correct/basic_function_call_caller/gcc/basic_function_call_caller.expected
@@ -125,8 +125,8 @@ implementation main()
   var Gamma_$load$20: bool;
   var Gamma_y_old: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     #4, Gamma_#4 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
     stack, Gamma_stack := memory_store64_le(stack, #4, R29), gamma_store64(Gamma_stack, #4, Gamma_R29);
     assume {:captureState "%00000302"} true;
@@ -138,9 +138,9 @@ implementation main()
     assume {:captureState "%0000031a"} true;
     R30, Gamma_R30 := 1836bv64, true;
     call zero();
-    goto l00000323;
-  l00000323:
-    assume {:captureState "l00000323"} true;
+    goto $00000323;
+  $00000323:
+    assume {:captureState "$00000323"} true;
     R1, Gamma_R1 := zero_extend32_32(R0[32:0]), Gamma_R0;
     R0, Gamma_R0 := 69632bv64, true;
     R0, Gamma_R0 := bvadd64(R0, 20bv64), Gamma_R0;
@@ -194,8 +194,8 @@ procedure zero();
 
 implementation zero()
 {
-  lzero:
-    assume {:captureState "lzero"} true;
+  $zero:
+    assume {:captureState "$zero"} true;
     R0, Gamma_R0 := 0bv64, true;
     goto zero_basil_return;
   zero_basil_return:

diff --git a/src/test/correct/basic_function_call_caller/gcc_O2/basic_function_call_caller.expected b/src/test/correct/basic_function_call_caller/gcc_O2/basic_function_call_caller.expected
@@ -97,8 +97,8 @@ implementation main()
 {
   var Gamma_y_old: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     R1, Gamma_R1 := 69632bv64, true;
     R2, Gamma_R2 := bvadd64(R1, 20bv64), Gamma_R1;
     R3, Gamma_R3 := zero_extend32_32(R0[32:0]), Gamma_R0;

diff --git a/src/test/correct/basic_function_call_caller/gcc_pic/basic_function_call_caller.expected b/src/test/correct/basic_function_call_caller/gcc_pic/basic_function_call_caller.expected
@@ -135,8 +135,8 @@ implementation main()
   var Gamma_$load$22: bool;
   var Gamma_y_old: bool;
   var x_old: bv32;
-  lmain:
-    assume {:captureState "lmain"} true;
+  $main:
+    assume {:captureState "$main"} true;
     #4, Gamma_#4 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
     stack, Gamma_stack := memory_store64_le(stack, #4, R29), gamma_store64(Gamma_stack, #4, Gamma_R29);
     assume {:captureState "%00000302"} true;
@@ -148,9 +148,9 @@ implementation main()
     assume {:captureState "%0000031a"} true;
     R30, Gamma_R30 := 1900bv64, true;
     call zero();
-    goto l00000323;
-  l00000323:
-    assume {:captureState "l00000323"} true;
+    goto $00000323;
+  $00000323:
+    assume {:captureState "$00000323"} true;
     R1, Gamma_R1 := zero_extend32_32(R0[32:0]), Gamma_R0;
     R0, Gamma_R0 := 65536bv64, true;
     call rely();
@@ -212,8 +212,8 @@ procedure zero();
 
 implementation zero()
 {
-  lzero:
-    assume {:captureState "lzero"} true;
+  $zero:
+    assume {:captureState "$zero"} true;
     R0, Gamma_R0 := 0bv64, true;
     goto zero_basil_return;
   zero_basil_return: