C++ semantics [symbol] tags.

kframework · Oct 23, 2019 · cc2264c · cc2264c
1 parent 8217762
commit cc2264c
Show file tree

Hide file tree

Showing 4 changed files with 205 additions and 174 deletions.
diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h
@@ -355,7 +355,7 @@ class GetKastVisitor
                                                     TALI->NumTemplateArgs));
         } else {
           Kast::add(Kast::KApply("TemplateSpecialization", Sort::DECL, {Sort::ATYPE, Sort::DECL}));
-          Kast::add(Kast::KApply("TemplateSpecializationType", Sort::ATYPE, {Sort::CID}));
+          Kast::add(Kast::KApply("TemplateSpecializationType2", Sort::ATYPE, {Sort::CID}));
           TRY_TO(TraverseDeclarationName(FTSI->getTemplate()->getDeclName()));
         }
       } else if (FTSI->getTemplateSpecializationKind() != TSK_Undeclared &&
@@ -378,7 +378,7 @@ class GetKastVisitor
           } else {
              Kast::add(Kast::KApply("TemplateInstantiationDeclaration", Sort::DECL, {Sort::ATYPE, Sort::DECL}));
           }
-          Kast::add(Kast::KApply("TemplateSpecializationType", Sort::ATYPE, {Sort::CID}));
+          Kast::add(Kast::KApply("TemplateSpecializationType2", Sort::ATYPE, {Sort::CID}));
           TRY_TO(TraverseDeclarationName(FTSI->getTemplate()->getDeclName()));
         }
       }
@@ -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}));
+    std::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/common/compat.k b/semantics/common/compat.k
@@ -38,7 +38,7 @@ module COMPAT-SYNTAX
      syntax KItem ::= set(Set)
 
      syntax K ::= listToK(List) [function]
-     syntax List ::= kSeqToList(K) [function]
+     syntax List ::= kSeqToList(K) [function, symbol]
 
      syntax KTuple ::= kpair(K, K)
                     | ktriple(K, K, K)