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

Question

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

Answer 1

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.

Answer 2

It may be that the latest versions of SPARK support access types; it used not to, at all.

First, your Not_Null_My_Acc needs to be a subtype of My_Acc, unless you meant it to be a type in its own right.

Second, you can’t deallocate Self inside Replace and allocate a new value; Self is in-mode, & hence not writable.

Third, you can’t apply ’Old to Self, because

warning: attribute "Old" applied to constant has no effect

What you can say is

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