Skip to content

Commit

Permalink
One more test on mem pairs
Browse files Browse the repository at this point in the history
  • Loading branch information
msooseth committed Nov 26, 2024
1 parent 3797dc0 commit 65a8103
Showing 1 changed file with 22 additions and 0 deletions.
22 changes: 22 additions & 0 deletions test/test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1562,6 +1562,28 @@ tests = testGroup "hevm"
(e, [Qed _]) <- withDefaultSolver $
\s -> checkAssert s defaultPanicCodes c sig [] opts
assertBoolM "The expression is not partial" $ Expr.containsNode isPartial e
, test "mem-tuple" $ do
Just c <- solcRuntime "C"
[i|
contract C {
struct Pair {
uint x;
uint y;
}
function prove_tuple_pass(Pair memory p) public pure {
uint256 f = p.x;
uint256 g = p.y;
unchecked {
p.x+=p.y;
assert(p.x == (f + g));
}
}
}
|]
let opts = defaultVeriOpts
let sig = Nothing
(_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] opts
putStrLnM "Qed, memory tuple is good"
, test "symbolic-loops-not-reached" $ do
Just c <- solcRuntime "C"
[i|
Expand Down

0 comments on commit 65a8103

Please sign in to comment.