search

microsoft / verisol

A formal verifier and analysis tool for Solidity Smart Contracts
Other
245 stars 46 forks source link

Unhandled Exception: cba.Util.InvalidProg: Cannot resolve __SolToBoogieTest_out.bpl #260

Open syscoopco opened 4 years ago

syscoopco commented 4 years ago

Any helps would be appreciated. See below the command, boogie.txt content and corral.txt content:

COMMAND EXECUTION:

$ VeriSol /home/user/work/verisol/ManicatoTokenVeriSol.sol ManicatoToken Command line args = {/home/user/work/verisol/ManicatoTokenVeriSol.sol, ManicatoToken} SpecFilesDir = /home/user/work/verisol ... running Solc on /home/user/work/verisol/ManicatoTokenVeriSol.sol ... running SolToBoogie to translate Solidity to Boogie Warning: A mapping with complex value type allowances of valuetype mapping (address => uint256) ... running /home/user/.dotnet/tools/boogie -doModSetAnalysis -inline:spec -noinfer -inlineDepth:4 -proc:BoogieEntry_* SolToBoogieTest_out.bpl *** Did not find a proof (see boogie.txt) ... running /home/user/.dotnet/tools/corral /recursionBound:4 /k:1 /main:CorralEntry_ManicatoToken /tryCTrace /printDataValues:1 SolToBoogieTest_out.bpl Error: Unhandled Exception: cba.Util.InvalidProg: Cannot resolve __SolToBoogieTest_out.bpl at cba.Util.BoogieUtil.ReadAndOnlyResolve(String filename) in /Users/mje/Code/corral/source/Util/BoogieUtil.cs:line 445 at cba.Driver.GetInputProgram(Configs config) in /Users/mje/Code/corral/source/Driver.cs:line 541 at cba.Driver.run(String[] args) in /Users/mje/Code/corral/source/Driver.cs:line 206 at cba.Driver.Main(String[] args) in /Users/mje/Code/corral/source/Driver.cs:line 44

*** Corral may have aborted abnormally (see corral.txt)

BOOGIE.TXT

Boogie program verifier version 2.4.1.10503, Copyright (c) 2003-2014, Microsoft. SolToBoogieTest_out.bpl(1319,22): Error: more than one declaration of function/procedure name: sub_SafeMath SolToBoogieTest_out.bpl(1410,22): Error: more than one declaration of function/procedure name: div_SafeMath SolToBoogieTest_out.bpl(1461,22): Error: more than one declaration of function/procedure name: mod_SafeMath SolToBoogieTest_out.bpl(1313,0): Error: wrong number of arguments in call to sub_SafeMath: 6 SolToBoogieTest_out.bpl(1404,0): Error: wrong number of arguments in call to div_SafeMath: 6 SolToBoogieTest_out.bpl(1455,0): Error: wrong number of arguments in call to mod_SafeMath: 6 6 name resolution errors detected in __SolToBoogieTest_out.bpl

CORRAL.TXT

SolToBoogieTest_out.bpl(1319,22): Error: more than one declaration of function/procedure name: sub_SafeMath SolToBoogieTest_out.bpl(1410,22): Error: more than one declaration of function/procedure name: div_SafeMath SolToBoogieTest_out.bpl(1461,22): Error: more than one declaration of function/procedure name: mod_SafeMath SolToBoogieTest_out.bpl(1313,0): Error: wrong number of arguments in call to sub_SafeMath: 6 SolToBoogieTest_out.bpl(1404,0): Error: wrong number of arguments in call to div_SafeMath: 6 SolToBoogieTest_out.bpl(1455,0): Error: wrong number of arguments in call to mod_SafeMath: 6 6 name resolution errors in __SolToBoogieTest_out.bpl

shuvendu-lahiri commented 4 years ago

If you can repro your issue into a small example, I am happy to look. Looks like something to do with duplicate safeMath libraries in VeriSol.

syscoopco commented 4 years ago

Hi Shuvendu,

You're almost right. This bug also has to do with the overloading of some functions within SafeMath library: sub, mod, ...No bug if not using SafeMath, so how long for this to be solved?

The error can be easily reproduced if you put the attached files in a same folder (let's say /verisol), and run the command: VeriSol /verisol/ManicatoTokenVeriSol.sol ManicatoToken

example.zip

syscoopco commented 4 years ago

Meanwhile, I can use a Verisol - Tolerant version of SafeMath ;-)