I’m very new to Certora, was trying the Bank.sol example but got the following error after adding --debug flag.
Would really appreciate any help.
PS C:\Users\rssav\Desktop\verify> certoraRun Bank.sol --verify Bank:IntegrityOfDeposit.spec --solc solc7 --debug
DEBUG: setting cache key to Bank.sol-optimisticFalse-iterNone
DEBUG: directory C:\Users\rssav\Desktop\verify\.last_confs already exists
DEBUG: Saving last configuration file to C:\Users\rssav\Desktop\verify\.last_confs\last_conf_02_07_2022__18_40_25.conf
DEBUG: args.packages_path is C:\Users\rssav\Desktop\verify\node_modules
WARNING: Default package file package.json not found
DEBUG: parsed args successfully.
DEBUG: args= Namespace(files=['Bank.sol'], verify=['Bank:IntegrityOfDeposit.spec'], assert_contracts=None, bytecode_jsons=None, bytecode_spec=None, msg=None, rule=None, multi_assert_check=False, rule_sanity=None, short_output=False, typecheck_only=False, send_only=False, solc='C:/Users/rssav/Desktop/solc/solc7.exe', solc_args=None,
solc_map=None, path='C:\\Users\\rssav\\Desktop\\verify', optimize=None, optimize_map=None, packages_path='C:\\Users\\rssav\\Desktop\\verify\\node_modules', packages=None, optimistic_loop=False, loop_iter=None, method=None, cache='Bank.sol-optimisticFalse-iterNone', smt_timeout=None, link=None, address={}, struct_link=None, debug='', debug_topics=False, staging=None, cloud=None, jar=None, java_args=None, check_args=False, build_only=False, disableLocalTypeChecking=False, no_compare=False, expected_file='expected.json', queue_wait_minutes=None, max_poll_minutes=None, log_query_frequency_seconds=None, max_attempts_to_fetch_output=None, delay_fetch_output_seconds=None, process='emv', settings=None, log_branch=None, disable_auto_cache_key_gen=False, max_graph_depth=None, tool_output=None, internal_funcs=None, coinbaseMode=False, mode=<Mode.VERIFY>, user_defined_cache=False, contracts={'Bank'}, file_paths={'Bank.sol'}, file_to_contract={'Bank.sol': 'Bank'}, verified_contract_files=['Bank.sol'], spec_files=['IntegrityOfDeposit.spec'], local=False, env='production')
Collecting contracts and building
DEBUG: error occurred when running git executable
Traceback (most recent call last):
File "C:\Users\rssav\AppData\Local\Programs\Python\Python310\Lib\site-packages\certora_cli\EVMVerifier\certoraCollectRunMetadata.py", line 150, in collect_run_metadata
cwd_relative = cwd_abs.relative_to(base_dir)
File "C:\Users\rssav\AppData\Local\Programs\Python\Python310\lib\pathlib.py", line 816, in relative_to
raise ValueError("{!r} is not in the subpath of {!r}"
ValueError: 'C:\\Users\\rssav\\Desktop\\verify' is not in the subpath of '' OR one path is relative and the other is absolute.
DEBUG: improvised base dir reconstruction found .
DEBUG: There is no TAC file. Going to script EVMVerifier\certoraBuild.py to main_with_args()
DEBUG: Creating dir C:/Users/rssav/Desktop/verify/.certora_config
DEBUG: In C:\Users\rssav\Desktop\verify\integrityOfDeposit.spec, found the imports: []
DEBUG: copying spec file C:/Users/rssav/Desktop/verify/integrityOfDeposit.spec to C:/Users/rssav/Desktop/verify/.certora_config/0_integrityOfDeposit.spec.spec
DEBUG: writing C:/Users/rssav/Desktop/verify/.certora_verify.json
Local CVL specification syntax checking finished successfully
DEBUG:
building file Bank.sol
DEBUG: relevant solc is C:/Users/rssav/Desktop/solc/solc7.exe
DEBUG: about to run C:/Users/rssav/Desktop/solc/solc7.exe -o "C:\Users\rssav\Desktop\verify\.certora_config\Bank.sol_0/" --overwrite --allow-paths "C:\Users\rssav\Desktop\verify",. --standard-json
DEBUG: solc input = {
"language": "Solidity",
"sources": {
"C:\\Users\\rssav\\Desktop\\verify\\Bank.sol": {
"urls": [
"C:\\Users\\rssav\\Desktop\\verify\\Bank.sol"
]
}
},
"settings": {
"remappings": [],
"outputSelection": {
"*": {
"*": [
"storageLayout",
"abi",
"evm.bytecode",
"evm.deployedBytecode",
"evm.methodIdentifiers",
"evm.assembly"
],
"": [
"id",
"ast"
]
}
}
}
}
DEBUG: Running cmd C:/Users/rssav/Desktop/solc/solc7.exe -o "C:\Users\rssav\Desktop\verify\.certora_config\Bank.sol_0/" --overwrite --allow-paths "C:\Users\rssav\Desktop\verify",. --standard-json
DEBUG: stdout, stderr = C:\Users\rssav\Desktop\verify\.certora_config\Bank.sol_0.standard.json.stdout, C:\Users\rssav\Desktop\verify\.certora_config\Bank.sol_0.standard.json.stderr
DEBUG: Exitcode 0
DEBUG: Collecting standard json: C:/Users/rssav/Desktop/solc/solc7.exe -o "C:\Users\rssav\Desktop\verify\.certora_config\Bank.sol_0/" --overwrite --allow-paths "C:\Users\rssav\Desktop\verify",. --standard-json
DEBUG: reading standard json data from C:\Users\rssav\Desktop\verify\.certora_config\Bank.sol_0.standard.json.stdout
DEBUG: Adding ast of Bank.sol for C:\Users\rssav\Desktop\verify\Bank.sol
CRITICAL: Encountered an error running Certora Prover; consider running the script again with --debug to find out why
Traceback (most recent call last):
File "C:\Users\rssav\AppData\Local\Programs\Python\Python310\Lib\site-packages\certora_cli\EVMVerifier\certoraBuild.py", line 3028, in build
certora_build_generator.build(args)
File "C:\Users\rssav\AppData\Local\Programs\Python\Python310\Lib\site-packages\certora_cli\EVMVerifier\certoraBuild.py", line 2233, in build
sdc_pre_finder = self.collect_for_file(build_arg_contract_file, i)
File "C:\Users\rssav\AppData\Local\Programs\Python\Python310\Lib\site-packages\certora_cli\EVMVerifier\certoraBuild.py", line 1674, in collect_for_file
contract_list = sorted([c for c in data["contracts"][contract_file]])
KeyError: 'C:/Users/rssav/Desktop/verify/Bank.sol'