You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The idea would be to use similar injection of assumptions on well-typedness of heap as used in full-imperative.
Instead of using Array, we could use a list of pairs for the heap.
The idea is that SharedCell is not special in stainless. The shared cell as data is indeed only a wrapper for some integer data type (unbounded if want to postpone reasoning about heap overflow).
The key is that it's the update and apply of the ref cell that refer to a global mutable object.
The beauty is that this can be made to work with the existing non-shared memory model. The cells themselves are not shared, it's just that some of them may store identical integers.
Maybe something like this would be a sketch of the model we want, if we additionally relax @extern var T to be ignored for the purpose of alias analysis in case class parameters.
The text was updated successfully, but these errors were encountered: