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

[syscoopco]

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]

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]

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]

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