Skip to content

Commit

Permalink
fix non-determinism in GTIRB GoTo order creation
Browse files Browse the repository at this point in the history
  • Loading branch information
l-kent committed Aug 19, 2024
1 parent 6003389 commit a321018
Show file tree
Hide file tree
Showing 81 changed files with 3,113 additions and 24,645 deletions.
2 changes: 1 addition & 1 deletion src/main/scala/translating/GTIRBToIR.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -370,7 +370,7 @@ class GTIRBToIR(mods: Seq[Module], parserMap: immutable.Map[String, Array[Array[
trueBlock.replaceJump(currentBlock.jump)
falseBlock.replaceJump(jumpCopy)
}
currentBlock.replaceJump(GoTo(mutable.Set(trueBlock, falseBlock)))
currentBlock.replaceJump(GoTo(Seq(trueBlock, falseBlock)))
currentBlock.statements.remove(i)

newBlocks
Expand Down
2 changes: 1 addition & 1 deletion src/test/correct/basic_function_call_reader/clang/basic_function_call_reader_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ implementation main()
NF, Gamma_NF := Cse0__5$0$7[32:31], Gamma_Cse0__5$0$7;
R8, Gamma_R8 := zero_extend32_32(Cse0__5$0$7), Gamma_Cse0__5$0$7;
assert Gamma_ZF;
goto $main$__0__$p64I2ZUnTxGzbzeacDZqwg$__1, $main$__0__$p64I2ZUnTxGzbzeacDZqwg$__0;
goto $main$__0__$p64I2ZUnTxGzbzeacDZqwg$__0, $main$__0__$p64I2ZUnTxGzbzeacDZqwg$__1;
$main$__1__$bKbuo5TmTwOMb5a3DV3xHQ:
assume {:captureState "$main$__1__$bKbuo5TmTwOMb5a3DV3xHQ"} true;
goto $main$__2__$aBEoJbwOSm2rHPYmBa6e_A;
Expand Down
2 changes: 1 addition & 1 deletion .../basic_function_call_reader/clang_no_plt_no_pic/basic_function_call_reader_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ implementation main()
NF, Gamma_NF := Cse0__5$2$7[32:31], Gamma_Cse0__5$2$7;
R8, Gamma_R8 := zero_extend32_32(Cse0__5$2$7), Gamma_Cse0__5$2$7;
assert Gamma_ZF;
goto $main$__0__$WfJX0DVpQGWbeLbKJqZHWA$__1, $main$__0__$WfJX0DVpQGWbeLbKJqZHWA$__0;
goto $main$__0__$WfJX0DVpQGWbeLbKJqZHWA$__0, $main$__0__$WfJX0DVpQGWbeLbKJqZHWA$__1;
$main$__1__$r0XSeayHQLKv3XOIC~hUrw:
assume {:captureState "$main$__1__$r0XSeayHQLKv3XOIC~hUrw"} true;
goto $main$__2__$lAtG_PvKQRuVF0Vm7Ddqjw;
Expand Down
2 changes: 1 addition & 1 deletion src/test/correct/basic_lock_read/clang/basic_lock_read_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ implementation main()
NF, Gamma_NF := Cse0__5$2$5[32:31], Gamma_Cse0__5$2$5;
R8, Gamma_R8 := zero_extend32_32(Cse0__5$2$5), Gamma_Cse0__5$2$5;
assert Gamma_ZF;
goto $main$__0__$rFLbTMieRHaXyRDy_WM9nA$__1, $main$__0__$rFLbTMieRHaXyRDy_WM9nA$__0;
goto $main$__0__$rFLbTMieRHaXyRDy_WM9nA$__0, $main$__0__$rFLbTMieRHaXyRDy_WM9nA$__1;
$main$__1__$24kG8YkCTZOdLFRKQWWeuQ:
assume {:captureState "$main$__1__$24kG8YkCTZOdLFRKQWWeuQ"} true;
goto $main$__2__$Uq6ddtMrQtqVC9c4DWnGkw;
Expand Down
2 changes: 1 addition & 1 deletion ...rect/basic_lock_security_read/clang_no_plt_no_pic/basic_lock_security_read_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ implementation main()
NF, Gamma_NF := Cse0__5$2$5[32:31], Gamma_Cse0__5$2$5;
R8, Gamma_R8 := zero_extend32_32(Cse0__5$2$5), Gamma_Cse0__5$2$5;
assert Gamma_ZF;
goto $main$__0__$ah2ASK3lTCmvZ46W1uC2Dg$__1, $main$__0__$ah2ASK3lTCmvZ46W1uC2Dg$__0;
goto $main$__0__$ah2ASK3lTCmvZ46W1uC2Dg$__0, $main$__0__$ah2ASK3lTCmvZ46W1uC2Dg$__1;
$main$__1__$IUFLo3ClTS6sO62N9ZSQ2Q:
assume {:captureState "$main$__1__$IUFLo3ClTS6sO62N9ZSQ2Q"} true;
goto $main$__2__$GM9lIeMTTKel2N9BZPjHpA;
Expand Down
2 changes: 1 addition & 1 deletion .../basic_operation_evaluation/clang_no_plt_no_pic/basic_operation_evaluation_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,7 @@ implementation main()
R8, Gamma_R8 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 12bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 12bv64));
R10, Gamma_R10 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 8bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 8bv64));
assert Gamma_R10;
goto $main$__0__$cbaW_N42Q0ecmUdVUz6rsw$__1, $main$__0__$cbaW_N42Q0ecmUdVUz6rsw$__0;
goto $main$__0__$cbaW_N42Q0ecmUdVUz6rsw$__0, $main$__0__$cbaW_N42Q0ecmUdVUz6rsw$__1;
$main$__0__$cbaW_N42Q0ecmUdVUz6rsw$__0:
assume {:captureState "$main$__0__$cbaW_N42Q0ecmUdVUz6rsw$__0"} true;
assume (R10[32:0] == 0bv32);
Expand Down
2 changes: 1 addition & 1 deletion src/test/correct/basic_operation_evaluation/gcc/basic_operation_evaluation_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ implementation main()
R0, Gamma_R0 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 20bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 20bv64));
R1, Gamma_R1 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 24bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 24bv64));
assert Gamma_R1;
goto $main$__0__$B9tkaGtQRX6xFjqGS87lEw$__1, $main$__0__$B9tkaGtQRX6xFjqGS87lEw$__0;
goto $main$__0__$B9tkaGtQRX6xFjqGS87lEw$__0, $main$__0__$B9tkaGtQRX6xFjqGS87lEw$__1;
$main$__0__$B9tkaGtQRX6xFjqGS87lEw$__0:
assume {:captureState "$main$__0__$B9tkaGtQRX6xFjqGS87lEw$__0"} true;
assume (R1[32:0] == 0bv32);
Expand Down
2 changes: 1 addition & 1 deletion ...ct/basic_operation_evaluation/gcc_no_plt_no_pic/basic_operation_evaluation_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ implementation main()
R0, Gamma_R0 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 20bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 20bv64));
R1, Gamma_R1 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 24bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 24bv64));
assert Gamma_R1;
goto $main$__0__$aTVS6C3SRXWJtEa_z5e59w$__1, $main$__0__$aTVS6C3SRXWJtEa_z5e59w$__0;
goto $main$__0__$aTVS6C3SRXWJtEa_z5e59w$__0, $main$__0__$aTVS6C3SRXWJtEa_z5e59w$__1;
$main$__0__$aTVS6C3SRXWJtEa_z5e59w$__0:
assume {:captureState "$main$__0__$aTVS6C3SRXWJtEa_z5e59w$__0"} true;
assume (R1[32:0] == 0bv32);
Expand Down
2 changes: 1 addition & 1 deletion ...test/correct/basic_operation_evaluation/gcc_pic/basic_operation_evaluation_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ implementation main()
R0, Gamma_R0 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 20bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 20bv64));
R1, Gamma_R1 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 24bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 24bv64));
assert Gamma_R1;
goto $main$__0__$JcNgWRJOQcqIG8g4zfosRw$__1, $main$__0__$JcNgWRJOQcqIG8g4zfosRw$__0;
goto $main$__0__$JcNgWRJOQcqIG8g4zfosRw$__0, $main$__0__$JcNgWRJOQcqIG8g4zfosRw$__1;
$main$__0__$JcNgWRJOQcqIG8g4zfosRw$__0:
assume {:captureState "$main$__0__$JcNgWRJOQcqIG8g4zfosRw$__0"} true;
assume (R1[32:0] == 0bv32);
Expand Down
2 changes: 1 addition & 1 deletion ...st/correct/basic_sec_policy_read/clang_no_plt_no_pic/basic_sec_policy_read_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ implementation main()
NF, Gamma_NF := Cse0__5$2$7[32:31], Gamma_Cse0__5$2$7;
R8, Gamma_R8 := zero_extend32_32(Cse0__5$2$7), Gamma_Cse0__5$2$7;
assert Gamma_ZF;
goto $main$__0__$mhUWbWciRjyRRsDZhN~PKg$__1, $main$__0__$mhUWbWciRjyRRsDZhN~PKg$__0;
goto $main$__0__$mhUWbWciRjyRRsDZhN~PKg$__0, $main$__0__$mhUWbWciRjyRRsDZhN~PKg$__1;
$main$__1__$7Fr3FH6lTNeYctpHVIjwfA:
assume {:captureState "$main$__1__$7Fr3FH6lTNeYctpHVIjwfA"} true;
goto $main$__2__$T6JPTszHSASiS5SG2BJuAQ;
Expand Down
2 changes: 1 addition & 1 deletion src/test/correct/basic_sec_policy_read/clang_pic/basic_sec_policy_read_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -155,7 +155,7 @@ implementation main()
NF, Gamma_NF := Cse0__5$3$9[32:31], Gamma_Cse0__5$3$9;
R8, Gamma_R8 := zero_extend32_32(Cse0__5$3$9), Gamma_Cse0__5$3$9;
assert Gamma_ZF;
goto $main$__0__$_zy4nZRRQ4202Be_0Qr3jw$__1, $main$__0__$_zy4nZRRQ4202Be_0Qr3jw$__0;
goto $main$__0__$_zy4nZRRQ4202Be_0Qr3jw$__0, $main$__0__$_zy4nZRRQ4202Be_0Qr3jw$__1;
$main$__1__$rmVyzzfSSQeYVjuxiNU3PA:
assume {:captureState "$main$__1__$rmVyzzfSSQeYVjuxiNU3PA"} true;
goto $main$__2__$nmt_XUHDT5eyVHAHshN3ww;
Expand Down
2 changes: 1 addition & 1 deletion src/test/correct/cjump/clang/cjump_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ implementation main()
NF, Gamma_NF := Cse0__5$0$6[32:31], Gamma_Cse0__5$0$6;
R8, Gamma_R8 := zero_extend32_32(Cse0__5$0$6), Gamma_Cse0__5$0$6;
assert Gamma_ZF;
goto $main$__0__$PnDIl5cyR4GGh5gDIaWl6w$__1, $main$__0__$PnDIl5cyR4GGh5gDIaWl6w$__0;
goto $main$__0__$PnDIl5cyR4GGh5gDIaWl6w$__0, $main$__0__$PnDIl5cyR4GGh5gDIaWl6w$__1;
$main$__1__$QUCiZ1czSk63UIuy~Dy6Bg:
assume {:captureState "$main$__1__$QUCiZ1czSk63UIuy~Dy6Bg"} true;
goto $main$__2__$5gUE9BicSVSdDO98Zitx1A;
Expand Down
2 changes: 1 addition & 1 deletion src/test/correct/cjump/clang_no_plt_no_pic/cjump_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ implementation main()
NF, Gamma_NF := Cse0__5$3$6[32:31], Gamma_Cse0__5$3$6;
R8, Gamma_R8 := zero_extend32_32(Cse0__5$3$6), Gamma_Cse0__5$3$6;
assert Gamma_ZF;
goto $main$__0__$nCAfHRQORqmBecA1YhhLlg$__1, $main$__0__$nCAfHRQORqmBecA1YhhLlg$__0;
goto $main$__0__$nCAfHRQORqmBecA1YhhLlg$__0, $main$__0__$nCAfHRQORqmBecA1YhhLlg$__1;
$main$__1__$zSPNKyWWTDmPQQiP1j8ENA:
assume {:captureState "$main$__1__$zSPNKyWWTDmPQQiP1j8ENA"} true;
goto $main$__2__$l8R0l_GWRn60VI56pcjGpA;
Expand Down
81 changes: 9 additions & 72 deletions src/test/correct/function1/gcc/function1_gtirb.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,14 +84,7 @@ procedure {:extern} rely();
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
free ensures (memory_load8_le(mem, 2048bv64) == 1bv8);
free ensures (memory_load8_le(mem, 2049bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2050bv64) == 2bv8);
free ensures (memory_load8_le(mem, 2051bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2052bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2053bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2054bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2055bv64) == 0bv8);
free ensures (memory_load64_le(mem, 2048bv64) == 131073bv64);
free ensures (memory_load8_le(mem, 2056bv64) == 37bv8);
free ensures (memory_load8_le(mem, 2057bv64) == 100bv8);
free ensures (memory_load8_le(mem, 2058bv64) == 10bv8);
Expand Down Expand Up @@ -119,14 +112,7 @@ procedure {:extern} guarantee_reflexive();

