Search code examples
adaspark-ada

How is the `'Old` attribute in a **Post** contract handled for access types that might got deallocated inside the function or procedure?

Assume having the following setup:

type My is new Integer;
type My_Acc is access My;

procedure Replace(Self : in out My_Acc; New_Int : Integer)
  with Pre => New_Int /= Self.all, Post => Self'Old.all /= Self.all;

Note: Code above might not be fully valid, but I hope the concept is understandable.

Now what happens if Unchecked_Deallocation() is used on Self inside Replace and a new Integer is allocated and set to Self (This should result in Self'Old pointing to a now invalid memory location)?

Does Ada keep kind of a snapshot where Self'Old points to the previous memory location, but before Unchecked_Deallocation() is executed?

If Self'Old would get invalid for use in the Post contract, how could you still access the previous value? Is it possible to create a manual snapshot in the Pre contract that can then be used in Post? Maybe it can be achieved using Ghost_Code?

I want to make everything in Spark, in case that changes something.

Edit: Fixed Self to in out as mentioned by Simon Wright.

Edit: Fixed type of Self to allow null

Solution

  • In ARM 6.1.1(26ff) it says

    Each X'Old in a postcondition expression that is enabled denotes a constant that is implicitly declared at the beginning of the subprogram body, entry body, or accept statement.

    The implicitly declared entity denoted by each occurrence of X'Old is declared as follows: ...

    X'Old : constant S := X;

    ... in other words, nothing fancy is expected, just a straight copy of (in this case) Self: not Self.all.

    So, if your Replace deallocates Self, then Self’Old is a dangling reference, and erroneous.

    I suggested previously that changing the postcondition to

    Post => Self.all'Old /= Self.all;

    would be safe; why wouldn’t that meet your requirements? is there something going on you haven’t told us about?

    Note the subtle difference between Self’Old.all and Self.all’Old. The first one takes a copy of Self as it was before the call, which gets dereferenced after the call (by which time it’s pointing into hyperspace), while the second one dereferences the prior Self and copies the integer value it finds there; on return that’s still valid.