update GTIRB expected which were out of date

UQ-PAC · Sep 18, 2024 · acd0377 · acd0377
1 parent 6d49c85
commit acd0377
Show file tree

Hide file tree

Showing 25 changed files with 48 additions and 48 deletions.
diff --git a/src/test/correct/basicfree/clang/basicfree_gtirb.expected b/src/test/correct/basicfree/clang/basicfree_gtirb.expected
@@ -110,7 +110,7 @@ implementation FUN_650()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 16bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 16bv64)) || L(mem, bvadd64(R16, 16bv64)));
     R16, Gamma_R16 := bvadd64(R16, 16bv64), Gamma_R16;
     call malloc();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_680();
@@ -141,7 +141,7 @@ implementation FUN_680()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 40bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 40bv64)) || L(mem, bvadd64(R16, 40bv64)));
     R16, Gamma_R16 := bvadd64(R16, 40bv64), Gamma_R16;
     call #free();
-    assume false; //no return target
+    assume false;
 }
 
 procedure main();

diff --git a/src/test/correct/basicfree/gcc/basicfree_gtirb.expected b/src/test/correct/basicfree/gcc/basicfree_gtirb.expected
@@ -108,7 +108,7 @@ implementation FUN_680()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4040bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4040bv64)) || L(mem, bvadd64(R16, 4040bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4040bv64), Gamma_R16;
     call #free();
-    assume false; //no return target
+    assume false;
 }
 
 procedure main();
@@ -206,7 +206,7 @@ implementation FUN_650()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4016bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4016bv64)) || L(mem, bvadd64(R16, 4016bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4016bv64), Gamma_R16;
     call malloc();
-    assume false; //no return target
+    assume false;
 }
 
 procedure #free();

diff --git a/src/test/correct/function1/clang/function1_gtirb.expected b/src/test/correct/function1/clang/function1_gtirb.expected
@@ -205,7 +205,7 @@ implementation FUN_630()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 32bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 32bv64)) || L(mem, bvadd64(R16, 32bv64)));
     R16, Gamma_R16 := bvadd64(R16, 32bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure get_two();

diff --git a/src/test/correct/function1/clang_O2/function1_gtirb.expected b/src/test/correct/function1/clang_O2/function1_gtirb.expected
@@ -108,7 +108,7 @@ implementation FUN_630()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 32bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 32bv64)) || L(mem, bvadd64(R16, 32bv64)));
     R16, Gamma_R16 := bvadd64(R16, 32bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure main();

diff --git a/src/test/correct/function1/gcc/function1_gtirb.expected b/src/test/correct/function1/gcc/function1_gtirb.expected
@@ -140,7 +140,7 @@ implementation FUN_630()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4040bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4040bv64)) || L(mem, bvadd64(R16, 4040bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4040bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure get_two();

diff --git a/src/test/correct/function1/gcc_O2/function1_gtirb.expected b/src/test/correct/function1/gcc_O2/function1_gtirb.expected
@@ -190,7 +190,7 @@ implementation FUN_620()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4024bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4024bv64)) || L(mem, bvadd64(R16, 4024bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4024bv64), Gamma_R16;
     call __printf_chk();
-    assume false; //no return target
+    assume false;
 }
 
 procedure __printf_chk();

diff --git a/src/test/correct/indirect_call/clang/indirect_call_gtirb.expected b/src/test/correct/indirect_call/clang/indirect_call_gtirb.expected
@@ -144,7 +144,7 @@ implementation FUN_630()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 32bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 32bv64)) || L(mem, bvadd64(R16, 32bv64)));
     R16, Gamma_R16 := bvadd64(R16, 32bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure greet();

diff --git a/src/test/correct/indirect_call/clang_pic/indirect_call_gtirb.expected b/src/test/correct/indirect_call/clang_pic/indirect_call_gtirb.expected
@@ -241,7 +241,7 @@ implementation FUN_650()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 32bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 32bv64)) || L(mem, bvadd64(R16, 32bv64)));
     R16, Gamma_R16 := bvadd64(R16, 32bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure greet();

diff --git a/src/test/correct/indirect_call/gcc/indirect_call_gtirb.expected b/src/test/correct/indirect_call/gcc/indirect_call_gtirb.expected
@@ -116,7 +116,7 @@ implementation FUN_630()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4040bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4040bv64)) || L(mem, bvadd64(R16, 4040bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4040bv64), Gamma_R16;
     call puts();
-    assume false; //no return target
+    assume false;
 }
 
 procedure greet();

