Add a second test to ExternalLibTest

runtimeverification · Dec 15, 2024 · 76fe7c8 · 76fe7c8
1 parent 84ea0b0
commit 76fe7c8
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 0 deletions.
diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all
@@ -115,6 +115,7 @@ ExpectRevertTest.testFail_ExpectRevert_failAndSuccess()
 ExpectRevertTest.testFail_expectRevert_false()
 ExpectRevertTest.testFail_expectRevert_multipleReverts()
 ExternalLibTest.testSquare(uint256)
+ExternalLibTest.testSum(uint256,uint256)
 FeeTest.test_fee_setup()
 FfiTest.testffi()
 FfiTest.testFFIFOO()

diff --git a/src/tests/integration/test-data/foundry-prove-skip-legacy b/src/tests/integration/test-data/foundry-prove-skip-legacy
@@ -103,6 +103,7 @@ ExpectRevertTest.testFail_ExpectRevert_failAndSuccess()
 ExpectRevertTest.testFail_expectRevert_false()
 ExpectRevertTest.testFail_expectRevert_multipleReverts()
 ExternalLibTest.testSquare(uint256)
+ExternalLibTest.testSum(uint256,uint256)
 FeeTest.test_fee_setup()
 FfiTest.testffi()
 FfiTest.testFFIFOO()

diff --git a/src/tests/integration/test-data/foundry/test/ExternalLibTest.t.sol b/src/tests/integration/test-data/foundry/test/ExternalLibTest.t.sol
@@ -16,6 +16,10 @@ library SimpleMath {
     function square(uint256 x) public pure returns (uint256) {
         return x * x;
     }
+
+    function sum(uint256 a, uint256 b) external pure returns (uint256 res) {
+        res = a + b;
+    }
 }
 
 contract ExternalLibTest is Test {
@@ -24,4 +28,10 @@ contract ExternalLibTest is Test {
         vm.assume(n <= type(uint128).max);
         assertEq(SimpleMath.square(n), n * n);
     }
+
+    function testSum(uint256 x, uint256 y) public {
+        vm.assume(x <= type(uint128).max);
+        vm.assume(y <= type(uint128).max);
+        assertEq(SimpleMath.sum(x, y), 10);
+    }
 }