procedure FUN_630();
modifies Gamma_R16, Gamma_R17, Gamma_mem, R16, R17, mem;
free requires (memory_load8_le(mem, 2048bv64) == 1bv8);
free requires (memory_load8_le(mem, 2049bv64) == 0bv8);
free requires (memory_load8_le(mem, 2050bv64) == 2bv8);
free requires (memory_load8_le(mem, 2051bv64) == 0bv8);
free requires (memory_load8_le(mem, 2052bv64) == 0bv8);
free requires (memory_load8_le(mem, 2053bv64) == 0bv8);
free requires (memory_load8_le(mem, 2054bv64) == 0bv8);
free requires (memory_load8_le(mem, 2055bv64) == 0bv8);
free requires (memory_load64_le(mem, 2048bv64) == 131073bv64);
free requires (memory_load8_le(mem, 2056bv64) == 37bv8);
free requires (memory_load8_le(mem, 2057bv64) == 100bv8);
free requires (memory_load8_le(mem, 2058bv64) == 10bv8);
Expand All @@ -135,14 +121,7 @@ procedure FUN_630();
free requires (memory_load64_le(mem, 69016bv64) == 1792bv64);
free requires (memory_load64_le(mem, 69616bv64) == 1924bv64);
free requires (memory_load64_le(mem, 69640bv64) == 69640bv64);
free ensures (memory_load8_le(mem, 2048bv64) == 1bv8);
free ensures (memory_load8_le(mem, 2049bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2050bv64) == 2bv8);
free ensures (memory_load8_le(mem, 2051bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2052bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2053bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2054bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2055bv64) == 0bv8);
free ensures (memory_load64_le(mem, 2048bv64) == 131073bv64);
free ensures (memory_load8_le(mem, 2056bv64) == 37bv8);
free ensures (memory_load8_le(mem, 2057bv64) == 100bv8);
free ensures (memory_load8_le(mem, 2058bv64) == 10bv8);
Expand All @@ -166,14 +145,7 @@ implementation FUN_630()

