microsoft / verisol

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

modifier with invocations #82

Closed garbervetsky closed 5 years ago

garbervetsky commented 5 years ago

A modifier invoking a helper function fails to to parse. The error seems to be related to not having the field currentContract instantiated.

Unhandled Exception: System.ArgumentNullException: Value cannot be null. Parameter name: key at System.ThrowHelper.ThrowArgumentNullException(ExceptionArgument argument) at System.Collections.Generic.Dictionary2.FindEntry(TKey key) at System.Collections.Generic.Dictionary2.ContainsKey(TKey key) at SolToBoogie.TranslatorContext.HasEventNameInContract(ContractDefinition contract, String eventName) in .\verisol\Sources\SolToBoogie\TranslatorContext.cs:line 279 at SolToBoogie.ProcedureTranslator.Visit(FunctionCall node) in C:\Users\diegog\Source\Repos\verisol\Sources\SolToBoogie\ProcedureTranslator.cs:line 1254

pragma solidity ^0.4.24; contract ModifierFunc { function isValid(uint id) public view returns (bool) { return (id > 0); } modifier valid(uint id) { require(isValid(id), "id is not valid"); // this invocation produces an exception _; } }

shuvendu-lahiri commented 5 years ago

@rongpan would you be able to take a quick look at this case?

rongpan commented 5 years ago

85