update expected

UQ-PAC · Jan 24, 2024 · 2b088f3 · 2b088f3
1 parent fa65d14
commit 2b088f3
Show file tree

Hide file tree

Showing 6 changed files with 14 additions and 6 deletions.
diff --git a/src/test/correct/indirect_call/gcc_O2/indirect_call.expected b/src/test/correct/indirect_call/gcc_O2/indirect_call.expected
@@ -236,12 +236,10 @@ implementation greet()
     R0, Gamma_R0 := 0bv64, true;
     R0, Gamma_R0 := bvadd64(R0, 1992bv64), Gamma_R0;
     call puts();
-    //no return target
-    assume false;
+    assume false; //no return target
   greet_return:
     assume {:captureState "greet_return"} true;
     return;
-
 }
 
 procedure main();

diff --git a/...rrect/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected b/...rrect/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected
@@ -273,6 +273,9 @@ implementation main()
     R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31);
     R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
     R31, Gamma_R31 := bvadd64(R31, 48bv64), Gamma_R31;
+    goto main_return;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
 

diff --git a/...correct/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected b/...correct/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected
@@ -273,6 +273,9 @@ implementation main()
     R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31);
     R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
     R31, Gamma_R31 := bvadd64(R31, 48bv64), Gamma_R31;
+    goto main_return;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
 

diff --git a/src/test/correct/malloc_with_local3/gcc_O2/malloc_with_local3.expected b/src/test/correct/malloc_with_local3/gcc_O2/malloc_with_local3.expected
@@ -1061,11 +1061,9 @@ implementation printCharValue()
     mem, Gamma_mem := memory_store8_le(mem, R3, R2[8:0]), gamma_store8(Gamma_mem, R3, Gamma_R2);
     assume {:captureState "%00000293"} true;
     call __printf_chk();
-    //no return target
-    assume false;
+    assume false; //no return target
   printCharValue_return:
     assume {:captureState "printCharValue_return"} true;
     return;
-
 }
 
diff --git a/...rrect/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected b/...rrect/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected
@@ -289,6 +289,9 @@ implementation main()
     R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31);
     R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
     R31, Gamma_R31 := bvadd64(R31, 48bv64), Gamma_R31;
+    goto main_return;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }
 

diff --git a/...correct/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected b/...correct/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected
@@ -287,6 +287,9 @@ implementation main()
     R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31);
     R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64));
     R31, Gamma_R31 := bvadd64(R31, 48bv64), Gamma_R31;
+    goto main_return;
+  main_return:
+    assume {:captureState "main_return"} true;
     return;
 }