procedure get_two();
modifies Gamma_R0, Gamma_R1, Gamma_R31, Gamma_stack, R0, R1, R31, stack;
free requires (memory_load8_le(mem, 2048bv64) == 1bv8);
free requires (memory_load8_le(mem, 2049bv64) == 0bv8);
free requires (memory_load8_le(mem, 2050bv64) == 2bv8);
free requires (memory_load8_le(mem, 2051bv64) == 0bv8);
free requires (memory_load8_le(mem, 2052bv64) == 0bv8);
free requires (memory_load8_le(mem, 2053bv64) == 0bv8);
free requires (memory_load8_le(mem, 2054bv64) == 0bv8);
free requires (memory_load8_le(mem, 2055bv64) == 0bv8);
free requires (memory_load64_le(mem, 2048bv64) == 131073bv64);
free requires (memory_load8_le(mem, 2056bv64) == 37bv8);
free requires (memory_load8_le(mem, 2057bv64) == 100bv8);
free requires (memory_load8_le(mem, 2058bv64) == 10bv8);
Expand All @@ -184,14 +156,7 @@ procedure get_two();
free requires (memory_load64_le(mem, 69640bv64) == 69640bv64);
free ensures (Gamma_R31 == old(Gamma_R31));
free ensures (R31 == old(R31));
free ensures (memory_load8_le(mem, 2048bv64) == 1bv8);
free ensures (memory_load8_le(mem, 2049bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2050bv64) == 2bv8);
free ensures (memory_load8_le(mem, 2051bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2052bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2053bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2054bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2055bv64) == 0bv8);
free ensures (memory_load64_le(mem, 2048bv64) == 131073bv64);
free ensures (memory_load8_le(mem, 2056bv64) == 37bv8);
free ensures (memory_load8_le(mem, 2057bv64) == 100bv8);
free ensures (memory_load8_le(mem, 2058bv64) == 10bv8);
Expand Down Expand Up @@ -229,14 +194,7 @@ procedure main();
modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R2, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R2, R29, R30, R31, mem, stack;
free requires (memory_load64_le(mem, 69632bv64) == 0bv64);
free requires (memory_load64_le(mem, 69640bv64) == 69640bv64);
free requires (memory_load8_le(mem, 2048bv64) == 1bv8);
free requires (memory_load8_le(mem, 2049bv64) == 0bv8);
free requires (memory_load8_le(mem, 2050bv64) == 2bv8);
free requires (memory_load8_le(mem, 2051bv64) == 0bv8);
free requires (memory_load8_le(mem, 2052bv64) == 0bv8);
free requires (memory_load8_le(mem, 2053bv64) == 0bv8);
free requires (memory_load8_le(mem, 2054bv64) == 0bv8);
free requires (memory_load8_le(mem, 2055bv64) == 0bv8);
free requires (memory_load64_le(mem, 2048bv64) == 131073bv64);
free requires (memory_load8_le(mem, 2056bv64) == 37bv8);
free requires (memory_load8_le(mem, 2057bv64) == 100bv8);
free requires (memory_load8_le(mem, 2058bv64) == 10bv8);
Expand All @@ -249,14 +207,7 @@ procedure main();
free ensures (Gamma_R31 == old(Gamma_R31));
free ensures (R29 == old(R29));
free ensures (R31 == old(R31));
free ensures (memory_load8_le(mem, 2048bv64) == 1bv8);
free ensures (memory_load8_le(mem, 2049bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2050bv64) == 2bv8);
free ensures (memory_load8_le(mem, 2051bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2052bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2053bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2054bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2055bv64) == 0bv8);
free ensures (memory_load64_le(mem, 2048bv64) == 131073bv64);
free ensures (memory_load8_le(mem, 2056bv64) == 37bv8);
free ensures (memory_load8_le(mem, 2057bv64) == 100bv8);
free ensures (memory_load8_le(mem, 2058bv64) == 10bv8);
Expand Down Expand Up @@ -326,14 +277,7 @@ implementation main()
}

