Fix issue 796

src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala

@@ -105,7 +105,12 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl =>
       }
       if (firstChecks.isEmpty) latterChecks else firstChecks
 
-    case n@PForStmt(_, cond, _, _, _) => isExpr(cond).out ++ comparableTypes.errors(exprType(cond), BooleanT)(n)
+    case n@PForStmt(_, cond, _, spec, _) =>
+      val isGhost = isEnclosingGhost(n)
+      val noTerminationMeasureMsg = "Loop occurring in ghost context does not have a termination measure"
+      isExpr(cond).out ++
+        comparableTypes.errors(exprType(cond), BooleanT)(n) ++
+        error(n, noTerminationMeasureMsg, isGhost && spec.terminationMeasure.isEmpty)
 
     case PShortForRange(range, shorts, _, _, _) =>
       underlyingType(exprType(range.exp)) match {

src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra

@@ -77,6 +77,7 @@ func ParallelSum(s []int) (res int) {
 		invariant forall j int :: 0 <= j && j < n ==> acc(&s[j], 1/2)
 		invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!>
 		invariant forall j int :: 0 <= j && j < n ==> (j < i ? acc(&seenSlice[j], 1/2) && seenSlice[j] == s[j] : sync.InjEval(tokens[j], j))
+		decreases n - i
 		for i:=0; i < n; i++ {
 			unfold sync.InjEval(tokens[i], i)
 			unfold locHasVal!<&seenSlice[i],s[i]!>()

src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra

@@ -127,6 +127,7 @@ func SearchReplace(s []int, x, y int) {
     invariant forall j int :: 0 <= j &&
       j < (i == len(seqs) ? len(s) : i * workRange) ==>
       acc(&s[j]) && s[j] == (s0[j] == x ? y : s0[j])
+    decreases len(pseqs) - i
     for i := 0; i != len(pseqs); i++ {
       unfold sync.InjEval(pseqs[i],i)
       low := i * workRange

src/test/resources/regressions/examples/evaluation/parallel_sum.gobra

@@ -77,6 +77,7 @@ func ParallelSum(s []int) (res int) {
 		invariant forall j int :: 0 <= j && j < n ==> acc(&s[j], 1/2)
 		invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!>
 		invariant forall j int :: 0 <= j && j < n ==> (j < i ? acc(&seenSlice[j], 1/2) && seenSlice[j] == s[j] : sync.InjEval(tokens[j], j))
+		decreases n - i
 		for i:=0; i < n; i++ {
 			unfold sync.InjEval(tokens[i], i)
 			unfold locHasVal!<&seenSlice[i],s[i]!>()

src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra

@@ -128,6 +128,7 @@ func SearchReplace(s []int, x, y int) {
     invariant forall j int :: 0 <= j &&
       j < (i == len(seqs) ? len(s) : i * workRange) ==>
       acc(&s[j]) && s[j] == (s0[j] == x ? y : s0[j])
+    decreases len(pseqs) - i
     for i := 0; i != len(pseqs); i++ {
       unfold sync.InjEval(pseqs[i],i)
       low := i * workRange

src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra

@@ -77,6 +77,7 @@ func ParallelSum(s []int) (res int) {
 		invariant forall j int :: 0 <= j && j < n ==> acc(&s[j], 1/2)
 		invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!>
 		invariant forall j int :: 0 <= j && j < n ==> (j < i ? acc(&seenSlice[j], 1/2) && seenSlice[j] == s[j] : sync.InjEval(tokens[j], j))
+		decreases n - i
 		for i:=0; i < n; i++ {
 			unfold sync.InjEval(tokens[i], i)
 			unfold locHasVal!<&seenSlice[i],s[i]!>()

src/test/resources/regressions/examples/parallel_search_replace_shared.gobra

@@ -139,6 +139,7 @@ func SearchReplace(s []int, x, y int) {
     invariant forall j int :: 0 <= j &&
       j < (i == len(seqs) ? len(s) : i * workRange) ==>
       acc(&s[j]) && s[j] == (s0[j] == x ? y : s0[j])
+    decreases len(pseqs) - i
     for i := 0; i != len(pseqs); i++ {
       unfold sync.InjEval(pseqs[i],i)
       low := i * workRange

src/test/resources/regressions/features/sequences/seq-index-fail10.gobra

@@ -5,6 +5,9 @@ package pkg
 
 requires 0 < len(xs)
 func foo(ghost xs seq[bool]) {
-  //:: ExpectedOutput(for_loop_error:seq_index_exceeds_length_error)
-  ghost for ;xs[42]; { }
+  ghost {
+    decreases
+    //:: ExpectedOutput(for_loop_error:seq_index_exceeds_length_error)
+    for ;xs[42]; { break }
+  }
 }

src/test/resources/regressions/features/sequences/seq-index-fail9.gobra

@@ -5,6 +5,9 @@ package pkg
 
 requires 0 < len(xs)
 func foo(ghost xs seq[bool]) {
-  //:: ExpectedOutput(for_loop_error:seq_index_negative_error)
-  ghost for ;xs[-1]; { }
+  ghost {
+    decreases
+    //:: ExpectedOutput(for_loop_error:seq_index_negative_error)
+    for ;xs[-1]; { break }
+  }
 }

src/test/resources/regressions/features/sequences/seq-index-simple1.gobra

@@ -39,5 +39,8 @@ func example7(ghost xs seq[bool]) {
 
 requires 0 < len(xs)
 func example8(ghost xs seq[bool]) {
-  ghost for ;xs[0]; { }
+  ghost {
+    decreases
+    for ;xs[0]; { break }
+  }
 }

src/test/resources/regressions/issues/000796.gobra

@@ -0,0 +1,20 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue000796
+
+func m1() {
+	//:: ExpectedOutput(type_error)
+	ghost for {
+
+	}
+}
+
+func m2() {
+	ghost {
+		//:: ExpectedOutput(type_error)
+		for {
+
+		}
+	}
+}