This project is read-only.

Working with arrays of pointers/ array of claims

Mar 27, 2011 at 10:13 PM
Edited Mar 27, 2011 at 10:13 PM

Hi all, 

since it is not possible to assign ownership of an array of claims (as well as any other array of pointers) in a single statement, I am trying to do this in a loop now. The problem is that it is also not possible to include an array of claims into a writes clause of a loop where the ownership transfer occurs. So I have to put the whole span of an object containing these claims into the writes clause of the loop. Now, if I have two different arrays of claims (of different size) in the span of the object, and want to initialize these arrays in two different loops I have a problem. Vcc needs to know that both arrays are fresh in order to wrap the object containing these claims. And I cannot find a way to transfer the knowledge of freshness of the first array through the second loop (which has the whole span of the object in the writes clause).


Is there a way out of the problem?

And are there any plans to introduce set comprehension to VCC in the future?  If yes, maybe then it is a good idea to simply model this operation with assumes for now...

Mar 28, 2011 at 9:06 AM

Hi Mikhail,

  when you say "array of claims" you mean "array of claim pointers", right? I have a feeling of what your problem could be, but I'm not sure I fully understand the problem from the description alone - if you want, send me a sample offline or post here (if possible include the portions where the claims are created)... And, yes, I guess the plan is to have set comprehension at some point.

  Best, Mark


Mar 28, 2011 at 4:28 PM

Hi Mark,

yes, I am talking about the array of claim pointers actually. The problem is that I can not specify writes clause in a way that it only takes this array and does not include the other components of the span of the object. Thus, I could not maintain freshness of an array of claims through a function call. But it seems that this problem can be solved with the unchanged() predicate on all the pointers in the array. Though in the end its still an ugly solution.