Incomplete Slice Allocation Spec

[ArquintL]

The Go spec is again a bit vague but the best I found is the following statement:

That is, executing

make([]T, length, capacity)

produces the same slice as allocating an array and slicing it, so these two expressions are equivalent:

make([]int, 50, 100)
new([100]int)[0:50]

Comparing this to our current encoding:

gobra/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala

Lines 131 to 144 in 25474a2

	/**
	* Encodes the allocation of a new slice
	*
	* [r := make([]T, len, cap)] ->
	* asserts 0 <= [len] && 0 <= [cap] && [len] <= [cap]
	* var a [ []T ]
	* inhales cap(a) == [cap]
	* inhales len(a) == [len]
	* inhales forall i: int :: {loc(a, i)} 0 <= i && i < [cap] ==> Footprint[ a[i] ]
	* inhales forall i: int :: {loc(a, i)} 0 <= i && i < [len] ==> [ a[i] == dfltVal(T) ]
	* r := a
	*
	* R[ sliceLit(E) ] -> R[ arrayLit(E)[0:|E|] ]
	*/

I'd thus argue that the inhale statement on line 140 can be strengthened to

- inhales forall i: int :: {loc(a, i)} 0 <= i && i < [len] ==> [ a[i] == dfltVal(T) ] 
+ inhales forall i: int :: {loc(a, i)} 0 <= i && i < [cap] ==> [ a[i] == dfltVal(T) ]