diff --git a/src/test/correct/indirect_call/gcc_pic/indirect_call_gtirb.expected b/src/test/correct/indirect_call/gcc_pic/indirect_call_gtirb.expected
@@ -185,7 +185,7 @@ implementation FUN_650()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4032bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4032bv64)) || L(mem, bvadd64(R16, 4032bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4032bv64), Gamma_R16;
     call puts();
-    assume false; //no return target
+    assume false;
 }
 
 procedure main();

diff --git a/src/test/correct/malloc_with_local/clang/malloc_with_local_gtirb.expected b/src/test/correct/malloc_with_local/clang/malloc_with_local_gtirb.expected
@@ -146,7 +146,7 @@ implementation FUN_680()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 16bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 16bv64)) || L(mem, bvadd64(R16, 16bv64)));
     R16, Gamma_R16 := bvadd64(R16, 16bv64), Gamma_R16;
     call malloc();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_6b0();
@@ -185,7 +185,7 @@ implementation FUN_6b0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 40bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 40bv64)) || L(mem, bvadd64(R16, 40bv64)));
     R16, Gamma_R16 := bvadd64(R16, 40bv64), Gamma_R16;
     call #free();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_6c0();
@@ -224,7 +224,7 @@ implementation FUN_6c0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 48bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 48bv64)) || L(mem, bvadd64(R16, 48bv64)));
     R16, Gamma_R16 := bvadd64(R16, 48bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure main();

diff --git a/src/test/correct/malloc_with_local/clang_O2/malloc_with_local_gtirb.expected b/src/test/correct/malloc_with_local/clang_O2/malloc_with_local_gtirb.expected
@@ -133,7 +133,7 @@ implementation FUN_630()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 32bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 32bv64)) || L(mem, bvadd64(R16, 32bv64)));
     R16, Gamma_R16 := bvadd64(R16, 32bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure main();

diff --git a/src/test/correct/malloc_with_local/gcc/malloc_with_local_gtirb.expected b/src/test/correct/malloc_with_local/gcc/malloc_with_local_gtirb.expected
@@ -154,7 +154,7 @@ implementation FUN_680()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4008bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4008bv64)) || L(mem, bvadd64(R16, 4008bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4008bv64), Gamma_R16;
     call malloc();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_6b0();
@@ -201,7 +201,7 @@ implementation FUN_6b0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4032bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4032bv64)) || L(mem, bvadd64(R16, 4032bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4032bv64), Gamma_R16;
     call #free();
-    assume false; //no return target
+    assume false;
 }
 
 procedure main();
@@ -385,7 +385,7 @@ implementation FUN_6c0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4040bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4040bv64)) || L(mem, bvadd64(R16, 4040bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4040bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure malloc();

diff --git a/src/test/correct/malloc_with_local/gcc_O2/malloc_with_local_gtirb.expected b/src/test/correct/malloc_with_local/gcc_O2/malloc_with_local_gtirb.expected
@@ -126,7 +126,7 @@ implementation FUN_620()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4024bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4024bv64)) || L(mem, bvadd64(R16, 4024bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4024bv64), Gamma_R16;
     call __printf_chk();
-    assume false; //no return target
+    assume false;
 }
 
 procedure main();

