search

flintlang / flint

The Flint Programming Language for Smart Contracts
MIT License
245 stars 18 forks source link

Problem with Init() #455

Closed wmanshu closed 5 years ago

wmanshu commented 5 years ago

If I initialize this global variable var bids : [Address : [Bid]] using self.bids = [:[]]. I get this error:

Expected ']' in dictionary literal expression at line 33, column 19:
    self.bids = [:[]]

If I initialize it byself.bids = [:], then error message says post condition not holds Where Bid is a self-defined struct

mrRachar commented 5 years ago

Firstly, the syntax [:[]] doesn't really make any sense. I finally figured out what you were talking about with self.bids = [:], and you're right, any contract or struct field equivalent to 

contract ExampleContract {
  var x: [Address: [ExampleStruct]] = [:]  // Also fails with `let`
}

currently fail a Boogie post-condition, that must be generated somewhere by the verification system. I am having a look into this problem now.

It would be more helpful in the future to provide simplified but implicitly complete examples of issues rather than your code to help diagnose them. For example, your fields are completely out of context, etc.