Fixes.

kframework · Oct 23, 2019 · 396b2c3 · 396b2c3
1 parent 92bd95a
commit 396b2c3
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 17 deletions.
diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h
@@ -1070,7 +1070,13 @@ class GetKastVisitor
     if (T->getSizeModifier() != clang::ArrayType::Normal) {
       throw std::logic_error("unimplemented: static/* array");
     }
-    Kast::add(Kast::KApply("ArrayType", Sort::ATYPE, {Sort::ATYPE, sort}));
+    string arr;
+    if (sort == Sort::AEXPR) {
+       arr = "ArrayTypeAExpr";
+    } else {
+       arr = "ArrayType";
+    }
+    Kast::add(Kast::KApply(arr, Sort::ATYPE, {Sort::ATYPE, sort}));
     TRY_TO(TraverseType(T->getElementType()));
     return true;
   }

diff --git a/semantics/cpp/language/translation/syntax.k b/semantics/cpp/language/translation/syntax.k
@@ -61,7 +61,7 @@ module CPP-ABSTRACT-SYNTAX
 
      syntax StorageClassSpecifier ::= Mutable() [symbol]
 
-     // syntax FunctionSpecifier ::= Explicit() [symbol]
+     syntax FunctionSpecifier ::= Explicit()
 
      syntax Specifier ::= StorageClassSpecifier | FunctionSpecifier
                         | Constexpr() [symbol]
@@ -109,7 +109,7 @@ module CPP-ABSTRACT-SYNTAX
      syntax AType ::= CPPType
                     | ATypeResult
                     | ElaboratedTypeSpecifier(Tag, CId, NNS) [symbol]
-                    | ElaboratedTypeSpecifier(Tag, CId, NNS, List) // TODO(chathhorn): make symbol
+                    | ElaboratedTypeSpecifier(Tag, CId, NNS, List)
                     | FunctionPrototype(AType, StrictList, ExceptionSpec, Bool) [strict(1), symbol]
                     | MethodPrototype(Bool, Bool, AType, AType) [strict(3, 4), symbol]
                     | StaticMethodPrototype(AType) [strict, symbol]
@@ -120,15 +120,15 @@ module CPP-ABSTRACT-SYNTAX
                     | PointerType(AType) [strict, symbol]
                     | MemberPointerType(AType, AType) [strict, symbol]
                     | ArrayType(AType, Int) [strict(1), symbol]
-                    | ArrayType(AType, AExpr) [strict(1)]
+                    | ArrayTypeAExpr(AType, AExpr) [strict(1), symbol]
                     | TypedefType(CId) [symbol]
                     | QualifiedTypeName(Tag, NNS, AType) [symbol]
                     | Decltype(Expr) [symbol]
                     | TemplateParameterType(CId) [symbol]
                     | LValRefType(AType) [strict, symbol]
                     | RValRefType(AType) [strict, symbol]
-                    | TemplateSpecializationType(CId) [symbol]
                     | TemplateSpecializationType(CId, List) [symbol]
+                    | TemplateSpecializationType2(CId) [symbol]
                     | PackExpansionType(AType) [symbol]
                     | AutoType(Bool) [symbol]
                     | Name
@@ -183,28 +183,28 @@ module CPP-ABSTRACT-SYNTAX
                    | TBreakStmt() [symbol]
                    | ContinueStmt() [symbol]
                    | ReturnStmt(Init) [symbol]
-                   | IfTStmt(Decl, Stmt, Stmt) [symbol]
-                   | IfTStmt(Expr, Stmt, Stmt) [symbol]
-                   | WhileTStmt(Decl, Stmt) [symbol]
-                   | WhileTStmt(Expr, Stmt) [symbol]
+                   | IfTStmt(Decl, Stmt, Stmt)
+                   | IfTStmt(Expr, Stmt, Stmt)
+                   | WhileTStmt(Decl, Stmt)
+                   | WhileTStmt(Expr, Stmt)
                    | NullStmt() [symbol]
-                   | ForTStmt(Stmt, Expr, Stmt, Stmt) [symbol]
-                   | ForTStmt(Stmt, Decl, Stmt, Stmt) [symbol]
-                   | ForTStmt(Expr, Stmt, Stmt) [symbol]
+                   | ForTStmt(Stmt, Expr, Stmt, Stmt)
+                   | ForTStmt(Stmt, Decl, Stmt, Stmt)
+                   | ForTStmt(Expr, Stmt, Stmt)
                    | TemplateDefinitionStmt(K) [symbol] // synthetic statement created by the body of a function template definition when it's evaluted before instantiation
 
      syntax AStmt ::= NoStatement() [symbol]
                     | CompoundAStmt(List) [symbol]
                     | LabelAStmt(CId, List) [symbol]
                     | ForAStmt(AStmt, AExpr, AExpr, AStmt) [symbol]
-                    | ForAStmt(AStmt, Decl, AExpr, AStmt) [symbol]
-                    | WhileAStmt(Decl, AStmt) [symbol]
+                    | ForAStmt(AStmt, Decl, AExpr, AStmt)
+                    | WhileAStmt(Decl, AStmt)
                     | WhileAStmt(Expr, AStmt) [symbol]
                     | DoWhileAStmt(AStmt, Expr) [symbol]
                     | IfAStmt(Decl, AStmt, AStmt) [symbol]
-                    | IfAStmt(Expr, AStmt, AStmt) [symbol]
+                    | IfAStmt(Expr, AStmt, AStmt)
                     | SwitchAStmt(Decl, AStmt) [symbol]
-                    | SwitchAStmt(Expr, AStmt) [symbol]
+                    | SwitchAStmt(Expr, AStmt)
                     | CaseAStmt(Expr, AStmt) [symbol]
                     | DefaultAStmt(AStmt) [symbol]
                     | TryAStmt(AStmt, List) [symbol]

diff --git a/semantics/cpp/language/translation/typing/canonicalization.k b/semantics/cpp/language/translation/typing/canonicalization.k
@@ -61,7 +61,7 @@ module CPP-TRANSLATION-TYPING-CANONICALIZATION
 
      rule MemberPointerType(t(... st: classType(...)) #as D::CPPType, T:CPPType) => t(noQuals, .Set, memberPointerType(D, T))
 
-     rule ArrayType(T:CPPType, NoExpression()) => t(noQuals, .Set, incompleteArrayType(T))
+     rule ArrayTypeAExpr(T:CPPType, NoExpression()) => t(noQuals, .Set, incompleteArrayType(T))
 
      rule ArrayType(T:CPPType, I:Int) => t(noQuals, .Set, arrayType(T, I))