diff --git a/src/test/correct/malloc_with_local2/clang/malloc_with_local2_gtirb.expected b/src/test/correct/malloc_with_local2/clang/malloc_with_local2_gtirb.expected
@@ -167,7 +167,7 @@ implementation FUN_6c0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 48bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 48bv64)) || L(mem, bvadd64(R16, 48bv64)));
     R16, Gamma_R16 := bvadd64(R16, 48bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure main();
@@ -386,7 +386,7 @@ implementation FUN_6b0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 40bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 40bv64)) || L(mem, bvadd64(R16, 40bv64)));
     R16, Gamma_R16 := bvadd64(R16, 40bv64), Gamma_R16;
     call #free();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_680();
@@ -439,7 +439,7 @@ implementation FUN_680()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 16bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 16bv64)) || L(mem, bvadd64(R16, 16bv64)));
     R16, Gamma_R16 := bvadd64(R16, 16bv64), Gamma_R16;
     call malloc();
-    assume false; //no return target
+    assume false;
 }
 
 procedure printf();

diff --git a/src/test/correct/malloc_with_local2/gcc/malloc_with_local2_gtirb.expected b/src/test/correct/malloc_with_local2/gcc/malloc_with_local2_gtirb.expected
@@ -305,7 +305,7 @@ implementation FUN_6b0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4032bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4032bv64)) || L(mem, bvadd64(R16, 4032bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4032bv64), Gamma_R16;
     call #free();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_6c0();
@@ -352,7 +352,7 @@ implementation FUN_6c0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4040bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4040bv64)) || L(mem, bvadd64(R16, 4040bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4040bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_680();
@@ -399,7 +399,7 @@ implementation FUN_680()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4008bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4008bv64)) || L(mem, bvadd64(R16, 4008bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4008bv64), Gamma_R16;
     call malloc();
-    assume false; //no return target
+    assume false;
 }
 
 procedure #free();

diff --git a/src/test/correct/malloc_with_local3/clang/malloc_with_local3_gtirb.expected b/src/test/correct/malloc_with_local3/clang/malloc_with_local3_gtirb.expected
@@ -165,7 +165,7 @@ implementation FUN_6c0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 48bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 48bv64)) || L(mem, bvadd64(R16, 48bv64)));
     R16, Gamma_R16 := bvadd64(R16, 48bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure main();
@@ -376,7 +376,7 @@ implementation FUN_680()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 16bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 16bv64)) || L(mem, bvadd64(R16, 16bv64)));
     R16, Gamma_R16 := bvadd64(R16, 16bv64), Gamma_R16;
     call malloc();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_6b0();
@@ -427,7 +427,7 @@ implementation FUN_6b0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 40bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 40bv64)) || L(mem, bvadd64(R16, 40bv64)));
     R16, Gamma_R16 := bvadd64(R16, 40bv64), Gamma_R16;
     call #free();
-    assume false; //no return target
+    assume false;
 }
 
 procedure printCharValue();

diff --git a/src/test/correct/malloc_with_local3/gcc/malloc_with_local3_gtirb.expected b/src/test/correct/malloc_with_local3/gcc/malloc_with_local3_gtirb.expected
@@ -167,7 +167,7 @@ implementation FUN_680()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4008bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4008bv64)) || L(mem, bvadd64(R16, 4008bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4008bv64), Gamma_R16;
     call malloc();
-    assume false; //no return target
+    assume false;
 }
 
 procedure printCharValue();
@@ -314,7 +314,7 @@ implementation FUN_6c0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4040bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4040bv64)) || L(mem, bvadd64(R16, 4040bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4040bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_6b0();
@@ -369,7 +369,7 @@ implementation FUN_6b0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4032bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4032bv64)) || L(mem, bvadd64(R16, 4032bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4032bv64), Gamma_R16;
     call #free();
-    assume false; //no return target
+    assume false;
 }
 
 procedure main();

