diff --git a/docs/tutorial.md b/docs/tutorial.md index cace56515..d09f6bcf5 100644 --- a/docs/tutorial.md +++ b/docs/tutorial.md @@ -401,7 +401,7 @@ pure func toSeq(s []int) (res seq[int]) { Gobra supports many of Go's native types, namely integers (`int`, `int8`, `int16`, `int32`, `int64`, `byte`, `uint8`, `rune`, `uint16`, `uint32`, `uint64`, `uintptr`), strings, structs, pointers, arrays, slices, interfaces, and channels. Note that currently the support for strings and specific types of integers such as `rune` is very limited. -In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`|set1|`). +In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`len(set1)`). ## Interfaces @@ -680,4 +680,4 @@ java -Xss128m -jar gobra.jar -i [FILES_TO_VERIFY] To check the full list of flags available in Gobra, run the command ```bash java -jar gobra.jar -h -``` \ No newline at end of file +``` 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 "" diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala index cb9e18620..3012d1d16 100644 --- a/src/main/scala/viper/gobra/Gobra.scala +++ b/src/main/scala/viper/gobra/Gobra.scala @@ -293,7 +293,7 @@ class Gobra extends GoVerifier with GoIdeVerifier { private def performViperEncoding(program: Program, config: Config, pkgInfo: PackageInfo): Either[Vector[VerifierError], BackendVerifier.Task] = { if (config.shouldViperEncode) { - Right(Translator.translate(program, pkgInfo)(config)) + Translator.translate(program, pkgInfo)(config) } else { Left(Vector()) } diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index 0eff086cd..a87ad2d99 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -3736,7 +3736,7 @@ object Desugar { case t: Type.AdtClauseT => val tAdt = Type.AdtT(t.adtT, t.context) val adt: in.AdtT = in.AdtT(nm.adt(tAdt), addrMod) - val fields: Vector[in.Field] = (t.fields map { case (key: String, typ: Type) => + val fields: Vector[in.Field] = (t.fieldsWithTypes map { case (key: String, typ: Type) => in.Field(nm.adtField(key, tAdt), typeD(typ, Addressability.mathDataStructureElement)(src), true)(src) }).toVector in.AdtClauseT(idName(t.decl.id, t.context.getTypeInfo), adt, fields, addrMod) diff --git a/src/main/scala/viper/gobra/frontend/info/base/Type.scala b/src/main/scala/viper/gobra/frontend/info/base/Type.scala index c0eb1bdf1..5604d4e22 100644 --- a/src/main/scala/viper/gobra/frontend/info/base/Type.scala +++ b/src/main/scala/viper/gobra/frontend/info/base/Type.scala @@ -58,7 +58,17 @@ object Type { case class AdtT(decl: PAdtType, context: ExternalTypeInfo) extends Type - case class AdtClauseT(fields: Map[String, Type], decl: PAdtClause, adtT: PAdtType, context: ExternalTypeInfo) extends Type + case class AdtClauseT(fieldsToTypes: Map[String, Type], fields: Vector[String], decl: PAdtClause, adtT: PAdtType, context: ExternalTypeInfo) extends Type { + require(fields.forall(fieldsToTypes.isDefinedAt), "there must be a type for each key") + + def typeAt(idx: Int): Type = { + require(0 <= idx && idx < fields.size, s"index $idx is not within range of ADT fields (size ${fields.size})") + fieldsToTypes(fields(idx)) + } + + lazy val fieldsWithTypes: Vector[(String, Type)] = fields.map(f => (f, fieldsToTypes(f))) + lazy val fieldTypes: Vector[Type] = fieldsWithTypes.map(_._2) + } case class MapT(key: Type, elem: Type) extends PrettyType(s"map[$key]$elem") diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala index 4c0bd33fb..e79d3a9d3 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala @@ -184,7 +184,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => if (elems.isEmpty) { successProp } else if (elems.exists(_.key.nonEmpty)) { - val tmap: Map[String, Type] = a.fields + val tmap: Map[String, Type] = a.fieldsToTypes failedProp("for adt literals either all or none elements must be keyed", !elems.forall(_.key.nonEmpty)) and @@ -198,7 +198,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl => }) } else if (elems.size == a.fields.size) { propForall( - elems.map(_.exp).zip(a.fields.values), + elems.map(_.exp).zip(a.fieldTypes), compositeValAssignableTo ) } else { diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala index b9b9da4db..7925531d6 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala @@ -94,9 +94,12 @@ trait NameResolution { case tree.parent.pair(decl: PAdtClause, adtDecl: PAdtType) => AdtClause(decl, adtDecl, this) - case tree.parent.pair(decl: PMatchBindVar, adt: PMatchAdt) => MatchVariable(decl, adt, this) case tree.parent.pair(decl: PMatchBindVar, tree.parent.pair(_: PMatchStmtCase, matchE: PMatchStatement)) => - MatchVariable(decl, matchE.exp, this) + MatchVariable(decl, matchE.exp, this) // match full expression of match statement + case tree.parent.pair(decl: PMatchBindVar, tree.parent.pair(_: PMatchExpCase, matchE: PMatchExp)) => + MatchVariable(decl, matchE.exp, this) // match full expression of match expression + case tree.parent.pair(decl: PMatchBindVar, adt: PMatchAdt) => + MatchVariable(decl, adt, this) // match part of subexpression case c => Violation.violation(s"This case should be unreachable, but got $c") } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala index 979af8e2e..40ad6d048 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala @@ -145,8 +145,8 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case Some(p: ap.DomainFunction) => FunctionT(p.symb.args map p.symb.context.typ, p.symb.context.typ(p.symb.result)) case Some(p: ap.AdtClause) => - val fields = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)).toMap - AdtClauseT(fields, p.symb.decl, p.symb.adtDecl, this) + val fields = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)) + AdtClauseT(fields.toMap, fields.map(_._1), p.symb.decl, p.symb.adtDecl, this) case Some(p: ap.AdtField) => p.symb match { case AdtDestructor(decl, _, context) => context.symbType(decl.typ) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala index 0f1b234fd..c62376ec4 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala @@ -157,8 +157,8 @@ trait IdTyping extends BaseTyping { this: TypeInfoImpl => // ADT clause is special since it is a type with a name that is not a named type case a: AdtClause => - val types = a.fields.map(f => f.id.name -> a.context.symbType(f.typ)).toMap - AdtClauseT(types, a.decl, a.adtDecl, this) + val fields = a.fields.map(f => f.id.name -> a.context.symbType(f.typ)) + AdtClauseT(fields.toMap, fields.map(_._1), a.decl, a.adtDecl, this) case BuiltInType(tag, _, _) => tag.typ case _ => violation(s"expected type, but got $id") diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala index 15f131f3c..bbfa0a00f 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala @@ -155,8 +155,8 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => // ADT clause is special since it is a type with a name that is not a named type case Some(p: ap.AdtClause) => - val types = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)).toMap - AdtClauseT(types, p.symb.decl, p.symb.adtDecl, p.symb.context) + val fields = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)) + AdtClauseT(fields.toMap, fields.map(_._1), p.symb.decl, p.symb.adtDecl, p.symb.context) case _ => violation(s"expected type, but got $n") } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala index 5e2d996ac..a071b79af 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala @@ -41,8 +41,10 @@ trait GhostIdTyping { this: TypeInfoImpl => case func: DomainFunction => FunctionT(func.args map func.context.typ, func.context.typ(func.result.outs.head)) case AdtClause(decl, adtDecl, context) => + val fields = decl.args.flatMap(_.fields).map(f => f.id.name -> context.symbType(f.typ)) AdtClauseT( - decl.args.flatMap(_.fields).map(f => f.id.name -> context.symbType(f.typ)).toMap, + fields.toMap, + fields.map(_._1), decl, adtDecl, context @@ -50,10 +52,8 @@ trait GhostIdTyping { this: TypeInfoImpl => case MatchVariable(decl, p, context) => p match { case PMatchAdt(clause, fields) => - val argTypeWithIndex = context.symbType(clause).asInstanceOf[AdtClauseT].decl.args.flatMap(_.fields).map(_.typ).zipWithIndex - val fieldsWithIndex = fields.zipWithIndex - val fieldIndex = fieldsWithIndex.iterator.find(e => e._1 == decl).get._2 - context.symbType(argTypeWithIndex.iterator.find(e => e._2 == fieldIndex).get._1) + val clauseT = context.symbType(clause).asInstanceOf[AdtClauseT] + clauseT.typeAt(fields.indexOf(decl)) case e: PExpression => context.typ(e) case _ => violation("untypeable") diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala index 7eff705f7..3ab5e4a53 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala @@ -54,8 +54,8 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => case m: PMatchPattern => m match { case PMatchAdt(clause, fields) => symbType(clause) match { case t: AdtClauseT => - val fieldTypes = fields map typ - val clauseFieldTypes = t.decl.args.flatMap(f => f.fields).map(f => symbType(f.typ)) + val fieldTypes = fields.map(typ) + val clauseFieldTypes = t.fieldTypes error(m, s"Expected ${clauseFieldTypes.size} patterns, but got ${fieldTypes.size}", clauseFieldTypes.size != fieldTypes.size) ++ fieldTypes.zip(clauseFieldTypes).flatMap(a => assignableTo.errors(a)(m)) case _ => violation("Pattern matching only works on ADT Literals") @@ -292,10 +292,8 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => w eq _ } val adtClauseT = underlyingType(typeSymbType(c)).asInstanceOf[AdtClauseT] - val flatFields = adtClauseT.decl.args.flatMap(f => f.fields) - if (index < flatFields.size) { - val field = flatFields(index) - typeSymbType(field.typ) + if (index < adtClauseT.fields.size) { + adtClauseT.typeAt(index) } else UnknownType // Error is found when PMatchADT is checked higher up the ADT case tree.parent.pair(_: PMatchExpCase, m: PMatchExp) => exprType(m.exp) diff --git a/src/main/scala/viper/gobra/reporting/Message.scala b/src/main/scala/viper/gobra/reporting/Message.scala index 61530d91b..418e8e4db 100644 --- a/src/main/scala/viper/gobra/reporting/Message.scala +++ b/src/main/scala/viper/gobra/reporting/Message.scala @@ -173,6 +173,14 @@ case class GeneratedViperMessage(taskName: String, inputs: Vector[String], vprAs lazy val vprAstFormatted: String = silver.ast.pretty.FastPrettyPrinter.pretty(vprAst()) } +case class TransformerFailureMessage(inputs: Vector[String], result: Vector[VerifierError]) extends GobraMessage { + override val name: String = s"transformer_failure_message" + + override def toString: String = s"transformer_failure_message(" + + s"files=$inputs, " + + s"failures=${result.map(_.toString).mkString(",")})" +} + case class ChoppedViperMessage(inputs: Vector[String], idx: Int, vprAst: () => vpr.Program, backtrack: () => BackTranslator.BackTrackInfo) extends GobraMessage { override val name: String = s"chopped_viper_message" diff --git a/src/main/scala/viper/gobra/reporting/Reporter.scala b/src/main/scala/viper/gobra/reporting/Reporter.scala index f4cffc761..0c6d7cb66 100644 --- a/src/main/scala/viper/gobra/reporting/Reporter.scala +++ b/src/main/scala/viper/gobra/reporting/Reporter.scala @@ -66,6 +66,7 @@ case class FileWriterReporter(name: String = "filewriter_reporter", } case m:ParserErrorMessage if streamErrs => m.result.foreach(err => logger.error(s"Error at: ${err.formattedMessage}")) case m:TypeCheckFailureMessage if streamErrs => m.result.foreach(err => logger.error(s"Error at: ${err.formattedMessage}")) + case m:TransformerFailureMessage if streamErrs => m.result.foreach(err => logger.error(s"Error at: ${err.formattedMessage}")) case _ => // ignore } diff --git a/src/main/scala/viper/gobra/reporting/VerifierError.scala b/src/main/scala/viper/gobra/reporting/VerifierError.scala index 858c2f2ae..a2877f4cb 100644 --- a/src/main/scala/viper/gobra/reporting/VerifierError.scala +++ b/src/main/scala/viper/gobra/reporting/VerifierError.scala @@ -56,11 +56,15 @@ case class DiamondError(message: String) extends VerifierError { val id = "diamond_error" } -case class TimeoutError(message: String) extends VerifierError { +case class TimeoutError(message: String) extends VerifierError { val position: Option[SourcePosition] = None val id = "timeout_error" } +case class ConsistencyError(message: String, position: Option[SourcePosition]) extends VerifierError { + val id = "consistency_error" +} + sealed trait VerificationError extends VerifierError { def info: Source.Verifier.Info diff --git a/src/main/scala/viper/gobra/translator/Translator.scala b/src/main/scala/viper/gobra/translator/Translator.scala index 537b7d94f..63334f790 100644 --- a/src/main/scala/viper/gobra/translator/Translator.scala +++ b/src/main/scala/viper/gobra/translator/Translator.scala @@ -10,17 +10,28 @@ package viper.gobra.translator import viper.gobra.ast.internal.Program import viper.gobra.backend.BackendVerifier import viper.gobra.frontend.{Config, PackageInfo} -import viper.gobra.reporting.GeneratedViperMessage +import viper.gobra.reporting.{ConsistencyError, GeneratedViperMessage, TransformerFailureMessage, VerifierError} import viper.gobra.translator.context.DfltTranslatorConfig import viper.gobra.translator.encodings.programs.ProgramsImpl import viper.gobra.translator.transformers.{AssumeTransformer, TerminationTransformer, ViperTransformer} import viper.gobra.util.Violation +import viper.silver.ast.{AbstractSourcePosition, SourcePosition} import viper.silver.ast.pretty.FastPrettyPrinter +import viper.silver.verifier.AbstractError import viper.silver.{ast => vpr} object Translator { - def translate(program: Program, pkgInfo: PackageInfo)(config: Config): BackendVerifier.Task = { + private def createConsistencyErrors(errs: Seq[AbstractError]): Vector[ConsistencyError] = + errs.map(err => { + val pos = err.pos match { + case sp: AbstractSourcePosition => Some(new SourcePosition(sp.file, sp.start, sp.end)) + case _ => None + } + ConsistencyError(err.readableMessage, pos) + }).toVector + + def translate(program: Program, pkgInfo: PackageInfo)(config: Config): Either[Vector[VerifierError], BackendVerifier.Task] = { val translationConfig = new DfltTranslatorConfig() val programTranslator = new ProgramsImpl() val task = programTranslator.translate(program)(translationConfig) @@ -30,17 +41,25 @@ object Translator { new TerminationTransformer ) - val transformedTask = transformers.foldLeft(task) { - case (t, transformer) => transformer.transform(t) - .fold(errs => Violation.violation(s"Applying transformer ${transformer.getClass.getSimpleName} resulted in errors: ${errs.toString}"), identity) + val transformedTask = transformers.foldLeft[Either[Vector[VerifierError], BackendVerifier.Task]](Right(task)) { + case (Right(t), transformer) => transformer.transform(t).left.map(createConsistencyErrors) + case (errs, _) => errs } if (config.checkConsistency) { - val errors = transformedTask.program.checkTransitively - if (errors.nonEmpty) Violation.violation(errors.toString) + transformedTask + .flatMap(task => { + val consistencyErrs = task.program.checkTransitively + if (consistencyErrs.isEmpty) Right(()) + else Left(createConsistencyErrors(consistencyErrs)) + }) + .left.map(errs => Violation.violation(errs.toString)) } - config.reporter report GeneratedViperMessage(config.taskName, config.packageInfoInputMap(pkgInfo).map(_.name), () => sortAst(transformedTask.program), () => transformedTask.backtrack) + val inputs = config.packageInfoInputMap(pkgInfo).map(_.name) + transformedTask.fold( + errs => config.reporter report TransformerFailureMessage(inputs, errs), + task => config.reporter report GeneratedViperMessage(config.taskName, inputs, () => sortAst(task.program), () => task.backtrack)) transformedTask } diff --git a/src/test/resources/regressions/features/closures/closures-calldesc2.gobra b/src/test/resources/regressions/features/closures/closures-calldesc2.gobra index 6f39c6b9f..bc8ffc64c 100644 --- a/src/test/resources/regressions/features/closures/closures-calldesc2.gobra +++ b/src/test/resources/regressions/features/closures/closures-calldesc2.gobra @@ -33,6 +33,7 @@ func hof(ghost cs Calls, f func(ghost seq[int], int)int)(res int) { ghost ensures forall k int :: k > 0 && len(s) == k ==> res == s[k-1] + seqSum(s[:(k-1)]) +decreases len(s) pure func seqSum(s seq[int]) (res int) { return len(s) == 0 ? 0 : (s[len(s)-1] + seqSum(s[:(len(s)-1)])) } diff --git a/src/test/resources/regressions/features/closures/closures-calldesc4-map.gobra b/src/test/resources/regressions/features/closures/closures-calldesc4-map.gobra index ebfe9f7f8..53c6d6e88 100644 --- a/src/test/resources/regressions/features/closures/closures-calldesc4-map.gobra +++ b/src/test/resources/regressions/features/closures/closures-calldesc4-map.gobra @@ -112,6 +112,7 @@ func test2() { ghost ensures forall k int :: k > 0 && len(s) == k ==> res == s[k-1] + seqSum(s[:(k-1)]) +decreases len(s) pure func seqSum(s seq[int]) (res int) { return len(s) == 0 ? 0 : (s[len(s)-1] + seqSum(s[:(len(s)-1)])) } diff --git a/src/test/resources/regressions/issues/000651.gobra b/src/test/resources/regressions/issues/000651.gobra new file mode 100644 index 000000000..d199f9546 --- /dev/null +++ b/src/test/resources/regressions/issues/000651.gobra @@ -0,0 +1,25 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package test + +type A adt { + A_ { + a uint + b set[int] + c bool + d bool + e seq[int] + } +} + +ghost +decreases +pure func f(x A) A { + return A_ { + a: x.a, + b: x.b, + c: x.c, + d: x.d, + e: x.e} +} \ No newline at end of file diff --git a/src/test/resources/regressions/issues/000655.gobra b/src/test/resources/regressions/issues/000655.gobra new file mode 100644 index 000000000..fcafa8991 --- /dev/null +++ b/src/test/resources/regressions/issues/000655.gobra @@ -0,0 +1,16 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package test + +// ##(-I ./000655/) +import "pkg" + +ghost +pure func foo(x pkg.List) bool { + return match x { + case pkg.Nil{}: true + case pkg.Cons{?head, pkg.Nil{}}: true + case _: false + } +} \ No newline at end of file diff --git a/src/test/resources/regressions/issues/000655/pkg/f.gobra b/src/test/resources/regressions/issues/000655/pkg/f.gobra new file mode 100644 index 000000000..2252d81b9 --- /dev/null +++ b/src/test/resources/regressions/issues/000655/pkg/f.gobra @@ -0,0 +1,14 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package pkg + +type List adt { + Cons { + head int + tail List + } + + Nil {} +} + diff --git a/src/test/resources/regressions/issues/000659.gobra b/src/test/resources/regressions/issues/000659.gobra new file mode 100644 index 000000000..7c6ecb2d9 --- /dev/null +++ b/src/test/resources/regressions/issues/000659.gobra @@ -0,0 +1,33 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue659 + +type Node struct { + ok bool +} + +pred (s *Set)mem(){ + acc(s) && + acc(s.nodes) && + forall i int:: i in domain(s.nodes) ==> acc(s.nodes[i]) +} + +type Set struct { + nodes map[int]*Node +} + +requires s.mem() +requires acc(n) +requires !(k in unfolding s.mem() in domain(s.nodes)) +func (s *Set) add2(n *Node, k int){ + unfold s.mem() + _,ok := s.nodes[0]; + if ok { + s.nodes[k] = n + fold s.mem() + //:: ExpectedOutput(assert_error:assertion_error) + assert false // should fail + return + } +} diff --git a/src/test/scala/viper/gobra/DetailedBenchmarkTests.scala b/src/test/scala/viper/gobra/DetailedBenchmarkTests.scala index 1e2ea620f..09c9cdb6b 100644 --- a/src/test/scala/viper/gobra/DetailedBenchmarkTests.scala +++ b/src/test/scala/viper/gobra/DetailedBenchmarkTests.scala @@ -142,7 +142,7 @@ class DetailedBenchmarkTests extends BenchmarkTests { val c = config.get assert(c.packageInfoInputMap.size == 1) val pkgInfo = c.packageInfoInputMap.keys.head - Right(Translator.translate(program, pkgInfo)(c)) + Translator.translate(program, pkgInfo)(c) }) private val verifying = NextStep("Viper verification", encoding, (viperTask: BackendVerifier.Task) => { diff --git a/viperserver b/viperserver index 2091da1b6..7b13e90a3 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit 2091da1b66e0ede0692493ccb49f08d619622586 +Subproject commit 7b13e90a37cc2e881f986fc2adbb0ff20c0f34e8