diff --git a/src/test/correct/basicfree/clang/basicfree_gtirb.expected b/src/test/correct/basicfree/clang/basicfree_gtirb.expected index 9e8648f7a..0afab7180 100644 --- 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 index 266703ea4..9b75b6fd3 100644 --- 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 index f947324c6..6a09e1ad8 100644 --- 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 index 4de982386..a6814f2c8 100644 --- 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 index a3e86929d..d659b4364 100644 --- 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 index bb4ea6029..c6c0b7514 100644 --- 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 index be9562312..9824811ab 100644 --- 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 index d552dd48f..cd39145d7 100644 --- 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 index 865a3484a..1587a7a14 100644 --- 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 index b90c4182b..6fae6b6ba 100644 --- 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 index 1477f8efa..35a8659c0 100644 --- 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 index 7be6dae35..69e194091 100644 --- 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 index bb14ba90e..9c82490bb 100644 --- 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 index c85477c98..026f5518e 100644 --- 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 index fb4f6641c..22e7f1347 100644 --- 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 index edb83519f..034a6ffd3 100644 --- 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 index 5d6c718b3..508af9ec4 100644 --- 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 index dbf557d37..dfaf0a7b1 100644 --- 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 index ca51a57d4..b26def393 100644 --- 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 index fb09941da..4cb699d0b 100644 --- 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 index 2aa4c91b0..bddf81deb 100644 --- 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 index a8f531eae..1b662d317 100644 --- 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(); diff --git a/src/test/correct/syscall/clang_O2/syscall_gtirb.expected b/src/test/correct/syscall/clang_O2/syscall_gtirb.expected index 9a603287d..0c9d7d48d 100644 --- a/src/test/correct/syscall/clang_O2/syscall_gtirb.expected +++ b/src/test/correct/syscall/clang_O2/syscall_gtirb.expected @@ -78,7 +78,7 @@ implementation main() $main$__0__$noLlJkgwRnOvXgJivIONmQ: assume {:captureState "$main$__0__$noLlJkgwRnOvXgJivIONmQ"} true; call .L_610(); - assume false; //no return target + assume false; } procedure .L_610(); @@ -109,7 +109,7 @@ implementation .L_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(); diff --git a/src/test/correct/syscall/gcc/syscall_gtirb.expected b/src/test/correct/syscall/gcc/syscall_gtirb.expected index a760f92e4..bff162b41 100644 --- a/src/test/correct/syscall/gcc/syscall_gtirb.expected +++ b/src/test/correct/syscall/gcc/syscall_gtirb.expected @@ -117,7 +117,7 @@ implementation FUN_610() 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 fork(); - assume false; //no return target + assume false; } procedure main(); diff --git a/src/test/correct/syscall/gcc_O2/syscall_gtirb.expected b/src/test/correct/syscall/gcc_O2/syscall_gtirb.expected index bfe3f85b8..ef48faa8c 100644 --- a/src/test/correct/syscall/gcc_O2/syscall_gtirb.expected +++ b/src/test/correct/syscall/gcc_O2/syscall_gtirb.expected @@ -78,7 +78,7 @@ implementation main() $main$__0__$LN79XLVpSMWduuQh58xTyg: assume {:captureState "$main$__0__$LN79XLVpSMWduuQh58xTyg"} true; call .L_610(); - assume false; //no return target + assume false; } procedure .L_610(); @@ -109,7 +109,7 @@ implementation .L_610() 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 fork(); - assume false; //no return target + assume false; } procedure fork();