Fix issue 491

[Felalolf]

This PR:

• Fixes a bug in the encoding context, where using the copy constructor would cause the freshname generator to break.
• Makes the length argument of array type expressions constant. This makes our treatment of types more consistent.
• Fixes an unsoundness with length.
• Fixes an unsoundness where panics that are caused by referencing L-values were not detected. Instead of checking that every L-value is safe immediately, we check that all usages of L-values are safe. See safeReference for more details.
• Fixes several unsoundnesses in the encoding of zero sized types.
• Adds an UncheckedRef node. The node is necessary to make our encoding modular.
• Renames InterfaceReceiverIsNilReason to the more general ReceiverIsNilReason.
• Fixes some error codes. Previously, assignments and dereferencs sometimes failed with exhale and call error, respectively, and now fail with assignment and deref error, respectively.

There is one failing test. The test fails due to an error in the desugaring of closures. I will most likely add an IgnoreFile annotation and open a separate issue. The currently generated internal representation should fail since it contains an unsafe dereference.

[jcp19]

Is this meant to only check locations? If so, I would probably make the param type more restrictive (i.e., in.Location)

[Felalolf]

No, it also checks expressions (in particular, see the body of the method, where we use it to check whether the receiver of an index and field-ref expression cannot be nil).

[Felalolf]

I could change it to something along the lines of:

private def cannotBeNil(l: in.Location): Boolean = {
  def aux(e: in.Expr): Boolean = {
    // body of cannotBeNil
  }
  aux(l)
}

[Felalolf]

This PR still has issues because of which it is not merged

[jcp19]

This PR still has issues because of which it is not merged

For reference, the issue mentioned here is that Gobra is often not able to prove non-nilness of memory locations that are obviously non-nil. Consider the simple example below

requires  8 <= len(raw)
preserves forall i int :: { &raw[i] } 0 <= i && i < len(raw) ==>
	acc(&raw[i])
func DecodeFromBytes(raw []byte) {
	assert forall i int :: 0 <= i && i < len(raw[2:4]) ==>
		&raw[2:4][i] == &raw[2 + i]
}

In the current status of the PR, we get the following error:

[info] Error at: </Users/joao/000491-bug.gobra:7:58> Reading might fail. 
[info] The receiver raw[2:4][i] might be nil