Several errors in WesternUnion.flint

[wmanshu]

First error located here at this function, the error message is

Not accessing property of a struct: errorType
WesternUnion.flint@71:11:17
Fatal error: flint/Sources/Verifier/Boogie/Statement+Expression.swift, line 831

function example, so the line 71 is the post condition line:

  public func withdraw()
    mutates (accounts, Wei.rawValue)
    post (account[customer].getRawValue() == 0)
  {
    var amt: Wei = Wei(&accounts[customer])
    send(customer, &amt)
  }

[wmanshu]

This problem solved

---

WesternUnion :: (manager) {
  public func addCustomer(customer: Address)
    mutates (customers, numCustomers)
    post (customers[prev(numCustomers)] == customer && arrayEach(c, customers, c == prev(c) || c == customer))
// I was trying to avoid forall so I used arrayEach here
  {
    customers[numCustomers] = customer
    numCustomers += 1 //Issue if we don't increment numCustomers
  }
}

I got this error message when compiling

Potential out-of-bounds error: Could not verify that array access is within array bounds at line 53, column 5:
    customers[numCustomers] = customer 

However, nowhere defines the array bounds

---

From the program above I tried to change the post condition by adding && arrayContains(customers, customer), so it becomes

post (customers[prev(numCustomers)] == customer && arrayEach(c, customers, c == prev(c) || c == customer) && arrayContains(customers, customer))

Logically, it is definitely correct since the (numCustomers - 1)th element of the customers array is the customer, but I get a new error and which fails the verification. And the error message is just

Error in /home/manshu/flint/examples/valid/WesternUnion.flint:
Could not verify post-condition holds by end of function at line 44, column 10:
  public func addCustomer(customer: Address)

[mrRachar]

You seem to have managed to get the issue down to the send function but unfortunately right now this cannot be part of any proof, as its Boogie representation havocs all values in the function. This issue is currently tracked at #456.