Infinite Ghost Loops

[gottschali]

The following program verifies on 97f0988

func fun2() int {
	//@ ghost for {}
	return 0
}
func main() {
	fun2()
}

By the ghost erasure property, it should not verify since with ghost code it loops infinitely but without terminates.

@jcp19 mentioned this could be fixed by adding a syntactical check that requires a termination measure for ghost loops.