backup

src/main/antlr4/GobraLexer.g4

@@ -89,3 +89,6 @@ PROOF       : 'proof';
 GHOST_EQUALS     : '===';
 GHOST_NOT_EQUALS : '!==';
 WITH        : 'with';
+EXHALEMODE  : 'exhaleMode' -> mode(NLSEMI);
+MCE         : 'mce';
+STRICT      : 'strict';

src/main/antlr4/GobraParser.g4

@@ -162,7 +162,12 @@ sqType: (kind=(SEQ | SET | MSET | OPT) L_BRACKET type_ R_BRACKET)
 // Specifications
 
 specification returns[boolean trusted = false, boolean pure = false;]:
-  ((specStatement | PURE {$pure = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? // Non-greedily match PURE to avoid missing eos errors.
+  ((specStatement | PURE {$pure = true;} | (EXHALEMODE L_PAREN exhaleMode R_PAREN) | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? // Non-greedily match PURE to avoid missing eos errors.
+  ;
+
+exhaleMode
+  : MCE
+  | STRICT
   ;
 
 specStatement

src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java

@@ -1,4 +1,4 @@
-// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.0
+// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 
@@ -376,6 +376,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitSpecification(GobraParser.SpecificationContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitExhaleMode(GobraParser.ExhaleModeContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *

src/main/java/viper/gobra/frontend/GobraParserVisitor.java

@@ -1,4 +1,4 @@
-// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.0
+// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.ParseTreeVisitor;
 
@@ -326,6 +326,12 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitSpecification(GobraParser.SpecificationContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#exhaleMode}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitExhaleMode(GobraParser.ExhaleModeContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#specStatement}.
 	 * @param ctx the parse tree

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -876,13 +876,18 @@ case class PTupleTerminationMeasure(tuple: Vector[PExpression], cond: Option[PEx
 
 sealed trait PSpecification extends PGhostNode
 
+sealed trait PExhaleMode extends PNode
+case object PStrict extends PExhaleMode
+case object PMce extends PExhaleMode
+
 case class PFunctionSpec(
                       pres: Vector[PExpression],
                       preserves: Vector[PExpression],
                       posts: Vector[PExpression],
                       terminationMeasures: Vector[PTerminationMeasure],
+                      exhaleMode: Vector[PExhaleMode],
                       isPure: Boolean = false,
-                      isTrusted: Boolean = false
+                      isTrusted: Boolean = false,
                       ) extends PSpecification
 
 case class PBodyParameterInfo(

src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala

@@ -142,14 +142,20 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     "decreases" <+> measureDoc(measure)
   }
 
+  def showExhaleMode(mode: PExhaleMode): Doc = mode match {
+    case PStrict => "strict"
+    case PMce => "mce"
+  }
+
   def showSpec(spec: PSpecification): Doc = spec match {
-    case PFunctionSpec(pres, preserves, posts, measures, isPure, isTrusted) =>
+    case PFunctionSpec(pres, preserves, posts, measures, exhaleMode, isPure, isTrusted) =>
       (if (isPure) showPure else emptyDoc) <>
       (if (isTrusted) showTrusted else emptyDoc) <>
       hcat(pres map (showPre(_) <> line)) <>
-        hcat(preserves map (showPreserves(_) <> line)) <>
-        hcat(posts map (showPost(_) <> line)) <>
-        hcat(measures map (showTerminationMeasure(_) <> line))
+      hcat(preserves map (showPreserves(_) <> line)) <>
+      hcat(posts map (showPost(_) <> line)) <>
+      hcat(measures map (showTerminationMeasure(_) <> line)) <>
+      hcat(exhaleMode map (showExhaleMode(_) <> line))
 
     case PLoopSpec(inv, measure) =>
       hcat(inv map (showInv(_) <> line)) <> opt(measure)(showTerminationMeasure) <> line

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

@@ -425,7 +425,11 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     */
   override def visitMethodSpec(ctx: GobraParser.MethodSpecContext): PMethodSig = {
     val ghost = has(ctx.GHOST())
-    val spec = if (ctx.specification() != null) visitSpecification(ctx.specification()) else PFunctionSpec(Vector.empty,Vector.empty,Vector.empty, Vector.empty).at(ctx)
+    val spec =
+      if (ctx.specification() != null)
+        visitSpecification(ctx.specification())
+      else
+        PFunctionSpec(Vector.empty,Vector.empty,Vector.empty, Vector.empty, Vector.empty).at(ctx)
     // The name of each explicitly specified method must be unique and not blank.
     val id = idnDef.get(ctx.IDENTIFIER())
     val args = visitNode[Vector[Vector[PParameter]]](ctx.parameters())

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostLessPrinter.scala

@@ -21,7 +21,7 @@ class GhostLessPrinter(classifier: GhostClassifier) extends DefaultPrettyPrinter
           rec,
           filterParamList(args),
           filterResult(res),
-          PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty),
+          PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty),
           body.map( b => (PBodyParameterInfo(Vector.empty), b._2) )
         )
       )
@@ -32,7 +32,7 @@ class GhostLessPrinter(classifier: GhostClassifier) extends DefaultPrettyPrinter
           id,
           filterParamList(args),
           filterResult(res),
-          PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty),
+          PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty),
           body.map( b => (PBodyParameterInfo(Vector.empty), b._2) )
         )
       )
@@ -170,7 +170,7 @@ class GhostLessPrinter(classifier: GhostClassifier) extends DefaultPrettyPrinter
     case PFunctionLit(_, PClosureDecl(args, result, _, body)) => super.showMisc(PClosureDecl(
       filterParamList(args),
       filterResult(result),
-      PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty),
+      PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty),
       body.map( b => (PBodyParameterInfo(Vector.empty), b._2) )
     ))
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala

@@ -77,13 +77,14 @@ class GoifyingPrinter(info: TypeInfoImpl) extends DefaultPrettyPrinter {
     * Shows the Goified version of the function / method specification
     */
   override def showSpec(spec: PSpecification): Doc = spec match {
-    case PFunctionSpec(pres, preserves, posts, measures, isPure, isTrusted) =>
+    case PFunctionSpec(pres, preserves, posts, measures, exhaleMode, isPure, isTrusted) =>
       (if (isPure) specComment <+> showPure else emptyDoc) <>
       (if (isTrusted) specComment <+> showTrusted else emptyDoc) <>
       hcat(pres map (p => specComment <+> showPre(p) <> line)) <>
       hcat(preserves map (p => specComment <+> showPreserves(p) <> line)) <>
       hcat(posts map (p => specComment <+> showPost(p) <> line)) <>
-      hcat(measures map (p => specComment <+> showTerminationMeasure(p) <> line))
+      hcat(measures map (p => specComment <+> showTerminationMeasure(p) <> line)) <>
+      hcat(exhaleMode map (p => specComment <+> showExhaleMode(p) <> line))
 
     case PLoopSpec(inv, measure) =>
       hcat(inv map (p => specComment <+> showInv(p) <> line)) <>
@@ -124,7 +125,7 @@ class GoifyingPrinter(info: TypeInfoImpl) extends DefaultPrettyPrinter {
           rec,
           getActualParams(args),
           getActualResult(res),
-          PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty),
+          PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty),
           body
         )
       )
@@ -136,7 +137,7 @@ class GoifyingPrinter(info: TypeInfoImpl) extends DefaultPrettyPrinter {
           id,
           getActualParams(args),
           getActualResult(res),
-          PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty),
+          PFunctionSpec(Vector.empty, Vector.empty, Vector.empty, Vector.empty, Vector.empty),
           body
         )
       )

src/test/resources/regressions/features/mce/mce-success1.gobra

@@ -0,0 +1,10 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+requires true
+exhaleMode(strict)
+func f(x, y *int) {
+
+}