diff --git a/README.md b/README.md index c0c6760ae..2d7f4ce32 100644 --- a/README.md +++ b/README.md @@ -45,6 +45,28 @@ More information about the available options in Gobra can be found by running `r ### Running the Tests In the `gobra` directory, run the command `sbt test`. +### Debugging +By default, Gobra runs in sbt on a forked JVM. This means that simply attaching a debugger to sbt will not work. There +are two workarounds: + +- Run Gobra in a non-forked JVM by first running `set fork := false` in sbt. This will allow you to attach a debugger to + sbt normally. However, for unknown reasons, this causes issues with class resolution in the Viper backend, so actually + only the parsing can really be debugged. +- Attach the debugger to the forked JVM. + - Create a debug configuration in IntelliJ and specify to `Attach to remote JVM`, set `localhost` as host, and + a port (e.g. 5005). + - Run `set javaOptions += "-agentlib:jdwp=transport=dt_socket,server=y,suspend=y,address=5005"` + in sbt (use any port you like, just make sure to use the same one in the debugger). Now, the forked JVM can be + debugged instead of the sbt JVM. This requires starting the debugger again every time a new VM is created, + e.g. for every `run`. +- Let the debugger listen to the forked JVM. + - Create a debug configuration in IntelliJ and specify to `Listen to remote JVM`, enable auto restart, set + `localhost` as host, and a port (e.g. 5005). + - Run `set javaOptions += "-agentlib:jdwp=transport=dt_socket,server=n,address=localhost:5005,suspend=y"` in sbt. + Thanks to auto restart, the debugger keeps listening even when the JVM is restarted, e.g. for every `run`. + Note however that the debugger must be running/listening as otherwise the JVM will emit a connection + refused error. + ## Licensing Most Gobra sources are licensed under the Mozilla Public License Version 2.0. The [LICENSE](./LICENSE) lists the exceptions to this rule. 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/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala index 53692e770..ed4ca4f49 100644 --- a/src/main/scala/viper/gobra/backend/ViperBackends.scala +++ b/src/main/scala/viper/gobra/backend/ViperBackends.scala @@ -6,7 +6,7 @@ package viper.gobra.backend -import viper.gobra.frontend.Config +import viper.gobra.frontend.{Config, MCE} import viper.gobra.util.GobraExecutionContext import viper.server.ViperConfig import viper.server.core.ViperCoreServer @@ -27,9 +27,12 @@ object ViperBackends { if (config.conditionalizePermissions) { options ++= Vector("--conditionalizePermissions") } - if (!config.disableMoreCompleteExhale) { - options ++= Vector("--enableMoreCompleteExhale") + val mceSiliconOpt = config.mceMode match { + case MCE.Disabled => "0" + case MCE.Enabled => "1" + case MCE.OnDemand => "2" } + options ++= Vector(s"--exhaleMode=$mceSiliconOpt") if (config.assumeInjectivityOnInhale) { options ++= Vector("--assumeInjectivityOnInhale") } @@ -78,7 +81,7 @@ object ViperBackends { /** returns an existing ViperCoreServer instance or otherwise creates a new one */ protected def getOrCreateServer(config: Config)(executionContext: GobraExecutionContext): ViperCoreServer = { server.getOrElse({ - var serverConfig = List("--logLevel", config.logLevel.levelStr) + var serverConfig = List("--disablePlugins", "--logLevel", config.logLevel.levelStr) if(config.cacheFile.isDefined) { serverConfig = serverConfig.appendedAll(List("--cacheFile", config.cacheFile.get.toString)) } @@ -100,9 +103,12 @@ object ViperBackends { var options: Vector[String] = Vector.empty options ++= Vector("--logLevel", "ERROR") options ++= Vector("--disableCatchingExceptions") - if (!config.disableMoreCompleteExhale) { - options ++= Vector("--enableMoreCompleteExhale") + val mceSiliconOpt = config.mceMode match { + case MCE.Disabled => "0" + case MCE.Enabled => "1" + case MCE.OnDemand => "2" } + options ++= Vector(s"--exhaleMode=$mceSiliconOpt") if (config.assumeInjectivityOnInhale) { options ++= Vector("--assumeInjectivityOnInhale") } diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index e39e461fd..5dae8c252 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -65,13 +65,23 @@ object ConfigDefaults { lazy val DefaultAssumeInjectivityOnInhale: Boolean = true lazy val DefaultParallelizeBranches: Boolean = false lazy val DefaultConditionalizePermissions: Boolean = false - lazy val DefaultDisableMoreCompleteExhale: Boolean = false + lazy val DefaultMCEMode: MCE.Mode = MCE.Enabled lazy val DefaultEnableLazyImports: Boolean = false lazy val DefaultNoVerify: Boolean = false lazy val DefaultNoStreamErrors: Boolean = false lazy val DefaultParseAndTypeCheckMode: TaskManagerMode = TaskManagerMode.Parallel } +// More-complete exhale modes +object MCE { + sealed trait Mode + object Disabled extends Mode + // When running in `OnDemand`, mce will only be enabled when silicon retries a query. + // More information can be found in https://github.com/viperproject/silicon/pull/682. + object OnDemand extends Mode + object Enabled extends Mode +} + case class Config( gobraDirectory: Path = ConfigDefaults.DefaultGobraDirectory, // Used as an identifier of a verification task, ideally it shouldn't change between verifications @@ -117,7 +127,7 @@ case class Config( // branches will be verified in parallel parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches, conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions, - disableMoreCompleteExhale: Boolean = ConfigDefaults.DefaultDisableMoreCompleteExhale, + mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode, enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors, @@ -164,7 +174,7 @@ case class Config( assumeInjectivityOnInhale = assumeInjectivityOnInhale || other.assumeInjectivityOnInhale, parallelizeBranches = parallelizeBranches, conditionalizePermissions = conditionalizePermissions, - disableMoreCompleteExhale = disableMoreCompleteExhale, + mceMode = mceMode, enableLazyImports = enableLazyImports || other.enableLazyImports, noVerify = noVerify || other.noVerify, noStreamErrors = noStreamErrors || other.noStreamErrors, @@ -215,7 +225,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector assumeInjectivityOnInhale: Boolean = ConfigDefaults.DefaultAssumeInjectivityOnInhale, parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches, conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions, - disableMoreCompleteExhale: Boolean = ConfigDefaults.DefaultDisableMoreCompleteExhale, + mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode, enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors, @@ -270,7 +280,7 @@ trait RawConfig { assumeInjectivityOnInhale = baseConfig.assumeInjectivityOnInhale, parallelizeBranches = baseConfig.parallelizeBranches, conditionalizePermissions = baseConfig.conditionalizePermissions, - disableMoreCompleteExhale = baseConfig.disableMoreCompleteExhale, + mceMode = baseConfig.mceMode, enableLazyImports = baseConfig.enableLazyImports, noVerify = baseConfig.noVerify, noStreamErrors = baseConfig.noStreamErrors, @@ -618,12 +628,23 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals short = 'c', ) - val disableMoreCompleteExhale: ScallopOption[Boolean] = opt[Boolean]( - name = "disableMoreCompleteExhale", - descr = "Disables the flag --enableMoreCompleteExhale passed by default to Silicon", - default = Some(ConfigDefaults.DefaultDisableMoreCompleteExhale), - noshort = true, - ) + val mceMode: ScallopOption[MCE.Mode] = { + val on = "on" + val off = "off" + val od = "od" + choice( + choices = Seq("on", "off", "od"), + name = "mceMode", + descr = s"Specifies if silicon should be run with more complete exhale enabled ($on), disabled ($off), or enabled on demand ($od).", + default = Some(on), + noshort = true + ).map{ + case `on` => MCE.Enabled + case `off` => MCE.Disabled + case `od` => MCE.OnDemand + case s => Violation.violation(s"Unexpected mode for more complete exhale: $s") + } + } val enableLazyImports: ScallopOption[Boolean] = opt[Boolean]( name = Config.enableLazyImportOptionName, @@ -705,11 +726,11 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals } } - // `disableMoreCompleteExhale` can only be enabled when using a silicon-based backend + // `mceMode` can only be provided when using a silicon-based backend addValidation { - val disableMoreCompleteExh = disableMoreCompleteExhale.toOption.contains(true) - if (disableMoreCompleteExh && !isSiliconBasedBackend) { - Left("The flag --disableMoreCompleteExhale can only be used with Silicon and ViperServer with Silicon") + val mceModeSupplied = mceMode.isSupplied + if (mceModeSupplied && !isSiliconBasedBackend) { + Left("The flag --mceMode can only be used with Silicon or ViperServer with Silicon") } else { Right(()) } @@ -801,7 +822,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals assumeInjectivityOnInhale = assumeInjectivityOnInhale(), parallelizeBranches = parallelizeBranches(), conditionalizePermissions = conditionalizePermissions(), - disableMoreCompleteExhale = disableMoreCompleteExhale(), + mceMode = mceMode(), enableLazyImports = enableLazyImports(), noVerify = noVerify(), noStreamErrors = noStreamErrors(), diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index 96a56fdc4..d62ab7029 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -1838,7 +1838,7 @@ object Desugar extends LazyLogging { } yield in.Seqn(Vector(dPre, exprAss, clauseBody))(src) case n: POutline => - val name = s"${rootName(n, info)}$$${nm.relativeId(n, info)}" + val name = s"${rootName(n, info)}$$${nm.relativeIdEnclosingFuncOrMethodDecl(n, info)}" val pres = (n.spec.pres ++ n.spec.preserves) map preconditionD(ctx, info) val posts = (n.spec.preserves ++ n.spec.posts) map postconditionD(ctx, info) val terminationMeasures = sequence(n.spec.terminationMeasures map terminationMeasureD(ctx, info)).res @@ -3768,7 +3768,7 @@ object Desugar extends LazyLogging { 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) @@ -3840,6 +3840,13 @@ object Desugar extends LazyLogging { case decl: PMethodSig => idName(decl.id, context) case decl: PMPredicateSig => idName(decl.id, context) case decl: PDomainFunction => idName(decl.id, context) + case decl: PClosureDecl => + // closure declarations do not have an associated name and may be arbitrarily nested. + // to simplify, we just return the enclosing function or method's name + info.enclosingFunctionOrMethod(decl) match { + case Some(d) => idName(d.id, context) + case None => violation(s"Could not find a function or method declaration enclosing the closure declaration.") + } case _ => ??? // axiom and method-implementation-proof } } @@ -4884,7 +4891,7 @@ object Desugar extends LazyLogging { * The id is of the form 'L$$' where a is the difference of the lines * of the node with the code root and b is the difference of the columns * of the node with the code root. - * If a differce is negative, the '-' character is replaced with '_'. + * If the difference is negative, the '-' character is replaced with '_'. * * @param node the node we are interested in * @param info type info to get position information @@ -4897,6 +4904,25 @@ object Desugar extends LazyLogging { ("L$" + (lpos.line - rpos.line) + "$" + (lpos.column - rpos.column)).replace("-", "_") } + /** + * Returns an id for a node with respect to its enclosing function or method declaration. + * The id is of the form 'L$$' where a is the difference of the lines + * of the node with the enclosing declaration and b is the difference of the columns + * of the node with the enclosing declaration. + * If the difference is negative, the '-' character is replaced with '_'. + * + * @param node the node we are interested in + * @param info type info to get position information + * @return string + */ + def relativeIdEnclosingFuncOrMethodDecl(node: PNode, info: TypeInfo) : String = { + val pom = info.getTypeInfo.tree.originalRoot.positions + val lpos = pom.positions.getStart(node).get + val enclosingMember = info.enclosingFunctionOrMethod(node).get + val rpos = pom.positions.getStart(enclosingMember).get + ("L$" + (lpos.line - rpos.line) + "$" + (lpos.column - rpos.column)).replace("-", "_") + } + /** returns the relativeId with the CONTINUE_LABEL_SUFFIX appended */ def continueLabel(loop: PGeneralForStmt, info: TypeInfo) : String = relativeId(loop, info) + CONTINUE_LABEL_SUFFIX 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/property/Convertibility.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala index 84430465e..6352cbd6b 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala @@ -20,6 +20,8 @@ trait Convertibility extends BaseProperty { this: TypeInfoImpl => case (left, right) if assignableTo(left, right) => true case (IntT(_), Float32T) => true case (IntT(_), Float64T) => true + case (Float32T, IntT(_)) => true + case (Float64T, IntT(_)) => true case (IntT(_), IntT(_)) => true case (SliceT(IntT(config.typeBounds.Byte)), StringT) => true case (StringT, SliceT(IntT(config.typeBounds.Byte))) => true diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeMerging.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeMerging.scala index 9ffd3e6cf..9aa0ffe51 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeMerging.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/TypeMerging.scala @@ -6,6 +6,7 @@ package viper.gobra.frontend.info.implementation.property +import viper.gobra.ast.internal.{Float32T, Float64T} import viper.gobra.frontend.info.base.Type.{AdtClauseT, AdtT, ArrayT, ChannelT, GhostSliceT, IntT, InternalSingleMulti, InternalTupleT, MapT, MultisetT, PermissionT, PointerT, SequenceT, SetT, Single, SliceT, Type} import viper.gobra.frontend.info.implementation.TypeInfoImpl @@ -23,6 +24,10 @@ trait TypeMerging extends BaseProperty { this: TypeInfoImpl => (lst, rst) match { case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[IntT] => Some(a) case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[IntT] => Some(b) + case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[Float64T] => Some(a) + case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[Float64T] => Some(b) + case (a, UNTYPED_INT_CONST) if underlyingType(a).isInstanceOf[Float32T] => Some(a) + case (UNTYPED_INT_CONST, b) if underlyingType(b).isInstanceOf[Float32T] => Some(b) case (IntT(_), PermissionT) => Some(PermissionT) case (PermissionT, IntT(_)) => Some(PermissionT) case (SequenceT(l), SequenceT(r)) => typeMerge(l,r) map SequenceT 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/translator/encodings/FloatEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/FloatEncoding.scala index 6ee174e5c..76ee45196 100644 --- a/src/main/scala/viper/gobra/translator/encodings/FloatEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/FloatEncoding.scala @@ -78,6 +78,10 @@ class FloatEncoding extends LeafTypeEncoding { for { e <- goE(expr) } yield withSrc(vpr.FuncApp(fromIntTo32, Seq(e)), conv) case conv@in.Conversion(in.Float64T(_), expr :: ctx.Int()) => for { e <- goE(expr) } yield withSrc(vpr.FuncApp(fromIntTo64, Seq(e)), conv) + case conv@in.Conversion(in.IntT(_, _), expr :: ctx.Float32()) => + for { e <- goE(expr) } yield withSrc(vpr.FuncApp(from32ToInt, Seq(e)), conv) + case conv@in.Conversion(in.IntT(_, _), expr :: ctx.Float64()) => + for { e <- goE(expr) } yield withSrc(vpr.FuncApp(from64ToInt, Seq(e)), conv) } } @@ -95,6 +99,8 @@ class FloatEncoding extends LeafTypeEncoding { addMemberFn(mulFloat64) addMemberFn(divFloat64) addMemberFn(fromIntTo64) + addMemberFn(from32ToInt) + addMemberFn(from64ToInt) } } private var isUsed32: Boolean = false @@ -267,4 +273,36 @@ class FloatEncoding extends LeafTypeEncoding { body = None )() } + + /** + * Generates + * function from32ToInt(l: Int): Int + */ + private lazy val from32ToInt = { + val arg = vpr.LocalVarDecl("n", floatType32)() + vpr.Function( + name = "from32ToInt", + formalArgs = Seq(arg), + typ = vpr.Int, + pres = Seq(), + posts = Seq(), + body = None + )() + } + + /** + * Generates + * function from64ToInt(l: Int): Int + */ + private lazy val from64ToInt = { + val arg = vpr.LocalVarDecl("n", floatType64)() + vpr.Function( + name = "from64ToInt", + formalArgs = Seq(arg), + typ = vpr.Int, + pres = Seq(), + posts = Seq(), + body = None + )() + } } \ No newline at end of file diff --git a/src/test/resources/regressions/examples/evaluation/binary_search_tree.gobra b/src/test/resources/regressions/examples/evaluation/binary_search_tree.gobra index 3f560953a..9ca21e1ba 100644 --- a/src/test/resources/regressions/examples/evaluation/binary_search_tree.gobra +++ b/src/test/resources/regressions/examples/evaluation/binary_search_tree.gobra @@ -29,9 +29,9 @@ pred (n *node) tree() { } ghost -requires n.tree() +requires acc(n.tree(), _) pure func (n *node) sorted(lowerBound, upperBound option[int]) bool { - return unfolding n.tree() in (lowerBound != none[int] ==> get(lowerBound) < n.value) && + return unfolding acc(n.tree(), _) in (lowerBound != none[int] ==> get(lowerBound) < n.value) && (upperBound != none[int] ==> n.value < get(upperBound)) && (n.left != nil ==> n.left.sorted(lowerBound, some(n.value))) && (n.right != nil ==> n.right.sorted(some(n.value), upperBound)) @@ -59,19 +59,19 @@ func (n *node) convert(oldLowerBound, oldUpperBound, newLowerBound, newUpperBoun } ghost -requires t.tree() +requires acc(t.tree(), _) ensures forall i int :: (0 <= i && i + 1 < len(res) ==> res[i] < res[i + 1]) // ordered pure func (t *Tree) sortedValues() (res seq[int]) { - return unfolding t.tree() in (t.root == nil) ? seq[int] { } : t.root.sortedValues(none[int], none[int]) + return unfolding acc(t.tree(), _) in (t.root == nil) ? seq[int] { } : t.root.sortedValues(none[int], none[int]) } ghost -requires n.tree() && n.sorted(lowerBound, upperBound) +requires acc(n.tree(), _) && n.sorted(lowerBound, upperBound) ensures n.sorted(lowerBound, upperBound) ensures forall i int :: (0 <= i && i < len(res) ==> ((lowerBound != none[int] ==> res[i] > get(lowerBound)) && (upperBound != none[int] ==> res[i] < get(upperBound)))) ensures forall i int :: (0 <= i && i + 1 < len(res) ==> res[i] < res[i + 1]) // ordered pure func (n *node) sortedValues(lowerBound, upperBound option[int]) (res seq[int]) { - return unfolding n.tree() in (n.left == nil ? seq[int]{ } : n.left.sortedValues(lowerBound, some(n.value))) ++ seq[int]{ n.value } ++ (n.right == nil ? seq[int]{ } : n.right.sortedValues(some(n.value), upperBound)) + return unfolding acc(n.tree(), _) in (n.left == nil ? seq[int]{ } : n.left.sortedValues(lowerBound, some(n.value))) ++ seq[int]{ n.value } ++ (n.right == nil ? seq[int]{ } : n.right.sortedValues(some(n.value), upperBound)) } ensures t.tree() && t.IsEmpty() diff --git a/src/test/resources/regressions/examples/evaluation/impl_errors/binary_search_tree.gobra b/src/test/resources/regressions/examples/evaluation/impl_errors/binary_search_tree.gobra index d8789591a..429dcb1a6 100644 --- a/src/test/resources/regressions/examples/evaluation/impl_errors/binary_search_tree.gobra +++ b/src/test/resources/regressions/examples/evaluation/impl_errors/binary_search_tree.gobra @@ -29,9 +29,9 @@ pred (n *node) tree() { } ghost -requires n.tree() +requires acc(n.tree(), _) pure func (n *node) sorted(lowerBound, upperBound option[int]) bool { - return unfolding n.tree() in (lowerBound != none[int] ==> get(lowerBound) < n.value) && + return unfolding acc(n.tree(), _) in (lowerBound != none[int] ==> get(lowerBound) < n.value) && (upperBound != none[int] ==> n.value < get(upperBound)) && (n.left != nil ==> n.left.sorted(lowerBound, some(n.value))) && (n.right != nil ==> n.right.sorted(some(n.value), upperBound)) @@ -59,19 +59,19 @@ func (n *node) convert(oldLowerBound, oldUpperBound, newLowerBound, newUpperBoun } ghost -requires t.tree() +requires acc(t.tree(), _) ensures forall i int :: (0 <= i && i + 1 < len(res) ==> res[i] < res[i + 1]) // ordered pure func (t *Tree) sortedValues() (res seq[int]) { - return unfolding t.tree() in (t.root == nil) ? seq[int] { } : t.root.sortedValues(none[int], none[int]) + return unfolding acc(t.tree(), _) in (t.root == nil) ? seq[int] { } : t.root.sortedValues(none[int], none[int]) } ghost -requires n.tree() && n.sorted(lowerBound, upperBound) +requires acc(n.tree(), _) && n.sorted(lowerBound, upperBound) ensures n.sorted(lowerBound, upperBound) ensures forall i int :: (0 <= i && i < len(res) ==> ((lowerBound != none[int] ==> res[i] > get(lowerBound)) && (upperBound != none[int] ==> res[i] < get(upperBound)))) ensures forall i int :: (0 <= i && i + 1 < len(res) ==> res[i] < res[i + 1]) // ordered pure func (n *node) sortedValues(lowerBound, upperBound option[int]) (res seq[int]) { - return unfolding n.tree() in (n.left == nil ? seq[int]{ } : n.left.sortedValues(lowerBound, some(n.value))) ++ seq[int]{ n.value } ++ (n.right == nil ? seq[int]{ } : n.right.sortedValues(some(n.value), upperBound)) + return unfolding acc(n.tree(), _) in (n.left == nil ? seq[int]{ } : n.left.sortedValues(lowerBound, some(n.value))) ++ seq[int]{ n.value } ++ (n.right == nil ? seq[int]{ } : n.right.sortedValues(some(n.value), upperBound)) } ensures t.tree() && t.IsEmpty() @@ -81,16 +81,16 @@ func NewTree() (t *Tree) { return t } -requires t.tree() -ensures res == unfolding t.tree() in t.root == nil +requires acc(t.tree(), _) +ensures res == unfolding acc(t.tree(), _) in t.root == nil pure func (t *Tree) IsEmpty() (res bool) { - return unfolding t.tree() in t.root == nil + return unfolding acc(t.tree(), _) in t.root == nil } requires dividend > 0 requires acc(t.tree(), 1/dividend) ensures acc(t.tree(), 1/dividend) -ensures res == t.pureContains(value, dividend) +ensures res == t.pureContains(value) func (t *Tree) Contains(value, dividend int) (res bool) { unfold acc(t.tree(), 1/dividend) if (t.root == nil) { @@ -103,9 +103,9 @@ func (t *Tree) Contains(value, dividend int) (res bool) { } ghost -requires dividend > 0 && acc(t.tree(), 1/dividend) -pure func (t *Tree) pureContains(value, dividend int) bool { - return unfolding acc(t.tree(), 1/dividend) in t.root != nil && value in t.root.sortedValues(none[int], none[int]) +requires acc(t.tree(), _) +pure func (t *Tree) pureContains(value int) bool { + return unfolding acc(t.tree(), _) in t.root != nil && value in t.root.sortedValues(none[int], none[int]) } requires dividend > 0 @@ -300,11 +300,11 @@ func main() { ensures t.tree() func client0(value int) (t *Tree) { t = NewTree() - assert !t.pureContains(value, 2) + assert !t.pureContains(value) t.Insert(value) assert t.sortedValues() == seq[int]{ value } t.Delete(value) - assert !t.pureContains(value, 2) + assert !t.pureContains(value) return t } @@ -324,7 +324,7 @@ func client2(t *Tree, value int) { // insert a new value t.Insert(value) var newValues = t.sortedValues() - assert t.pureContains(value, 2) + assert t.pureContains(value) ghost if (value in oldValues) { assert oldValues == newValues } else { diff --git a/src/test/resources/regressions/examples/evaluation/spec_errors/binary_search_tree.gobra b/src/test/resources/regressions/examples/evaluation/spec_errors/binary_search_tree.gobra index 56215d656..69b64eba7 100644 --- a/src/test/resources/regressions/examples/evaluation/spec_errors/binary_search_tree.gobra +++ b/src/test/resources/regressions/examples/evaluation/spec_errors/binary_search_tree.gobra @@ -29,9 +29,9 @@ pred (n *node) tree() { } ghost -requires n.tree() +requires acc(n.tree(), _) pure func (n *node) sorted(lowerBound, upperBound option[int]) bool { - return unfolding n.tree() in (lowerBound != none[int] ==> get(lowerBound) < n.value) && + return unfolding acc(n.tree(), _) in (lowerBound != none[int] ==> get(lowerBound) < n.value) && (upperBound != none[int] ==> n.value < get(upperBound)) && (n.left != nil ==> n.left.sorted(lowerBound, some(n.value))) && (n.right != nil ==> n.right.sorted(some(n.value), upperBound)) @@ -59,19 +59,19 @@ func (n *node) convert(oldLowerBound, oldUpperBound, newLowerBound, newUpperBoun } ghost -requires t.tree() +requires acc(t.tree(), _) ensures forall i int :: (0 <= i && i + 1 < len(res) ==> res[i] < res[i + 1]) // ordered pure func (t *Tree) sortedValues() (res seq[int]) { - return unfolding t.tree() in (t.root == nil) ? seq[int] { } : t.root.sortedValues(none[int], none[int]) + return unfolding acc(t.tree(), _) in (t.root == nil) ? seq[int] { } : t.root.sortedValues(none[int], none[int]) } ghost -requires n.tree() && n.sorted(lowerBound, upperBound) +requires acc(n.tree(), _) && n.sorted(lowerBound, upperBound) ensures n.sorted(lowerBound, upperBound) ensures forall i int :: (0 <= i && i < len(res) ==> ((lowerBound != none[int] ==> res[i] > get(lowerBound)) && (upperBound != none[int] ==> res[i] < get(upperBound)))) ensures forall i int :: (0 <= i && i + 1 < len(res) ==> res[i] < res[i + 1]) // ordered pure func (n *node) sortedValues(lowerBound, upperBound option[int]) (res seq[int]) { - return unfolding n.tree() in (n.left == nil ? seq[int]{ } : n.left.sortedValues(lowerBound, some(n.value))) ++ seq[int]{ n.value } ++ (n.right == nil ? seq[int]{ } : n.right.sortedValues(some(n.value), upperBound)) + return unfolding acc(n.tree(), _) in (n.left == nil ? seq[int]{ } : n.left.sortedValues(lowerBound, some(n.value))) ++ seq[int]{ n.value } ++ (n.right == nil ? seq[int]{ } : n.right.sortedValues(some(n.value), upperBound)) } ensures t.tree() && t.IsEmpty() @@ -81,16 +81,16 @@ func NewTree() (t *Tree) { return t } -requires t.tree() -ensures res == unfolding t.tree() in t.root == nil +requires acc(t.tree(), _) +ensures res == unfolding acc(t.tree(), _) in t.root == nil pure func (t *Tree) IsEmpty() (res bool) { - return unfolding t.tree() in t.root == nil + return unfolding acc(t.tree(), _) in t.root == nil } requires dividend > 0 requires acc(t.tree(), 1/dividend) ensures acc(t.tree(), 1/dividend) -ensures res == t.pureContains(value, dividend) +ensures res == t.pureContains(value) func (t *Tree) Contains(value, dividend int) (res bool) { unfold acc(t.tree(), 1/dividend) if (t.root == nil) { @@ -103,9 +103,9 @@ func (t *Tree) Contains(value, dividend int) (res bool) { } ghost -requires dividend > 0 && acc(t.tree(), 1/dividend) -pure func (t *Tree) pureContains(value, dividend int) bool { - return unfolding acc(t.tree(), 1/dividend) in t.root != nil && value in t.root.sortedValues(none[int], none[int]) +requires acc(t.tree(), _) +pure func (t *Tree) pureContains(value int) bool { + return unfolding acc(t.tree(), _) in t.root != nil && value in t.root.sortedValues(none[int], none[int]) } requires dividend > 0 @@ -300,12 +300,12 @@ func main() { ensures t.tree() func client0(value int) (t *Tree) { t = NewTree() - assert !t.pureContains(value, 2) + assert !t.pureContains(value) t.Insert(value) //:: ExpectedOutput(assert_error:assertion_error) assert t.sortedValues() == seq[int]{ value } t.Delete(value) - assert !t.pureContains(value, 2) + assert !t.pureContains(value) return t } @@ -326,7 +326,7 @@ func client2(t *Tree, value int) { t.Insert(value) var newValues = t.sortedValues() //:: ExpectedOutput(assert_error:assertion_error) - assert t.pureContains(value, 2) + assert t.pureContains(value) ghost if (value in oldValues) { assert oldValues == newValues } else { diff --git a/src/test/resources/regressions/examples/tutorial-examples/predicate.gobra b/src/test/resources/regressions/examples/tutorial-examples/predicate.gobra index f474d9392..dabd3b5ae 100644 --- a/src/test/resources/regressions/examples/tutorial-examples/predicate.gobra +++ b/src/test/resources/regressions/examples/tutorial-examples/predicate.gobra @@ -36,10 +36,10 @@ pure func head(ptr *node) int { requires p > 0 requires acc(list(ptr), p) pure func (ptr *node) contains(value int, ghost p perm) bool { - return unfolding list(ptr) in ptr.value == value || (ptr.next != nil && ptr.next.contains(value, p)) + return unfolding acc(list(ptr), p) in ptr.value == value || (ptr.next != nil && ptr.next.contains(value, p)) } requires acc(list(ptr), _) pure func (ptr *node) contains2(value int) bool { - return unfolding list(ptr) in ptr.value == value || (ptr.next != nil && ptr.next.contains2(value)) + return unfolding acc(list(ptr), _) in ptr.value == value || (ptr.next != nil && ptr.next.contains2(value)) } \ No newline at end of file diff --git a/src/test/resources/regressions/features/outline/outline-simple2.gobra b/src/test/resources/regressions/features/outline/outline-simple2.gobra index d59d5b9d8..6e1049d5d 100644 --- a/src/test/resources/regressions/features/outline/outline-simple2.gobra +++ b/src/test/resources/regressions/features/outline/outline-simple2.gobra @@ -93,4 +93,16 @@ func test6() { //:: ExpectedOutput(assert_error:assertion_error) assert x == 11 -} \ No newline at end of file +} + +func test7() { + f := + ensures acc(y) && *y >= 5 + func fspec() (y *int) { + ensures acc(&x) && x >= 5 + outline ( + x@ := 10 + ) + return &x + } +} diff --git a/src/test/resources/regressions/issues/000416.gobra b/src/test/resources/regressions/issues/000416.gobra index 38af7b8b2..0926f5b8f 100644 --- a/src/test/resources/regressions/issues/000416.gobra +++ b/src/test/resources/regressions/issues/000416.gobra @@ -14,7 +14,8 @@ func main () { Area(&r) } -requires s != nil && s.mem() && s.Size() +requires s != nil && s.mem() +ensures s != nil && s.mem() func Area(s shape.Shape) (ret int) { return s.Area() } \ No newline at end of file diff --git a/src/test/resources/regressions/issues/000416/importedImplementationPkg/importedImplementationPkg.gobra b/src/test/resources/regressions/issues/000416/importedImplementationPkg/importedImplementationPkg.gobra index 8de3c38d1..ea795dfba 100644 --- a/src/test/resources/regressions/issues/000416/importedImplementationPkg/importedImplementationPkg.gobra +++ b/src/test/resources/regressions/issues/000416/importedImplementationPkg/importedImplementationPkg.gobra @@ -15,13 +15,13 @@ pred (r *Rect) mem() { acc(r, 1/2) } -requires acc(r, 1/2) +requires acc(r, _) pure func (r *Rect) Size() bool { - return r.width > 0 && r.height > 0 + return r.width >= 0 && r.height >= 0 } -requires acc(r, 1/2) && r.Size() -ensures acc(r, 1/2) && ret > 0 +requires acc(r, 1/2) +ensures acc(r, 1/2) func (r *Rect) Area() (ret int) { return r.width * r.height } diff --git a/src/test/resources/regressions/issues/000416/importedImplementationPkg/shape/shape.gobra b/src/test/resources/regressions/issues/000416/importedImplementationPkg/shape/shape.gobra index 02613017c..6a57d0a3c 100644 --- a/src/test/resources/regressions/issues/000416/importedImplementationPkg/shape/shape.gobra +++ b/src/test/resources/regressions/issues/000416/importedImplementationPkg/shape/shape.gobra @@ -9,7 +9,7 @@ type Shape interface { requires acc(mem(), 1/2) pure Size() bool - requires mem() && Size() - ensures ret > 0 + requires mem() + ensures mem() Area() (ret int) } \ No newline at end of file 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/viperserver b/viperserver index d5d38d628..ae6a1c153 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit d5d38d62825e8bf4448c55f589dd8c838f33dc96 +Subproject commit ae6a1c153152bdae0005850190b24f0212113474