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.

[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

[ArquintL]

The handling of zero-sized data has been extracted and merged via #1022 and #1023. This PR just got updated by merging in master to (resolve its conflicts &) reduce its diff

[jcp19]

@ArquintL feedback incorporated. Can be merged together with #1077, otherwise, it leads to very bad incompletenesses.