adapts 'builtin' and 'stubs' packages to latest changes in Viper

viperproject · Jul 3, 2023 · 08bfba3 · 08bfba3
1 parent a18c450
commit 08bfba3
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/src/main/resources/stubs/strconv/atoi.gobra b/src/main/resources/stubs/strconv/atoi.gobra
@@ -44,6 +44,7 @@ pure func (e *NumError) Unwrap() error { return e.Err }
 ghost
 requires exp >= 0
 ensures res == (exp == 0 ? 1 : (base * Exp(base, exp - 1)))
+decreases exp
 pure func Exp(base int, exp int) (res int) {
 	return exp == 0 ? 1 : (base * Exp(base, exp - 1))
 }

diff --git a/src/main/resources/stubs/strings/strings.gobra b/src/main/resources/stubs/strings/strings.gobra
@@ -202,6 +202,7 @@ func Map(mapping func(rune) rune, s string) string
 // the result of (len(s) * count) overflows.
 requires count >= 0
 ensures res == (count == 0? "" : s + Repeat(s, count - 1))
+decreases count
 pure func Repeat(s string, count int) (res string) /*{
 	if count == 0 {
 		return ""