from #573: add integration test for symbolic constructor

Author: anvacaru

src/tests/integration/conftest.py

@@ -77,12 +77,14 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo
                             str(TEST_DATA_DIR / 'lemmas.k'),
                             str(TEST_DATA_DIR / 'cse-lemmas.k'),
                             str(TEST_DATA_DIR / 'pausability-lemmas.k'),
+                            str(TEST_DATA_DIR / 'symbolic-bytes-lemmas.k'),
                         ],
                         'imports': [
                             'LoopsTest:SUM-TO-N-INVARIANT',
                             'ArithmeticCallTest:CSE-LEMMAS',
                             'CSETest:CSE-LEMMAS',
                             'PortalTest:PAUSABILITY-LEMMAS',
+                            'ImmutableVarsTest:SYMBOLIC-BYTES-LEMMAS',
                         ],
                     }
                 ),

src/tests/integration/test-data/foundry-fail

@@ -5,3 +5,4 @@ AssertTest.test_failing_branch(uint256)
 AssertTest.test_revert_branch(uint256,uint256)
 AssumeTest.test_assume_false(uint256,uint256)
 AssumeTest.testFail_assume_false(uint256,uint256)
+ImmutableVarsTest.test_run_deployment(uint256)

src/tests/integration/test-data/foundry-prove-all

@@ -138,6 +138,7 @@ FreshCheatcodes.test_freshSymbolicWord()
 GasTest.testInfiniteGas()
 GasTest.testSetGas()
 GetCodeTest.testGetCode()
+ImmutableVarsTest.test_run_deployment(uint256)
 LabelTest.testLabel()
 LoopsTest.sum_N(uint256)
 LoopsTest.testIsNotPrime(uint256)

src/tests/integration/test-data/foundry-prove-skip

@@ -79,6 +79,7 @@ FreshCheatcodes.testFail_int128()
 FreshCheatcodes.test_freshUints(uint8)
 GasTest.testInfiniteGas()
 GetCodeTest.testGetCode()
+ImmutableVarsTest.test_run_deployment(uint256)
 LoopsTest.testIsNotPrime(uint256)
 LoopsTest.testIsPrime(uint256,uint256)
 LoopsTest.testIsPrimeBroken(uint256,uint256)

src/tests/integration/test-data/foundry-prove-skip-legacy

@@ -128,6 +128,7 @@ FreshCheatcodes.test_freshSymbolicWord()
 GasTest.testInfiniteGas()
 GasTest.testSetGas()
 GetCodeTest.testGetCode()
+ImmutableVarsTest.test_run_deployment(uint256)
 InitCodeTest.test_init()
 IntTypeTest.testFail_uint128(uint128)
 IntTypeTest.testFail_uint256(uint256)

src/tests/integration/test-data/foundry-show

@@ -8,4 +8,5 @@ AssertTest.test_revert_branch(uint256,uint256)
 AssumeTest.test_assume_false(uint256,uint256)
 AssumeTest.testFail_assume_false(uint256,uint256)
 AssumeTest.testFail_assume_true(uint256,uint256)
+ImmutableVarsTest.test_run_deployment(uint256)
 SetUpDeployTest.test_extcodesize()

src/tests/integration/test-data/foundry/test/ImmutableVarsTest.t.sol

@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+import "forge-std/Test.sol";
+import "kontrol-cheatcodes/KontrolCheats.sol";
+
+contract ImmutableVarsContract {
+    uint256 public immutable y;
+
+    constructor(uint256 _y) {
+        y = _y;
+    }
+}
+
+contract ImmutableVarsTest is Test {
+    function test_run_deployment(uint256 x) public returns (bool) {
+        ImmutableVarsContract c = new ImmutableVarsContract(x);
+        assert(c.y() == 85);
+    }
+}