When trying the End to End test example, property test is passed while it is supposed to fail about building-secure-contracts HOT 10 CLOSED

I'm checking this issue today, sorry for the delay

from building-secure-contracts.

This works fine here. Your json file looks correct to me however, can you please try using the suggested echidna file?

prefix: crytic_
initialize: init.json
multi-abi: true
cryticArgs: ['--truffle-build-directory', 'app/src/contracts/'] # needed by drizzle

Also please update to the latest Echidna release (2.0.1). I will still improve the tutorial with a few minor changes, so please take a look later just in case.

from building-secure-contracts.

This works fine here. Your json file looks correct to me however, can you please try using the suggested echidna file?

prefix: crytic_
initialize: init.json
multi-abi: true
cryticArgs: ['--truffle-build-directory', 'app/src/contracts/'] # needed by drizzle

Also please update to the latest Echidna release (2.0.1). I will still improve the tutorial with a few minor changes, so please take a look later just in case.

@ggrieco-tob Sure, let me give it a try. Actually I am also referring to this post https://github.com/crytic/echidna/wiki/How-to-use-Echidna-with-multiple-contracts, Echidna can output correct result using the proxy method. The proxy contract I write is as follow:

from building-secure-contracts.

This works fine here. Your json file looks correct to me however, can you please try using the suggested echidna file?

prefix: crytic_
initialize: init.json
multi-abi: true
cryticArgs: ['--truffle-build-directory', 'app/src/contracts/'] # needed by drizzle

Also please update to the latest Echidna release (2.0.1). I will still improve the tutorial with a few minor changes, so please take a look later just in case.

@ggrieco-tob And may I know what the 'cryticArgs' means in the config file, I enter the app/src/contracts directory and find out there are only json files of the compiled contracts.

from building-secure-contracts.

And may I know what the 'cryticArgs' means in the config file, I enter the app/src/contracts directory and find out there are only json files of the compiled contracts.

cryticArgs are a list of additional arguments to use in crytic-compile for the compilation of the contract to test. An up-to-date list of the echidna config options is available here: https://github.com/crytic/echidna/wiki/Config

from building-secure-contracts.

@ggrieco-tob Thank you sir. Previously I am using 2.0.0, now I am switching to 2.0.1 to give it a try. I am using the binary version, so the drizzle -box folder is put inside the echidna folder containing the binary programs.
But the result is still the same, echidna does not find the error. My directory is as follows:

The E2E.sol is put in the drizzle-box/contracts/crytic directory

And I view the app/src directory, there's no contracts folder being generated:

My command to run the echidna test is:
$ ./echidna-test drizzle-box/contracts/crytic/E2E.sol --contract E2E --config echidna.yaml

Do you think the cause could be the mismatch of contract directories or config file directory?

from building-secure-contracts.

@elopez can you take a look and try to reproduce this issue in MacOS? (which seems to be used here).

from building-secure-contracts.

Following the process as of this version of the document worked okay on my Mac, with a few caveats:

• I had to npm i ganache-cli@6, otherwise etheno would not play nice with ganache-cli v7.x
• I had to install etheno this way, otherwise I would end up with broken dependencies that would not let me run it:

python3 -m venv venv
venv/bin/pip3 install https://github.com/crytic/etheno/archive/refs/heads/master.zip 'eth-rlp<0.3.0'

@BarrySauce note that you're passing the .sol directly to echidna on your call -- you need to pass the project folder instead and let truffle handle the build of the E2E and other contracts. Give ./echidna-test drizzle-box/ --contract E2E --config echidna.yaml a try and let us know if that helps!

from building-secure-contracts.

Following the process as of this version of the document worked okay on my Mac, with a few caveats:

• I had to npm i ganache-cli@6, otherwise etheno would not play nice with ganache-cli v7.x
• I had to install etheno this way, otherwise I would end up with broken dependencies that would not let me run it:

python3 -m venv venv
venv/bin/pip3 install https://github.com/crytic/etheno/archive/refs/heads/master.zip 'eth-rlp<0.3.0'

@BarrySauce note that you're passing the .sol directly to echidna on your call -- you need to pass the project folder instead and let truffle handle the build of the E2E and other contracts. Give ./echidna-test drizzle-box/ --contract E2E --config echidna.yaml a try and let us know if that helps!

@elopez I tried your command and it works! Thank you for your help, and thank @ggrieco-tob for your support. So in case of this kind of test using with Etheno, we cannot pass the specific E2E .sol file, instead we are supposed to pass the project folder and the contract 👍

from building-secure-contracts.

Thanks for opening the issue and help us to improve our documentation. I added a clarification in the tutorial to avoid this issue in the future: 82bdc69

from building-secure-contracts.