Skip to content

Commit

Permalink
Apply suggestions from code review
Browse files Browse the repository at this point in the history
Co-authored-by: Linard Arquint <[email protected]>
  • Loading branch information
jcp19 and ArquintL authored Jan 12, 2024
1 parent f5ca811 commit 5bfc4c8
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
4 changes: 2 additions & 2 deletions src/main/resources/stubs/strings/strings.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -178,15 +178,15 @@ pure func Join(elems []string, sep string) (res string) /*{
// HasPrefix tests whether the string s begins with prefix.
pure
ensures ret == (len(s) >= len(prefix) && s[0:len(prefix)] == prefix)
decreases _
decreases
func HasPrefix(s, prefix string) (ret bool) {
return len(s) >= len(prefix) && (s[0:len(prefix)] == prefix)
}

// HasSuffix tests whether the string s ends with suffix.
pure
ensures ret == (len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix)
decreases _
decreases
func HasSuffix(s, suffix string) (ret bool) {
return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
}
Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/viper/gobra/frontend/Config.scala
Original file line number Diff line number Diff line change
Expand Up @@ -716,8 +716,8 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
)

val disableCheckTerminationPureFns: ScallopOption[Boolean] = opt[Boolean](
name = "disableTermCheckPureFns",
descr = "Do not check that all pure functions are marked with termination measures,",
name = "disablePureFunctsTerminationRequirement",
descr = "Do not enforce that all pure functions must have termination measures",
default = Some(ConfigDefaults.DefaultDisableCheckTerminationPureFns),
noshort = true,
)
Expand Down

0 comments on commit 5bfc4c8

Please sign in to comment.