Merge remote-tracking branch 'origin/dev' into unique-fields

src/main/vct/main/stages/Transformation.scala

@@ -437,7 +437,6 @@ case class SilverTransformation(
         EncodeForPermWithValue,
         EncodeAutoValue,
         ExtractInlineQuantifierPatterns,
-        RewriteTriggerADTFunctions,
         MonomorphizeContractApplicables,
 
         // Silver compat (basically no new nodes)

src/parsers/antlr4/CPPParser.g4

@@ -1,7 +1,13 @@
 parser grammar CPPParser;
-options {tokenVocab = LangCPPLexer;}
+options {
+    superClass = CPPParserBase;
+    tokenVocab = LangCPPLexer;
+}
 import LangCPPParser, SpecParser;
 
+@header {
+    import vct.parsers.parser.CPPParserBase;
+}
 @parser::members {
     public int specLevel = 0;
 }

src/parsers/antlr4/LangCPPParser.g4

@@ -427,27 +427,21 @@ typeSpecifierSeq: typeSpecifier+ attributeSpecifierSeq?;
 trailingTypeSpecifierSeq:
 	trailingTypeSpecifier+ attributeSpecifierSeq?;
 
-simpleTypeLengthModifier:
-	Short
-	| Long;
-
-simpleTypeSignednessModifier:
-	Unsigned
-	| Signed;
-
 simpleTypeSpecifier:
 	nestedNameSpecifier? theTypeName
 	| nestedNameSpecifier Template simpleTemplateId
-	| simpleTypeSignednessModifier
-	| simpleTypeSignednessModifier? simpleTypeLengthModifier+
-	| simpleTypeSignednessModifier? Char
-	| simpleTypeSignednessModifier? Char16
-	| simpleTypeSignednessModifier? Char32
-	| simpleTypeSignednessModifier? Wchar
+	| Char
+	| Char16
+	| Char32
+	| Wchar
 	| Bool
-	| simpleTypeSignednessModifier? simpleTypeLengthModifier* Int
+	| Short
+	| Int
+	| Long
+	| Signed
+	| Unsigned
 	| Float
-	| simpleTypeLengthModifier? Double
+	| Double
 	| Void
 	| Auto
 	| {specLevel>0}? valType
@@ -610,28 +604,22 @@ abstractDeclarator:
 	| abstractPackDeclarator;
 
 pointerAbstractDeclarator:
-	noPointerAbstractDeclarator
-	| pointerOperatorWithDoubleStar+ noPointerAbstractDeclarator?;
+    pointerOperatorWithDoubleStar* (noPointerAbstractDeclarator | pointerOperatorWithDoubleStar);
 
 noPointerAbstractDeclarator:
-	noPointerAbstractDeclarator (
-		parametersAndQualifiers
-		| noPointerAbstractDeclarator LeftBracket constantExpression? RightBracket
-			attributeSpecifierSeq?
-	)
-	| parametersAndQualifiers
-	| LeftBracket constantExpression? RightBracket attributeSpecifierSeq?
-	| LeftParen pointerAbstractDeclarator RightParen;
+    (parametersAndQualifiers | LeftParen pointerAbstractDeclarator RightParen) (
+        parametersAndQualifiers
+        | LeftBracket constantExpression? RightBracket attributeSpecifierSeq?
+    )*;
 
 abstractPackDeclarator:
 	pointerOperatorWithDoubleStar* noPointerAbstractPackDeclarator;
 
 noPointerAbstractPackDeclarator:
-	noPointerAbstractPackDeclarator (
+	Ellipsis (
 		parametersAndQualifiers
 		| LeftBracket constantExpression? RightBracket attributeSpecifierSeq?
-	)
-	| Ellipsis;
+	)*;
 
 parameterDeclarationClause:
 	parameterDeclarationList parameterDeclarationVarargs?;
@@ -713,11 +701,10 @@ memberDeclaratorList:
 	memberDeclarator (Comma memberDeclarator)*;
 
 memberDeclarator:
-	declarator (
-		virtualSpecifierSeq? pureSpecifier?
-		| braceOrEqualInitializer?
-	)
-	| clangppIdentifier? attributeSpecifierSeq? Colon constantExpression;
+	 declarator (virtualSpecifierSeq | { this.IsPureSpecifierAllowed() }? pureSpecifier | { this.IsPureSpecifierAllowed() }? virtualSpecifierSeq pureSpecifier | braceOrEqualInitializer)
+    | declarator
+    | clangppIdentifier? attributeSpecifierSeq? Colon constantExpression
+    ;
 
 virtualSpecifierSeq: virtualSpecifier+;
 
@@ -727,8 +714,7 @@ virtualSpecifier: Override | Final;
  */
 
 pureSpecifier:
-	Assign val = OctalLiteral {if($val.text.compareTo("0")!=0) throw new InputMismatchException(this);
-		};
+    Assign IntegerLiteral;
 
 //Derived classes
 baseClause: Colon baseSpecifierList;

src/parsers/vct/parsers/parser/CPPParserBase.java

@@ -0,0 +1,28 @@
+package vct.parsers.parser;
+
+import org.antlr.v4.runtime.*;
+
+public abstract class CPPParserBase extends Parser
+{
+    protected CPPParserBase(TokenStream input)
+    {
+        super(input);
+    }
+
+    protected boolean IsPureSpecifierAllowed()
+    {
+        try
+        {
+            var x = this._ctx; // memberDeclarator
+            var c = x.getChild(0).getChild(0);
+            var c2 = c.getChild(0);
+            var p = c2.getChild(1);
+            if (p == null) return false;
+            return (p instanceof vct.antlr4.generated.CPPParser.ParametersAndQualifiersContext);
+        }
+        catch (Exception e)
+        {
+        }
+        return false;
+    }
+}

src/parsers/vct/parsers/transform/CPPToCol.scala

@@ -897,53 +897,39 @@ case class CPPToCol[G](
           case _ => ??(typeSpec)
         }
       case SimpleTypeSpecifier1(_, _, _) => ??(typeSpec)
-      case SimpleTypeSpecifier2(signedness) => Seq(convert(signedness))
-      case SimpleTypeSpecifier3(Some(signedness), typeLengthMods) =>
-        Seq(convert(signedness)) ++ typeLengthMods.map(convert(_))
-      case SimpleTypeSpecifier3(None, typeLengthMods) =>
-        typeLengthMods.map(convert(_))
-      case SimpleTypeSpecifier4(Some(signedness), _) =>
-        Seq(convert(signedness), new CPPChar[G]())
-      case SimpleTypeSpecifier4(None, _) => Seq(new CPPChar[G]())
-      case SimpleTypeSpecifier5(_, _) => ??(typeSpec)
-      case SimpleTypeSpecifier6(_, _) => ??(typeSpec)
-      case SimpleTypeSpecifier7(_, _) => ??(typeSpec)
-      case SimpleTypeSpecifier8(_) => Seq(new CPPBool[G]())
-      case SimpleTypeSpecifier9(Some(signedness), typeLengthMods, _) =>
-        Seq(convert(signedness)) ++ typeLengthMods.map(convert(_)) :+
-          new CPPInt[G]()
-      case SimpleTypeSpecifier9(None, typeLengthMods, _) =>
-        typeLengthMods.map(convert(_)) :+ new CPPInt[G]()
-      case SimpleTypeSpecifier10(_) =>
+      // Char
+      case SimpleTypeSpecifier2(_) => Seq(new CPPChar[G]())
+      // Char16
+      case SimpleTypeSpecifier3(_) => ??(typeSpec)
+      // Char32
+      case SimpleTypeSpecifier4(_) => ??(typeSpec)
+      // Wchar
+      case SimpleTypeSpecifier5(_) => ??(typeSpec)
+      // Bool
+      case SimpleTypeSpecifier6(_) => Seq(new CPPBool[G]())
+      // Short
+      case SimpleTypeSpecifier7(_) => ??(typeSpec)
+      // Int
+      case SimpleTypeSpecifier8(_) => Seq(new CPPInt[G]())
+      // Long
+      case SimpleTypeSpecifier9(_) => ??(typeSpec)
+      // Signed
+      case SimpleTypeSpecifier10(_) => Seq(new CPPSigned[G]())
+      // Signed
+      case SimpleTypeSpecifier11(_) => Seq(new CPPUnsigned[G]())
+      // Float
+      case SimpleTypeSpecifier12(_) =>
         Seq(CPPSpecificationType(TFloats.C_ieee754_32bit))
-      case SimpleTypeSpecifier11(Some(typeLengthMod), _) =>
-        Seq(
-          convert(typeLengthMod),
-          CPPSpecificationType(TFloats.C_ieee754_64bit),
-        )
-      case SimpleTypeSpecifier11(None, _) =>
+      // Double
+      case SimpleTypeSpecifier13(_) =>
         Seq(CPPSpecificationType(TFloats.C_ieee754_64bit))
-      case SimpleTypeSpecifier12(_) => Seq(new CPPVoid[G]())
-      case SimpleTypeSpecifier13(_) => ??(typeSpec)
-      case SimpleTypeSpecifier14(valType) =>
-        Seq(CPPSpecificationType(convert(valType)))
+      // Void
+      case SimpleTypeSpecifier14(_) => Seq(new CPPVoid[G]())
+      // Auto
       case SimpleTypeSpecifier15(_) => ??(typeSpec)
-    }
-
-  def convert(
-      implicit signedness: SimpleTypeSignednessModifierContext
-  ): CPPTypeSpecifier[G] =
-    signedness match {
-      case SimpleTypeSignednessModifier0(_) => new CPPUnsigned[G]()
-      case SimpleTypeSignednessModifier1(_) => new CPPSigned[G]()
-    }
-
-  def convert(
-      implicit simpleTypeLengthMod: SimpleTypeLengthModifierContext
-  ): CPPTypeSpecifier[G] =
-    simpleTypeLengthMod match {
-      case SimpleTypeLengthModifier0(_) => new CPPShort[G]()
-      case SimpleTypeLengthModifier1(_) => new CPPLong[G]()
+      case SimpleTypeSpecifier16(valType) =>
+        Seq(CPPSpecificationType(convert(valType)))
+      case SimpleTypeSpecifier17(_) => ??(typeSpec)
     }
 
   // Do not support template or decltypes, or a typename as identifier in the nestedname