diff --git a/src/test/correct/malloc_with_local3/gcc_O2/malloc_with_local3_gtirb.expected b/src/test/correct/malloc_with_local3/gcc_O2/malloc_with_local3_gtirb.expected
@@ -145,7 +145,7 @@ implementation FUN_690()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4008bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4008bv64)) || L(mem, bvadd64(R16, 4008bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4008bv64), Gamma_R16;
     call malloc();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_6d0();
@@ -192,7 +192,7 @@ implementation FUN_6d0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4040bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4040bv64)) || L(mem, bvadd64(R16, 4040bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4040bv64), Gamma_R16;
     call #free();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_6a0();
@@ -239,7 +239,7 @@ implementation FUN_6a0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4016bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4016bv64)) || L(mem, bvadd64(R16, 4016bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4016bv64), Gamma_R16;
     call __printf_chk();
-    assume false; //no return target
+    assume false;
 }
 
 procedure main();
@@ -404,7 +404,7 @@ implementation printCharValue()
     mem, Gamma_mem := memory_store8_le(mem, R3, R2[8:0]), gamma_store8(Gamma_mem, R3, Gamma_R2);
     assume {:captureState "2236$0"} true;
     call FUN_6a0();
-    assume false; //no return target
+    assume false;
 }
 
 procedure malloc();

diff --git a/src/test/correct/multi_malloc/clang/multi_malloc_gtirb.expected b/src/test/correct/multi_malloc/clang/multi_malloc_gtirb.expected
@@ -275,7 +275,7 @@ implementation FUN_6b0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 40bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 40bv64)) || L(mem, bvadd64(R16, 40bv64)));
     R16, Gamma_R16 := bvadd64(R16, 40bv64), Gamma_R16;
     call #free();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_680();
@@ -316,7 +316,7 @@ implementation FUN_680()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 16bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 16bv64)) || L(mem, bvadd64(R16, 16bv64)));
     R16, Gamma_R16 := bvadd64(R16, 16bv64), Gamma_R16;
     call malloc();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_6c0();
@@ -357,7 +357,7 @@ implementation FUN_6c0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 48bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 48bv64)) || L(mem, bvadd64(R16, 48bv64)));
     R16, Gamma_R16 := bvadd64(R16, 48bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure #free();

diff --git a/src/test/correct/multi_malloc/gcc/multi_malloc_gtirb.expected b/src/test/correct/multi_malloc/gcc/multi_malloc_gtirb.expected
@@ -250,7 +250,7 @@ implementation FUN_6c0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4040bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4040bv64)) || L(mem, bvadd64(R16, 4040bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4040bv64), Gamma_R16;
     call printf();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_680();
@@ -285,7 +285,7 @@ implementation FUN_680()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4008bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4008bv64)) || L(mem, bvadd64(R16, 4008bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4008bv64), Gamma_R16;
     call malloc();
-    assume false; //no return target
+    assume false;
 }
 
 procedure FUN_6b0();
@@ -320,7 +320,7 @@ implementation FUN_6b0()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 4032bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 4032bv64)) || L(mem, bvadd64(R16, 4032bv64)));
     R16, Gamma_R16 := bvadd64(R16, 4032bv64), Gamma_R16;
     call #free();
-    assume false; //no return target
+    assume false;
 }
 
 procedure printf();

diff --git a/src/test/correct/syscall/clang/syscall_gtirb.expected b/src/test/correct/syscall/clang/syscall_gtirb.expected
@@ -181,7 +181,7 @@ implementation FUN_610()
     R17, Gamma_R17 := memory_load64_le(mem, bvadd64(R16, 16bv64)), (gamma_load64(Gamma_mem, bvadd64(R16, 16bv64)) || L(mem, bvadd64(R16, 16bv64)));
     R16, Gamma_R16 := bvadd64(R16, 16bv64), Gamma_R16;
     call fork();
-    assume false; //no return target
+    assume false;
 }
 
 procedure fork();