procedure printf();
free requires (memory_load8_le(mem, 2048bv64) == 1bv8);
free requires (memory_load8_le(mem, 2049bv64) == 0bv8);
free requires (memory_load8_le(mem, 2050bv64) == 2bv8);
free requires (memory_load8_le(mem, 2051bv64) == 0bv8);
free requires (memory_load8_le(mem, 2052bv64) == 0bv8);
free requires (memory_load8_le(mem, 2053bv64) == 0bv8);
free requires (memory_load8_le(mem, 2054bv64) == 0bv8);
free requires (memory_load8_le(mem, 2055bv64) == 0bv8);
free requires (memory_load64_le(mem, 2048bv64) == 131073bv64);
free requires (memory_load8_le(mem, 2056bv64) == 37bv8);
free requires (memory_load8_le(mem, 2057bv64) == 100bv8);
free requires (memory_load8_le(mem, 2058bv64) == 10bv8);
Expand All @@ -342,14 +286,7 @@ procedure printf();
free requires (memory_load64_le(mem, 69016bv64) == 1792bv64);
free requires (memory_load64_le(mem, 69616bv64) == 1924bv64);
free requires (memory_load64_le(mem, 69640bv64) == 69640bv64);
free ensures (memory_load8_le(mem, 2048bv64) == 1bv8);
free ensures (memory_load8_le(mem, 2049bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2050bv64) == 2bv8);
free ensures (memory_load8_le(mem, 2051bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2052bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2053bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2054bv64) == 0bv8);
free ensures (memory_load8_le(mem, 2055bv64) == 0bv8);
free ensures (memory_load64_le(mem, 2048bv64) == 131073bv64);
free ensures (memory_load8_le(mem, 2056bv64) == 37bv8);
free ensures (memory_load8_le(mem, 2057bv64) == 100bv8);
free ensures (memory_load8_le(mem, 2058bv64) == 10bv8);
Expand Down
Loading

0 comments on commit a321018

Please sign in to comment.