8000 Assign value of an array using another array · Issue #464 · flintlang/flint · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Assign value of an array using another array #464

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wmanshu opened this issue Aug 21, 2019 · 3 comments
Open

Assign value of an array using another array #464

wmanshu opened this issue Aug 21, 2019 · 3 comments
Labels
bug verifier

Comments

@wmanshu
Copy link
wmanshu commented Aug 21, 2019

Is it possible to support such assignment:

struct AData {
  var amount: [Int]

  public init(_amount: [Int])
  mutates (amount)
  {
    self.amount = _amount
  }
}

Also, this now gives anIllegal modification of variable not declared in 'mutates(...)' error
@wmanshu
Copy link
Author
wmanshu commented Aug 21, 2019

I am not sure if Flint support this. Because it can compile when --skip-verifier. But still shows error when not skip verifier

@mrRachar
Copy link
Collaborator

This is actually a known verifier issue, and is related to #436, and can be currently fixed by provided many type-level modifies identifiers. There is work being done on this right now in matteobilardi/flint which should hit later today.

mrRachar pushed a commit to matteobilardi/flint that referenced this issue Aug 22, 2019
Rationalise and simplify modifies arguments to relate to instance lev…
e93b936 
…el rather than type level properties

 - Two new AST passes to correct mutates type-level specification issues, fixing flintlang#434 flintlang#436 and hopefully fixing flintlang#464
  1. Generates called constructor information
  2. Updates the mutates statement using the properties of the states mutates variables and the constructor calling information
 - New semantic analysis extension to check as much as possible at that level that only the correct variables are mutated, as Boogie implementation does it this will enforce it by identifier
 - Corrected setter mutation variable identifier
 - Improved array and dictionary field access error messages
 - Fixed test suite to conform with improvements
@mrRachar mrRachar added the bug label Aug 22, 2019
@mrRachar
Copy link
Collaborator

Unfortunately it appears that this issue goes a little deeper, there seem to be some mutated array variables that aren't handled correctly by the verifier

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug verifier
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@mrRachar @wmanshu
0