Generating incorrect triggers

[gavinleroy]

For the following Gobra code:

package main

const HopLen = 16

requires len(raw) > HopLen * 2
requires forall i int :: 0 <= i && i < len(raw) ==> acc(&raw[i])
func DecodeFromBytes(raw []byte) (err int) {
	assert forall i int :: { &raw[6:6+HopLen][i] } 0 <= i && i < len(raw[6:6+HopLen]) ==> &raw[6:6+HopLen][i] == &raw[i+6]
	return 0
}

If you run this from Gobra, it will verify successfully, however, passing --printVpr and running it on the generated Viper program will result in an invalid trigger exception.
Within the trigger, there is a 6 + constant_blah_blah which is disallowed.

Silicon output for reference:

Silicon found 1 error in 3.91s:
  [0] { (ShArrayloc((sarray(ssliceFromSlice_Ref(raw_V0_CN0, 6, 6 + constant_HopLen_4b5075e4_G())): ShArray[Ref]), sadd((soffset(ssliceFromSlice_Ref(raw_V0_CN0, 6, 6 + constant_HopLen_4b5075e4_G())): Int), i_V2)): Ref) } is not a valid Trigger (test.gobra.vpr@312.31--312.244)

[jcp19]

This issue should no longer apply. On one hand, we fixed an issue where Gobra was generating ill-formed triggers for expressions involving maps. On the other hand, Viper was previously rejecting valid triggers, like the one shown in this example. This should be fixed in recent versions of Viper.