From 08bfba3cbd3bc4e37aaca49fe2ef8f63d156962b Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Mon, 3 Jul 2023 09:48:45 +0200 Subject: [PATCH] adapts 'builtin' and 'stubs' packages to latest changes in Viper --- src/main/resources/stubs/strconv/atoi.gobra | 1 + src/main/resources/stubs/strings/strings.gobra | 1 + 2 files changed, 2 insertions(+) diff --git a/src/main/resources/stubs/strconv/atoi.gobra b/src/main/resources/stubs/strconv/atoi.gobra index 3b94ea29d..454e456e0 100644 --- 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 index 22dbf3819..0307bf577 100644 --- 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 ""