Skip to content

Commit 035769d

Browse files
marcoeilersmarcoeilers
authored
Merge pull request #666 from viperproject/meilers_annotations
Annotations
2 parents 9208207 + 8c6b733 commit 035769d

13 files changed

Lines changed: 447 additions & 202 deletions

File tree

‎src/main/scala/viper/silver/ast/Ast.scala‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -371,6 +371,11 @@ case object NoInfo extends Info {
371371
override val isCached = false
372372
}
373373

374+
case class AnnotationInfo(values: Map[String, Seq[String]]) extends Info {
375+
override val isCached = false
376+
override val comment = Nil
377+
}
378+
374379
/** A simple `Info` that contains a list of comments. */
375380
case class SimpleInfo(comment: Seq[String]) extends Info {
376381
override val isCached = false

‎src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66

77
package viper.silver.ast.utility.rewriter
88

9-
import viper.silver.parser.PDomainFunction
9+
import viper.silver.parser.{PDomain, PDomainFunction, PField, PFunction, PMethod, PPredicate}
1010
import viper.silver.parser.Transformer.ParseTreeDuplicationError
1111
import viper.silver.ast.{AtomicType, BackendFuncApp, DomainFuncApp, ErrorTrafo, FuncApp, Info, Node, Position}
1212

@@ -49,9 +49,14 @@ trait Rewritable extends Product {
4949
case df: DomainFuncApp => secondArgList = Seq(df.pos, df.info, df.typ, df.domainName, df.errT)
5050
case ba: BackendFuncApp => secondArgList = Seq(ba.pos, ba.info, ba.typ, ba.interpretation, ba.errT)
5151
case no: Node => secondArgList = no.getMetadata
52-
case pa: PAxiom => secondArgList = Seq(pa.domainName) ++ Seq(pos.getOrElse(pa.pos))
52+
case pa: PAxiom => secondArgList = Seq(pa.domainName) ++ Seq(pos.getOrElse(pa.pos), pa.annotations)
5353
case pm: PMagicWandExp => firstArgList = Seq(children.head) ++ children.drop(2) ++ Seq(pos.getOrElse(pm.pos))
54-
case pd: PDomainFunction => secondArgList = Seq(pd.domainName) ++ Seq(pos.getOrElse(pd.pos))
54+
case pd: PDomainFunction => secondArgList = Seq(pd.domainName) ++ Seq(pos.getOrElse(pd.pos), pd.annotations)
55+
case pd: PDomain => secondArgList = Seq(pos.getOrElse(pd.pos), pd.annotations)
56+
case pm: PMethod => secondArgList = Seq(pos.getOrElse(pm.pos), pm.annotations)
57+
case pp: PPredicate => secondArgList = Seq(pos.getOrElse(pp.pos), pp.annotations)
58+
case pf: PFunction => secondArgList = Seq(pos.getOrElse(pf.pos), pf.annotations)
59+
case pf: PField => secondArgList = Seq(pos.getOrElse(pf.pos), pf.annotations)
5560
case pn: PNode => secondArgList = Seq(pos.getOrElse(pn.pos))
5661
case _ =>
5762
}

‎src/main/scala/viper/silver/parser/FastParser.scala‎

Lines changed: 41 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -510,7 +510,7 @@ class FastParser {
510510
}
511511

512512
if (body != method.body) {
513-
PMethod(method.idndef, method.formalArgs, method.formalReturns, method.pres, method.posts, body)(method.pos)
513+
PMethod(method.idndef, method.formalArgs, method.formalReturns, method.pres, method.posts, body)(method.pos, method.annotations)
514514
} else {
515515
method
516516
}
@@ -794,14 +794,23 @@ class FastParser {
794794

795795
// Note that `typedFapp` is before `"(" ~ exp ~ ")"` to ensure that the latter doesn't gobble up the brackets for the former
796796
// and then look like an `fapp` up untill the `: type` part, after which we need to backtrack all the way back (or error if cut)
797-
def atom(implicit ctx : P[_]) : P[PExp] = P(ParserExtension.newExpAtStart(ctx) | integer | booltrue | boolfalse | nul | old
797+
def atom(implicit ctx : P[_]) : P[PExp] = P(ParserExtension.newExpAtStart(ctx) | annotatedAtom
798+
| integer | booltrue | boolfalse | nul | old
798799
| result | unExp | typedFapp
799800
| "(" ~ exp ~ ")" | accessPred | inhaleExhale | perm | let | quant | forperm | unfolding | applying
800801
| setTypedEmpty | explicitSetNonEmpty | multiSetTypedEmpty | explicitMultisetNonEmpty | seqTypedEmpty
801802
| size | explicitSeqNonEmpty | seqRange
802803
| mapTypedEmpty | explicitMapNonEmpty | mapDomain | mapRange
803804
| fapp | idnuse | ParserExtension.newExpAtEnd(ctx))
804805

806+
def stringLiteral[$: P]: P[String] = P("\"" ~ CharsWhile(_ != '\"').! ~ "\"")
807+
808+
def annotation[$: P]: P[(String, Seq[String])] = P("@" ~~ annotationIdentifier ~ parens(stringLiteral.rep(sep = ",")))
809+
810+
def annotatedAtom[$: P]: P[PExp] = FP(annotation ~ atom).map{
811+
case (pos, (key, value, exp)) => PAnnotatedExp(exp, (key, value))(pos)
812+
}
813+
805814
def result[$: P]: P[PResultLit] = FP(keyword("result")).map { case (pos, _) => PResultLit()(pos) }
806815

807816
def unExp[$: P]: P[PUnExp] = FP(CharIn("\\-\\!").! ~ suffixExpr).map { case (pos, (a, b)) => PUnExp(a, b)(pos) }
@@ -818,6 +827,8 @@ class FastParser {
818827

819828
def identifier[$: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX
820829

830+
def annotationIdentifier[$: P]: P[String] = (CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).!
831+
821832
def ident[$: P]: P[String] = identifier.!.filter(a => !keywords.contains(a)).opaque("invalid identifier (could be a keyword)")
822833

823834
def idnuse[$: P]: P[PIdnUse] = FP(ident).map { case (pos, id) => PIdnUse(id)(pos) }
@@ -1094,11 +1105,16 @@ class FastParser {
10941105
case (pos, (func, args, typeGiven)) => PCall(func, args, Some(typeGiven))(pos)
10951106
}
10961107

1097-
def stmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | macroassign | fieldassign | localassign | fold | unfold | exhale | assertP |
1108+
def stmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | annotatedStmt |
1109+
macroassign | fieldassign | localassign | fold | unfold | exhale | assertP |
10981110
inhale | assume | ifthnels | whle | varDecl | defineDecl | newstmt |
10991111
methodCall | goto | lbl | packageWand | applyWand | macroref | block |
11001112
quasihavoc | quasihavocall | ParserExtension.newStmtAtEnd(ctx))
11011113

1114+
def annotatedStmt(implicit ctx : P[_]): P[PStmt] = (FP(annotation ~ stmt).map{
1115+
case (pos, (key, value, pStmt)) => PAnnotatedStmt(pStmt, (key, value))(pos)
1116+
})
1117+
11021118
def nodefinestmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | fieldassign | localassign | fold | unfold | exhale | assertP |
11031119
inhale | assume | ifthnels | whle | varDecl | newstmt |
11041120
methodCall | goto | lbl | packageWand | applyWand | macroref | block |
@@ -1210,7 +1226,8 @@ class FastParser {
12101226

12111227
def applying[$: P]: P[PExp] = FP(keyword("applying") ~/ "(" ~ magicWandExp ~ ")" ~ "in" ~ exp).map { case (pos, (a, b)) => PApplying(a, b)(pos) }
12121228

1213-
def programDecl(implicit ctx : P[_]) : P[PProgram] = P(FP((ParserExtension.newDeclAtStart(ctx) | preambleImport | defineDecl | domainDecl | fieldDecl | functionDecl | predicateDecl | methodDecl | ParserExtension.newDeclAtEnd(ctx)).rep).map {
1229+
def programDecl(implicit ctx : P[_]) : P[PProgram] =
1230+
P(FP((ParserExtension.newDeclAtStart(ctx) | preambleImport | defineDecl | fieldDecl | methodDecl | domainDecl | functionDecl | predicateDecl | ParserExtension.newDeclAtEnd(ctx)).rep).map {
12141231
case (pos, decls) => {
12151232
PProgram(
12161233
decls.collect { case i: PImport => i }, // Imports
@@ -1235,26 +1252,26 @@ class FastParser {
12351252

12361253
def anyString[$: P]: P[String] = P(CharPred(c => c !='\"').rep(1).!)
12371254

1238-
def domainDecl[$: P]: P[PDomain] = FP("domain" ~/ idndef ~ typeParams ~ ("interpretation" ~ parens((ident ~ ":" ~ quoted(anyString.!)).rep(sep = ","))).? ~ "{" ~ (domainFunctionDecl | axiomDecl).rep ~
1255+
def domainDecl[$: P]: P[PDomain] = FP(annotation.rep(0) ~ "domain" ~/ idndef ~ typeParams ~ ("interpretation" ~ parens((ident ~ ":" ~ quoted(anyString.!)).rep(sep = ","))).? ~ "{" ~ (domainFunctionDecl | axiomDecl).rep ~
12391256
"}").map {
1240-
case (pos, (name, typparams, interpretations, members)) =>
1257+
case (pos, (anns, name, typparams, interpretations, members)) =>
12411258
val funcs = members collect { case m: PDomainFunction1 => m }
12421259
val axioms = members collect { case m: PAxiom1 => m }
12431260
PDomain(
12441261
name,
12451262
typparams,
1246-
funcs map (f => PDomainFunction(f.idndef, f.formalArgs, f.typ, f.unique, f.interpretation)(PIdnUse(name.name)(name.pos))(f.pos)),
1247-
axioms map (a => PAxiom(a.idndef, a.exp)(PIdnUse(name.name)(name.pos))(a.pos)),
1248-
interpretations.map(i => i.toMap))(pos)
1263+
funcs map (f => PDomainFunction(f.idndef, f.formalArgs, f.typ, f.unique, f.interpretation)(PIdnUse(name.name)(name.pos))(f.pos, f.annotations)),
1264+
axioms map (a => PAxiom(a.idndef, a.exp)(PIdnUse(name.name)(name.pos))(a.pos, a.annotations)),
1265+
interpretations.map(i => i.toMap))(pos, anns)
12491266
}
12501267

12511268
def domainTypeVarDecl[$: P]: P[PTypeVarDecl] = FP(idndef).map{ case (pos, i) => PTypeVarDecl(i)(pos) }
12521269

12531270
def typeParams[$: P]: P[Seq[PTypeVarDecl]] = P(("[" ~ domainTypeVarDecl.rep(sep = ",") ~ "]").?).map(_.getOrElse(Nil))
12541271

1255-
def domainFunctionDecl[$: P]: P[PDomainFunction1] = FP("unique".!.? ~ domainFunctionSignature ~ ("interpretation" ~ quoted(anyString.!)).? ~~~ ";".lw.?).map {
1256-
case (pos, (unique, fdecl, interpretation)) => fdecl match {
1257-
case (name, formalArgs, t) => PDomainFunction1(name, formalArgs, t, unique.isDefined, interpretation)(pos)
1272+
def domainFunctionDecl[$: P]: P[PDomainFunction1] = FP(annotation.rep(0) ~ "unique".!.? ~ domainFunctionSignature ~ ("interpretation" ~ quoted(anyString.!)).? ~~~ ";".lw.?).map {
1273+
case (pos, (anns, unique, fdecl, interpretation)) => fdecl match {
1274+
case (name, formalArgs, t) => PDomainFunction1(name, formalArgs, t, unique.isDefined, interpretation)(pos, anns)
12581275
}
12591276
}
12601277

@@ -1268,15 +1285,15 @@ class FastParser {
12681285

12691286
def formalArgList[$: P]: P[Seq[PFormalArgDecl]] = P(formalArg.rep(sep = ","))
12701287

1271-
def axiomDecl[$: P]: P[PAxiom1] = FP(keyword("axiom") ~ idndef.? ~ "{" ~ exp ~ "}" ~~~ ";".lw.?).map { case (pos, (a, b)) => PAxiom1(a, b)(pos) }
1288+
def axiomDecl[$: P]: P[PAxiom1] = FP(annotation.rep(0) ~ keyword("axiom") ~ idndef.? ~ "{" ~ exp ~ "}" ~~~ ";".lw.?).map { case (pos, (anns, a, b)) => PAxiom1(a, b)(pos, anns) }
12721289

1273-
def fieldDecl[$: P]: P[PField] = FP(keyword("field") ~/ idndef ~ ":" ~ typ ~~~ ";".lw.?).map {
1274-
case (pos, (a, b)) => PField(a, b)(pos)
1290+
def fieldDecl[$: P]: P[PField] = FP(annotation.rep(0) ~ keyword("field") ~/ idndef ~ ":" ~ typ ~~~ ";".lw.?).map {
1291+
case (pos, (anns, a, b)) => PField(a, b)(pos, anns)
12751292
}
12761293

1277-
def functionDecl[$: P]: P[PFunction] = FP("function" ~/ idndef ~ "(" ~ formalArgList ~ ")" ~ ":" ~ typ ~~~ pre.lw.rep ~~~
1278-
post.lw.rep ~~~ ("{" ~ exp ~ "}").lw.?).map({ case (pos, (a, b, c, d, e, f)) =>
1279-
PFunction(a, b, c, d, e, f)(pos)
1294+
def functionDecl[$: P]: P[PFunction] = FP(annotation.rep(0) ~ "function" ~/ idndef ~ "(" ~ formalArgList ~ ")" ~ ":" ~ typ ~~~ pre.lw.rep ~~~
1295+
post.lw.rep ~~~ ("{" ~ exp ~ "}").lw.?).map({ case (pos, (anns, a, b, c, d, e, f)) =>
1296+
PFunction(a, b, c, d, e, f)(pos, anns)
12801297
})
12811298

12821299

@@ -1286,14 +1303,14 @@ class FastParser {
12861303

12871304
def decCl[$: P]: P[Seq[PExp]] = P(exp.rep(sep = ","))
12881305

1289-
def predicateDecl[$: P]: P[PPredicate] = FP(keyword("predicate") ~/ idndef ~ "(" ~ formalArgList ~ ")" ~~~ ("{" ~ exp ~ "}").lw.?).map {
1290-
case (pos, (a, b, c)) =>
1291-
PPredicate(a, b, c)(pos)
1306+
def predicateDecl[$: P]: P[PPredicate] = FP(annotation.rep(0) ~ keyword("predicate") ~/ idndef ~ "(" ~ formalArgList ~ ")" ~~~ ("{" ~ exp ~ "}").lw.?).map {
1307+
case (pos, (anns, a, b, c)) =>
1308+
PPredicate(a, b, c)(pos, anns)
12921309
}
12931310

1294-
def methodDecl[$: P]: P[PMethod] = FP(methodSignature ~~~/ pre.lw.rep ~~~ post.lw.rep ~~~ block.lw.?).map {
1295-
case (pos, (name, args, rets, pres, posts, body)) =>
1296-
PMethod(name, args, rets.getOrElse(Nil), pres, posts, body)(pos)
1311+
def methodDecl[$: P]: P[PMethod] = FP(annotation.rep(0) ~ methodSignature ~~~/ pre.lw.rep ~~~ post.lw.rep ~~~ block.lw.?).map {
1312+
case (pos, (anns, (name, args, rets), pres, posts, body)) =>
1313+
PMethod(name, args, rets.getOrElse(Nil), pres, posts, body)(pos, anns)
12971314
}
12981315

12991316
def methodSignature[$: P] = P("method" ~/ idndef ~ "(" ~ formalArgList ~ ")" ~~~ ("returns" ~ "(" ~ formalArgList ~ ")").lw.?)

‎src/main/scala/viper/silver/parser/ParseAst.scala‎

Lines changed: 29 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -407,6 +407,11 @@ trait PExp extends PNode {
407407
def forceSubstitution(ts: PTypeSubstitution): Unit
408408
}
409409

410+
case class PAnnotatedExp(e: PExp, annotation: (String, Seq[String]))(val pos: (Position, Position)) extends PExp {
411+
override def typeSubstitutions: collection.Seq[PTypeSubstitution] = e.typeSubstitutions
412+
override def forceSubstitution(ts: PTypeSubstitution): Unit = e.forceSubstitution(ts)
413+
}
414+
410415
case class PMagicWandExp(override val left: PExp, override val right: PExp)(val posi: (Position, Position)) extends PBinExp(left, MagicWandOp.op, right)(posi) with PResourceAccess
411416

412417
class PTypeSubstitution(val m: Map[String, PType]) //extends Map[String,PType]()
@@ -1206,6 +1211,8 @@ trait PStmt extends PNode {
12061211
}
12071212
}
12081213

1214+
case class PAnnotatedStmt(stmt: PStmt, annotation: (String, Seq[String]))(val pos: (Position, Position)) extends PStmt
1215+
12091216
case class PSeqn(ss: Seq[PStmt])(val pos: (Position, Position)) extends PStmt with PScope
12101217

12111218
case class PFold(e: PExp)(val pos: (Position, Position)) extends PStmt
@@ -1325,7 +1332,9 @@ abstract class PErrorEntity extends PEntity {
13251332

13261333

13271334
// a member (like method or axiom) that is its own name scope
1328-
trait PMember extends PDeclaration with PScope
1335+
trait PMember extends PDeclaration with PScope {
1336+
1337+
}
13291338

13301339
trait PAnyFunction extends PMember with PGlobalDeclaration with PTypedDeclaration {
13311340
def idndef: PIdnDef
@@ -1343,46 +1352,46 @@ case class PLocalImport(file: String)(val pos: (Position, Position)) extends PIm
13431352

13441353
case class PStandardImport(file: String)(val pos: (Position, Position)) extends PImport()
13451354

1346-
case class PMethod(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], formalReturns: Seq[PFormalArgDecl], pres: Seq[PExp], posts: Seq[PExp], body: Option[PStmt])(val pos: (Position, Position)) extends PMember with PGlobalDeclaration {
1355+
case class PMethod(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], formalReturns: Seq[PFormalArgDecl], pres: Seq[PExp], posts: Seq[PExp], body: Option[PStmt])
1356+
(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PMember with PGlobalDeclaration {
13471357
def deepCopy(idndef: PIdnDef = this.idndef, formalArgs: Seq[PFormalArgDecl] = this.formalArgs, formalReturns: Seq[PFormalArgDecl] = this.formalReturns, pres: Seq[PExp] = this.pres, posts: Seq[PExp] = this.posts, body: Option[PStmt] = this.body): PMethod = {
13481358
StrategyBuilder.Slim[PNode]({
1349-
case p: PMethod => PMethod(idndef, formalArgs, formalReturns, pres, posts, body)(p.pos)
1359+
case p: PMethod => PMethod(idndef, formalArgs, formalReturns, pres, posts, body)(p.pos, p.annotations)
13501360
}).execute[PMethod](this)
13511361
}
13521362

13531363
def deepCopyWithNameSubstitution(idndef: PIdnDef = this.idndef, formalArgs: Seq[PFormalArgDecl] = this.formalArgs, formalReturns: Seq[PFormalArgDecl] = this.formalReturns, pres: Seq[PExp] = this.pres, posts: Seq[PExp] = this.posts, body: Option[PStmt] = this.body)
13541364
(idn_generic_name: String, idn_substitution: String): PMethod = {
13551365
StrategyBuilder.Slim[PNode]({
1356-
case p: PMethod => PMethod(idndef, formalArgs, formalReturns, pres, posts, body)(p.pos)
1366+
case p: PMethod => PMethod(idndef, formalArgs, formalReturns, pres, posts, body)(p.pos, p.annotations)
13571367
case p@PIdnDef(name) if name == idn_generic_name => PIdnDef(idn_substitution)(p.pos)
13581368
case p@PIdnUse(name) if name == idn_generic_name => PIdnUse(idn_substitution)(p.pos)
13591369
}).execute[PMethod](this)
13601370
}
13611371
}
13621372

1363-
case class PDomain(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], funcs: Seq[PDomainFunction], axioms: Seq[PAxiom], interpretations: Option[Map[String, String]])(val pos: (Position, Position)) extends PMember with PGlobalDeclaration
1364-
1365-
case class PFunction(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], typ: PType, pres: Seq[PExp], posts: Seq[PExp], body: Option[PExp])(val pos: (Position, Position)) extends PAnyFunction {
1373+
case class PDomain(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], funcs: Seq[PDomainFunction], axioms: Seq[PAxiom], interpretations: Option[Map[String, String]])
1374+
(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PMember with PGlobalDeclaration
1375+
case class PFunction(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], typ: PType, pres: Seq[PExp], posts: Seq[PExp], body: Option[PExp])
1376+
(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PAnyFunction {
13661377
def deepCopy(idndef: PIdnDef = this.idndef, formalArgs: Seq[PFormalArgDecl] = this.formalArgs, typ: PType = this.typ, pres: Seq[PExp] = this.pres, posts: Seq[PExp] = this.posts, body: Option[PExp] = this.body): PFunction = {
13671378
StrategyBuilder.Slim[PNode]({
1368-
case p: PFunction => PFunction(idndef, formalArgs, typ, pres, posts, body)(p.pos)
1379+
case p: PFunction => PFunction(idndef, formalArgs, typ, pres, posts, body)(p.pos, p.annotations)
13691380
}).execute[PFunction](this)
13701381
}
13711382
}
13721383

1373-
case class PDomainFunction(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl], typ: PType, unique: Boolean, interpretation: Option[String])(val domainName: PIdnUse)(val pos: (Position, Position)) extends PAnyFunction
1374-
1375-
case class PAxiom(idndef: Option[PIdnDef], exp: PExp)(val domainName: PIdnUse)(val pos: (Position, Position)) extends PScope
1376-
1377-
case class PField(idndef: PIdnDef, typ: PType)(val pos: (Position, Position)) extends PMember with PTypedDeclaration with PGlobalDeclaration
1378-
1379-
case class PPredicate(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], body: Option[PExp])(val pos: (Position, Position)) extends PMember with PTypedDeclaration with PGlobalDeclaration {
1384+
case class PDomainFunction(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl], typ: PType, unique: Boolean, interpretation: Option[String])
1385+
(val domainName:PIdnUse)(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PAnyFunction
1386+
case class PAxiom(idndef: Option[PIdnDef], exp: PExp)(val domainName:PIdnUse)(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PScope
1387+
case class PField(idndef: PIdnDef, typ: PType)(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PMember with PTypedDeclaration with PGlobalDeclaration
1388+
case class PPredicate(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], body: Option[PExp])
1389+
(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PMember with PTypedDeclaration with PGlobalDeclaration{
13801390
val typ = PPredicateType()()
13811391
}
13821392

1383-
case class PDomainFunction1(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl], typ: PType, unique: Boolean, interpretation: Option[String])(val pos: (Position, Position))
1384-
1385-
case class PAxiom1(idndef: Option[PIdnDef], exp: PExp)(val pos: (Position, Position))
1393+
case class PDomainFunction1(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl], typ: PType, unique: Boolean, interpretation: Option[String])(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])])
1394+
case class PAxiom1(idndef: Option[PIdnDef], exp: PExp)(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])])
13861395

13871396
/**
13881397
* A entity represented by names for whom we have seen more than one
@@ -1536,6 +1545,8 @@ object Nodes {
15361545
case PDefine(idndef, optArgs, body) => Seq(idndef) ++ optArgs.getOrElse(Nil) ++ Seq(body)
15371546
case PQuasihavoc(lhs, e) => lhs.toSeq :+ e
15381547
case PQuasihavocall(vars, lhs, e) => vars ++ lhs.toSeq :+ e
1548+
case PAnnotatedExp(e, _) => Seq(e)
1549+
case PAnnotatedStmt(s, _) => Seq(s)
15391550
case t: PExtender => t.getSubnodes()
15401551
case _: PSkip => Nil
15411552
case _: PUnnamedFormalArgDecl => Nil

‎src/main/scala/viper/silver/parser/Resolver.scala‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,8 @@ case class TypeChecker(names: NameAnalyser) {
172172

173173
def check(stmt: PStmt): Unit = {
174174
stmt match {
175+
case PAnnotatedStmt(s, _) =>
176+
check(s)
175177
case PMacroRef(id) =>
176178
messages ++= FastMessaging.message(stmt, "unknown macro used: " + id.name)
177179
case s@PSeqn(ss) =>
@@ -622,7 +624,10 @@ case class TypeChecker(names: NameAnalyser) {
622624

623625
case t: PExtender => t.typecheck(this, names).getOrElse(Nil) foreach (message =>
624626
messages ++= FastMessaging.message(t, message))
625-
case psl: PSimpleLiteral =>
627+
case PAnnotatedExp(e, _) =>
628+
checkInternal(e)
629+
setType(e.typ)
630+
case psl: PSimpleLiteral=>
626631
psl match {
627632
case r@PResultLit() =>
628633
if (resultAllowed)

0 commit comments

Comments
 (0)
⚡