From 459629d97c160ea182e9251bcd6a6c737a32ad85 Mon Sep 17 00:00:00 2001 From: chathhorn Date: Tue, 22 Oct 2019 23:22:44 -0500 Subject: [PATCH] Fixes. --- semantics/c/language/common/conversion.k | 2 - .../c/language/translation/typing/expr.k | 6 --- semantics/c/library/stdio.k | 2 +- semantics/cpp/language/common/class.k | 21 +++++----- semantics/cpp/language/common/dynamic.k | 5 +-- semantics/cpp/language/common/syntax.k | 10 ++--- semantics/cpp/language/common/typing.k | 38 +++++++++---------- .../language/translation/decl/declarator.k | 25 ++++++------ .../language/translation/decl/initializer.k | 4 +- semantics/cpp/language/translation/env.k | 24 ++++++------ .../cpp/language/translation/overloading.k | 2 +- semantics/cpp/language/translation/syntax.k | 9 ++--- .../cpp/language/translation/typing/expr.k | 2 +- .../cpp/language/translation/value-category.k | 2 +- 14 files changed, 71 insertions(+), 81 deletions(-) diff --git a/semantics/c/language/common/conversion.k b/semantics/c/language/common/conversion.k index 1675a0634..ef9d26d32 100644 --- a/semantics/c/language/common/conversion.k +++ b/semantics/c/language/common/conversion.k @@ -358,8 +358,6 @@ module C-CONVERSION | implPointerToInt() rule lintCastingAwayQuals() => .K requires notBool hasLint - rule implPointerToInt() => .K - requires notBool hasLint syntax UType ::= castTypes(UType, UType) [function] rule castTypes(ut(_, T'::SimpleUType), ut(Mods::Set, _)) => ut(Mods, T') diff --git a/semantics/c/language/translation/typing/expr.k b/semantics/c/language/translation/typing/expr.k index cdffa2ae6..aba2d24ab 100644 --- a/semantics/c/language/translation/typing/expr.k +++ b/semantics/c/language/translation/typing/expr.k @@ -42,8 +42,6 @@ module C-TYPING-EXPR context typeof((HOLE:KItem => typeof(HOLE)) % _) [result(Type)] context typeof((HOLE:KItem => typeof(HOLE)) + _) [result(Type)] context typeof((HOLE:KItem => typeof(HOLE)) - _) [result(Type)] - context typeof((HOLE:KItem => typeof(HOLE)) == _) [result(Type)] - context typeof((HOLE:KItem => typeof(HOLE)) != _) [result(Type)] context typeof((HOLE:KItem => typeof(HOLE)) & _) [result(Type)] context typeof((HOLE:KItem => typeof(HOLE)) ^ _) [result(Type)] context typeof((HOLE:KItem => typeof(HOLE)) | _) [result(Type)] @@ -70,13 +68,9 @@ module C-TYPING-EXPR context typeof(_ % (HOLE:KItem => typeof(HOLE))) [result(Type)] context typeof(_ + (HOLE:KItem => typeof(HOLE))) [result(Type)] context typeof(_ - (HOLE:KItem => typeof(HOLE))) [result(Type)] - context typeof(_ == (HOLE:KItem => typeof(HOLE))) [result(Type)] - context typeof(_ != (HOLE:KItem => typeof(HOLE))) [result(Type)] context typeof(_ & (HOLE:KItem => typeof(HOLE))) [result(Type)] context typeof(_ ^ (HOLE:KItem => typeof(HOLE))) [result(Type)] context typeof(_ | (HOLE:KItem => typeof(HOLE))) [result(Type)] - context typeof(_ && (HOLE:KItem => typeof(HOLE))) [result(Type)] - context typeof(_ || (HOLE:KItem => typeof(HOLE))) [result(Type)] // primary expressions rule typeof(X:CId => T:Type) ... diff --git a/semantics/c/library/stdio.k b/semantics/c/library/stdio.k index c7b4a4fb3..fad93fb58 100644 --- a/semantics/c/library/stdio.k +++ b/semantics/c/library/stdio.k @@ -1659,7 +1659,7 @@ module LIBC-STDIO syntax List ::= tail(List) [function] rule tail(ListItem(_) L::List) => L - rule tail(_) => .List [owise] + rule tail(.List) => .List syntax String ::= fst(ParseStrResult) [function, klabel(fstParseStr)] rule fst(parseStrResult(S::String, _)) => S diff --git a/semantics/cpp/language/common/class.k b/semantics/cpp/language/common/class.k index ada354129..af92f596d 100644 --- a/semantics/cpp/language/common/class.k +++ b/semantics/cpp/language/common/class.k @@ -10,10 +10,6 @@ module CPP-CLASS-BASIC-SORTS syntax LocalQualifier - syntax LocalClass - - syntax InnerClass - syntax ClassSpecifier endmodule // CPP-CLASS-BASIC-SORTS @@ -39,15 +35,20 @@ module CPP-CLASS-BASIC-SYNTAX syntax Class ::= ClassQualifier "::" ClassSpecifier [klabel(classId)] - syntax LocalClass ::= LocalQualifier "::" ClassSpecifier [klabel(classId)] + // TODO(chathhorn): the stuff below causes parsing ambiguities with the Class production above. Need to resolve in + // a better way. + syntax InnerClass ::= Class // TODO(chathhorn): added as an interim fix. + syntax LocalInnerClass ::= Class // TODO(chathhorn): added as an interim fix. + + // syntax LocalClass ::= LocalQualifier "::" ClassSpecifier [klabel(classId)] - syntax Class ::= LocalClass - syntax Class ::= InnerClass + // syntax Class ::= LocalClass + // syntax Class ::= InnerClass - syntax InnerClass ::= Class "::" ClassSpecifier [klabel(classId)] + // syntax InnerClass ::= Class "::" ClassSpecifier [klabel(classId)] - syntax LocalInnerClass ::= LocalClass - | LocalInnerClass "::" ClassSpecifier [klabel(classId)] + // syntax LocalInnerClass ::= LocalClass + // | LocalInnerClass "::" ClassSpecifier [klabel(classId)] syntax ClassSpecifier ::= Class(Tag, CId, TemplateArgs) [klabel(classSpecifier)] diff --git a/semantics/cpp/language/common/dynamic.k b/semantics/cpp/language/common/dynamic.k index 74cc6e6bc..4064ffc02 100644 --- a/semantics/cpp/language/common/dynamic.k +++ b/semantics/cpp/language/common/dynamic.k @@ -8,8 +8,6 @@ module CPP-NAMESPACE-SORTS syntax NamespaceSpecifier - syntax UnnamedNamespace - endmodule // CPP-NAMESPACE-SORTS module CPP-NAMESPACE-SYNTAX @@ -20,7 +18,6 @@ module CPP-NAMESPACE-SYNTAX syntax Namespace ::= Namespace "::" NamespaceSpecifier | NoNamespace() // signifies a declaration at block scope - | UnnamedNamespace syntax NamespaceSpecifier ::= Namespace(CId) @@ -586,7 +583,7 @@ module CPP-DYNAMIC-OTHER-SYNTAX syntax DefaultArguments ::= DefaultArgumentsResult - syntax DefaultArgumentsResult ::= defArgs(vals: StrictListResult, types: StrictListResult, cats: StrictListResult) + syntax DefaultArgumentsResult ::= defArgsResult(vals: StrictListResult, types: StrictListResult, cats: StrictListResult) endmodule // CPP-DYNAMIC-OTHER-SYNTAX diff --git a/semantics/cpp/language/common/syntax.k b/semantics/cpp/language/common/syntax.k index 0731ae457..c3823c647 100644 --- a/semantics/cpp/language/common/syntax.k +++ b/semantics/cpp/language/common/syntax.k @@ -193,19 +193,19 @@ module CPP-SYNTAX syntax Expr ::= ConvertType(CPPType, Expr) | ExprLoc - syntax ExprLoc ::= ExprLoc(CabsLoc, Expr) + syntax ExprLoc ::= ExprLoc(CabsLoc, Expr) [symbol] - syntax Init ::= ExprLoc(CabsLoc, Init) + syntax Init ::= InitLoc(CabsLoc, Init) - syntax BraceInit ::= ExprLoc(CabsLoc, BraceInit) + syntax BraceInit ::= BraceInitLoc(CabsLoc, BraceInit) syntax Block ::= BlockStmt(List) | BlockStmt(Int, List) syntax Decl - syntax Stmt ::= LabelStmt(CId, List) - | GotoStmt(CId) + syntax Stmt ::= LabelStmt(CId, List) [symbol] + | GotoStmt(CId) [symbol] | ExpressionStmt(Expr) [strict(c)] | PRValExpressionStmt(Expr) [strict(c)] | BreakStmt() diff --git a/semantics/cpp/language/common/typing.k b/semantics/cpp/language/common/typing.k index b988f5c37..68333c58d 100644 --- a/semantics/cpp/language/common/typing.k +++ b/semantics/cpp/language/common/typing.k @@ -78,35 +78,35 @@ module CPP-TYPING-SYNTAX | CPPSimpleDependentType | CPPSimpleAutoType - syntax CPPSimpleSignedType ::= bitfieldType(CPPSimpleSignedType, Int) [klabel(bitfieldTypeCpp)] + // syntax CPPSimpleSignedType ::= bitfieldType(CPPSimpleSignedType, Int) [klabel(bitfieldTypeCpp)] - syntax CPPSimpleUnsignedType ::= bitfieldType(CPPSimpleUnsignedType, Int) [klabel(bitfieldTypeCpp)] + // syntax CPPSimpleUnsignedType ::= bitfieldType(CPPSimpleUnsignedType, Int) [klabel(bitfieldTypeCpp)] - syntax CPPSimpleSignedCharType ::= bitfieldType(CPPSimpleSignedCharType, Int) [klabel(bitfieldTypeCpp)] + // syntax CPPSimpleSignedCharType ::= bitfieldType(CPPSimpleSignedCharType, Int) [klabel(bitfieldTypeCpp)] - syntax CPPSimpleUnsignedCharType ::= bitfieldType(CPPSimpleUnsignedCharType, Int) [klabel(bitfieldTypeCpp)] + // syntax CPPSimpleUnsignedCharType ::= bitfieldType(CPPSimpleUnsignedCharType, Int) [klabel(bitfieldTypeCpp)] - syntax CPPSimpleBoolType ::= bitfieldType(CPPSimpleBoolType, Int) [klabel(bitfieldTypeCpp)] + // syntax CPPSimpleBoolType ::= bitfieldType(CPPSimpleBoolType, Int) [klabel(bitfieldTypeCpp)] - syntax CPPSimpleWideCharType ::= bitfieldType(CPPSimpleWideCharType, Int) [klabel(bitfieldTypeCpp)] + // syntax CPPSimpleWideCharType ::= bitfieldType(CPPSimpleWideCharType, Int) [klabel(bitfieldTypeCpp)] - syntax CPPSimpleScopedEnumType ::= bitfieldType(CPPSimpleScopedEnumType, Int) [klabel(bitfieldTypeCpp)] + // syntax CPPSimpleScopedEnumType ::= bitfieldType(CPPSimpleScopedEnumType, Int) [klabel(bitfieldTypeCpp)] - syntax CPPSimpleUnscopedEnumType ::= bitfieldType(CPPSimpleUnscopedEnumType, Int) [klabel(bitfieldTypeCpp)] + // syntax CPPSimpleUnscopedEnumType ::= bitfieldType(CPPSimpleUnscopedEnumType, Int) [klabel(bitfieldTypeCpp)] syntax CPPSimpleBitfieldType ::= bitfieldType(CPPSimpleType, Int) [klabel(bitfieldTypeCpp)] - syntax CPPSimpleSignedType ::= CPPSimpleBottomType - syntax CPPSimpleUnsignedType ::= CPPSimpleBottomType - syntax CPPSimpleSignedCharType ::= CPPSimpleBottomType - syntax CPPSimpleUnsignedCharType ::= CPPSimpleBottomType - syntax CPPSimpleBoolType ::= CPPSimpleBottomType - syntax CPPSimpleWideCharType ::= CPPSimpleBottomType - syntax CPPSimpleScopedEnumType ::= CPPSimpleBottomType - syntax CPPSimpleUnscopedEnumType ::= CPPSimpleBottomType - syntax CPPSimpleBitfieldType ::= CPPSimpleBottomType - - syntax CPPSimpleBottomType ::= bitfieldType(CPPSimpleBottomType, Int) [klabel(bitfieldTypeCpp)] + // syntax CPPSimpleSignedType ::= CPPSimpleBottomType + // syntax CPPSimpleUnsignedType ::= CPPSimpleBottomType + // syntax CPPSimpleSignedCharType ::= CPPSimpleBottomType + // syntax CPPSimpleUnsignedCharType ::= CPPSimpleBottomType + // syntax CPPSimpleBoolType ::= CPPSimpleBottomType + // syntax CPPSimpleWideCharType ::= CPPSimpleBottomType + // syntax CPPSimpleScopedEnumType ::= CPPSimpleBottomType + // syntax CPPSimpleUnscopedEnumType ::= CPPSimpleBottomType + // syntax CPPSimpleBitfieldType ::= CPPSimpleBottomType + + // syntax CPPSimpleBottomType ::= bitfieldType(CPPSimpleBottomType, Int) [klabel(bitfieldTypeCpp)] syntax CPPSimpleSignedType ::= CPPSimpleSignedCharType | "short" | "int" | "long" | "long-long" | "oversized" diff --git a/semantics/cpp/language/translation/decl/declarator.k b/semantics/cpp/language/translation/decl/declarator.k index ff4b8935a..f350ae328 100644 --- a/semantics/cpp/language/translation/decl/declarator.k +++ b/semantics/cpp/language/translation/decl/declarator.k @@ -8,7 +8,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR-SYNTAX imports CPP-SORTS imports CPP-TYPING-SORTS - syntax Decl ::= DeclaratorAndSpecifiers(Declarator, Set) + syntax Decl ::= DeclaratorAndSpecifiers(Decl, Set) | declareObject(NNSVal, NNSVal, CId, CId, CPPType, Init, DeclarationType, Linkage, Duration, Set) | defineObject(NNSVal, CId, CId, CPPType, Init, DeclarationType, Set) | initializeObject(NNSVal, CId, CPPType, init: KItem, DeclarationType) [strict(c; 4)] @@ -53,18 +53,18 @@ module CPP-TRANSLATION-DECL-DECLARATOR imports CPP-TRANSLATION-CONSTANT-SYNTAX imports CPP-TRANSLATION-DECL-CLASS-DESTRUCTOR - rule FunctionDecl(N::NNSVal, X::CId, Mangled::CId, T::CPPType, Params::List) + rule FunctionDecl(N::NNS, X::CId, Mangled::CId, T::AType, Params::List) => NormalizedDecl(N, X, Mangled, T, NoInit(), Function(Params)) [anywhere] - rule VarDecl(N::NNSVal, X::CId, Mangled::CId, T::CPPType, Init::Init, IsDirect:Bool) + rule VarDecl(N::NNS, X::CId, Mangled::CId, T::AType, Init::Init, IsDirect:Bool) => NormalizedDecl(N, X, Mangled, T, Init, Var(#if IsDirect #then DirectInit() #else CopyInit() #fi)) [anywhere] - rule FunctionDefinition(N::NNSVal, X::CId, Mangled::CId, T::CPPType, Params::List, Body::Stmt) + rule FunctionDefinition(N::NNS, X::CId, Mangled::CId, T::AType, Params::List, Body::Stmt) => NormalizedDecl(N, X, Mangled, T, Body, Function(Params)) [anywhere] rule DeclStmt(L::List) => listToK(L) - rule Specifier(S::Specifier, D:Declarator) => DeclaratorAndSpecifiers(D, SetItem(S)) + rule Specifier(S::Specifier, D::Decl) => DeclaratorAndSpecifiers(D, SetItem(S)) requires S =/=K Auto() [anywhere] // Auto is a type specifier in C++ so it is handled elsewhere by AutoType @@ -151,8 +151,6 @@ module CPP-TRANSLATION-DECL-DECLARATOR rule getClassLinkage(_:LocalQualifier :: _) => NoLinkage // @ref n4296 3.5:4 - rule getNamespaceLinkage(N:UnnamedNamespace) => InternalLinkage - rule getNamespaceLinkage(GlobalNamespace()) => ExternalLinkage rule getNamespaceLinkage(Parent::Namespace :: _) => getNamespaceLinkage(Parent) [owise] @@ -418,7 +416,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR syntax CPPType ::= completeDeclaration(CPPType, Init) [function] - rule completeDeclaration(T::CPPType, (ExprLoc(_, I::Init) => I)) + rule completeDeclaration(T::CPPType, (InitLoc(_, I::Init) => I)) // @ref n4296 8.5.4:3.2 (char x[] = {"foo"}) rule completeDeclaration(t(Q::Quals, Mods::Set, incompleteArrayType(t(Q'::Quals, Mods'::Set, T:CPPSimpleCharType))), BraceInit(ListItem(StringLiteral(Narrow::CharKind, S::String)))) => t(Q, Mods, arrayType(t(Q', Mods', T), lengthString(S) +Int 1)) @@ -790,9 +788,12 @@ module CPP-TRANSLATION-DECL-DECLARATOR rule stripInitHolds(V::Val) => V requires isEvalVal(V) - context defArgs(_, (HOLE:StrictList => types(HOLE)), _) + context defArgs(_, (HOLE::StrictList => types(HOLE)), _) + + context defArgs(_, _, (HOLE::StrictList => cats(HOLE))) - context defArgs(_, _, (HOLE:StrictList => cats(HOLE))) + rule defArgs(A:StrictListResult, B:StrictListResult, C:StrictListResult) + => defArgsResult(A, B, C) syntax DefaultArguments ::= computeDefaultArgs(CPPType, DeclarationType) @@ -841,7 +842,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR rule #makeFunctionDeclarationType(_, .List) => .List rule emptyDefaultArguments(t(... st: functionType(...)) #as T::CPPType) - => #emptyDefaultArguments(#if hasImplicitParameter(T) #then size(getRealParams(T)) -Int 1 #else size(getRealParams(T)) #fi, defArgs(krlist(.List), krlist(.List), krlist(.List))) + => #emptyDefaultArguments(#if hasImplicitParameter(T) #then size(getRealParams(T)) -Int 1 #else size(getRealParams(T)) #fi, defArgsResult(krlist(.List), krlist(.List), krlist(.List))) rule emptyDefaultArguments(_) => NoDefArgs() [owise] @@ -850,7 +851,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR rule #emptyDefaultArguments(0, DA::DefaultArgumentsResult) => DA rule #emptyDefaultArguments(N::Int => N -Int 1, - defArgs(krlist(_::List (.List => ListItem(NoArg()))), + defArgsResult(krlist(_::List (.List => ListItem(NoArg()))), krlist(_::List (.List => ListItem(NoInitType()))), krlist(_::List (.List => ListItem(NoInitCat()))))) [owise] endmodule diff --git a/semantics/cpp/language/translation/decl/initializer.k b/semantics/cpp/language/translation/decl/initializer.k index 1d135243d..a3110479e 100644 --- a/semantics/cpp/language/translation/decl/initializer.k +++ b/semantics/cpp/language/translation/decl/initializer.k @@ -102,7 +102,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER syntax KItem ::= #figureInitHeatBase(destT: CPPType, type: InitType, init: Init, srcT: K, srcCat: K, ConstructorType, Duration) - rule #figureInit(... init: ExprLoc(L::CabsLoc, I::Init) => I) ... + rule #figureInit(... init: InitLoc(L::CabsLoc, I::Init) => I) ... _ => L // @ref n4296 8.5:6.1 @@ -416,7 +416,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER rule #evalBraceOrEqualInitializer(_, _, NoInit()) => BraceInit(.List) - rule #evalBraceOrEqualInitializer(_, _, ExprLoc(L::CabsLoc, I::Init) => I) + rule #evalBraceOrEqualInitializer(_, _, InitLoc(L::CabsLoc, I::Init) => I) rule #evalBraceOrEqualInitializer(C::Class, Base::Expr, BraceInit(L::List)) => BraceInit(#evalBraceOrEqualInitializers(C, Base, L)) diff --git a/semantics/cpp/language/translation/env.k b/semantics/cpp/language/translation/env.k index 271a8b919..c12b82eed 100644 --- a/semantics/cpp/language/translation/env.k +++ b/semantics/cpp/language/translation/env.k @@ -99,11 +99,11 @@ module CPP-TRANSLATION-ENV CE::Map => CE[X <- stripType(T) |-> (T, envEntry(Base, IsUsing, NoDefArgs()))] requires notBool isCPPFunctionType(T) - rule getDefaultArgsVals(defArgs(... vals: krlist(Args::List))) => Args + rule getDefaultArgsVals(defArgsResult(... vals: krlist(Args::List))) => Args - rule getDefaultArgsTypes(defArgs(... types: krlist(Types::List))) => Types + rule getDefaultArgsTypes(defArgsResult(... types: krlist(Types::List))) => Types - rule getDefaultArgsCats(defArgs(... cats: krlist(Cats::List))) => Cats + rule getDefaultArgsCats(defArgsResult(... cats: krlist(Cats::List))) => Cats syntax Map ::= updateFnEnv(Map, CId, CPPType, SymBase, Bool) [function] @@ -123,38 +123,38 @@ module CPP-TRANSLATION-ENV syntax DefaultArgumentsResult ::= #updateDefaultArgs(newArgs: DefaultArgumentsResult, oldArgs: DefaultArgumentsResult) [function] rule #updateDefaultArgs(NewArgs::DefaultArgumentsResult, OldArgs::DefaultArgumentsResult) - => #updateDefaultArgs(NewArgs, OldArgs, defArgs(krlist(.List), krlist(.List), krlist(.List))) + => #updateDefaultArgs(NewArgs, OldArgs, defArgsResult(krlist(.List), krlist(.List), krlist(.List))) syntax DefaultArgumentsResult ::= #updateDefaultArgs(newArgs: DefaultArgumentsResult, oldArgs: DefaultArgumentsResult, resultArgs: DefaultArgumentsResult) [function, klabel(updateDefaultArgsHelper)] // The next rule compensates for the clang policy to aggregate existing default args from previous declarations // Hence, we'll trust clang to check that the user does not redefine an old def. arg. rule #updateDefaultArgs( - defArgs(krlist((ListItem(_) => .List) _), + defArgsResult(krlist((ListItem(_) => .List) _), krlist((ListItem(_) => .List) _), krlist((ListItem(_) => .List) _)), - defArgs(krlist((ListItem(I:KItem) => .List) _), + defArgsResult(krlist((ListItem(I:KItem) => .List) _), krlist((ListItem(T::CPPDType) => .List) _), krlist((ListItem(C::ValueCategory) => .List) _)), - defArgs(krlist(_::List (.List => ListItem(I:KItem))), + defArgsResult(krlist(_::List (.List => ListItem(I:KItem))), krlist(_::List (.List => ListItem(T::CPPDType))), krlist(_::List (.List => ListItem(C::ValueCategory))))) requires I =/=K NoArg() rule #updateDefaultArgs( - defArgs(krlist((ListItem(I:KItem) => .List) _), + defArgsResult(krlist((ListItem(I:KItem) => .List) _), krlist((ListItem(T::CPPDType) => .List) _), krlist((ListItem(C::ValueCategory) => .List) _)), - defArgs(krlist((ListItem(NoArg()) => .List) _), + defArgsResult(krlist((ListItem(NoArg()) => .List) _), krlist((ListItem(_) => .List) _), krlist((ListItem(_) => .List) _)), - defArgs(krlist(_::List (.List => ListItem(I:KItem))), + defArgsResult(krlist(_::List (.List => ListItem(I:KItem))), krlist(_::List (.List => ListItem(T::CPPDType))), krlist(_::List (.List => ListItem(C::ValueCategory))))) rule #updateDefaultArgs( - defArgs(krlist(.List), krlist(.List), krlist(.List)), - defArgs(krlist(.List), krlist(.List), krlist(.List)), + defArgsResult(krlist(.List), krlist(.List), krlist(.List)), + defArgsResult(krlist(.List), krlist(.List), krlist(.List)), DA::DefaultArgumentsResult) => DA rule clearScope() => .K ... diff --git a/semantics/cpp/language/translation/overloading.k b/semantics/cpp/language/translation/overloading.k index b2237374f..6402d3b57 100644 --- a/semantics/cpp/language/translation/overloading.k +++ b/semantics/cpp/language/translation/overloading.k @@ -606,7 +606,7 @@ module CPP-TRANSLATION-OVERLOADING requires isCPPPointerType(T) andBool isCPPFunctionType(innerType(T)) // only one viable candidate - rule bestViable(T::CPPType, envEntry(... base: Base::SymBase, defaultArgs: defArgs(... vals: DArgs::StrictListResult))) + rule bestViable(T::CPPType, envEntry(... base: Base::SymBase, defaultArgs: defArgsResult(... vals: DArgs::StrictListResult))) ~> #resolveOverload2(cSet(... id: X::QualId), list(Args::List), _, _, E::Expr, _) => #if isMethodPure(T) andBool isVirtualCall(hasTrace(E), T) #then .K #else Odr.newUse(Base) #fi ~> updateExternalUses(Base) diff --git a/semantics/cpp/language/translation/syntax.k b/semantics/cpp/language/translation/syntax.k index f2d97ad9a..90f3a038e 100644 --- a/semantics/cpp/language/translation/syntax.k +++ b/semantics/cpp/language/translation/syntax.k @@ -50,9 +50,9 @@ module CPP-ABSTRACT-SYNTAX | ConstructorMember(CId, Init) [symbol] | ConstructorDelegating(Init) [symbol] - syntax Declarator ::= FunctionDefinition(NNS, CId, CId, AType, List, AStmt) [strict(4), symbol] - | FunctionDecl(NNS, CId, CId, AType, List) [strict(4), symbol] - | VarDecl(NNS, CId, CId, AType, Init, isDirect: Bool) [strict(4), symbol] + syntax Declarator ::= FunctionDefinition(NNS, CId, CId, AType, List, Stmt) [symbol] + | FunctionDecl(NNS, CId, CId, AType, List) [symbol] + | VarDecl(NNS, CId, CId, AType, Init, isDirect: Bool) [symbol] | FieldDecl(NNS, CId, AType, Init) [strict(3), symbol] | BitFieldDecl(NNS, CId, AType, Expr) [strict(3), symbol] @@ -93,8 +93,7 @@ module CPP-ABSTRACT-SYNTAX | UsingDecl(Bool, NNS, CId) [symbol] | UsingDirective(CId, NNS) [symbol] - syntax Decl ::= DeclLoc(CabsLoc, Decl) [symbol] - | NoDecl() [symbol] + syntax Decl ::= NoDecl() [symbol] syntax BaseSpecifier ::= BaseClass(Bool, Bool, AccessSpecifier, AType) [symbol] diff --git a/semantics/cpp/language/translation/typing/expr.k b/semantics/cpp/language/translation/typing/expr.k index 254e9d9d7..225c88e1b 100644 --- a/semantics/cpp/language/translation/typing/expr.k +++ b/semantics/cpp/language/translation/typing/expr.k @@ -61,7 +61,7 @@ module CPP-TRANSLATION-TYPING-EXPR rule ofSTypeList(K:KItem types:: L::STypeList) => ListItem(K) ofSTypeList(L) [owise] - rule (ExprLoc(_, BraceInit(L::List)) => BraceInit(L)) types:: _ + rule (BraceInitLoc(_, BraceInit(L::List)) => BraceInit(L)) types:: _ rule (.K => types(list(L))) ~> BraceInit(L::List) types:: _ diff --git a/semantics/cpp/language/translation/value-category.k b/semantics/cpp/language/translation/value-category.k index 90c420626..d7d9ad96a 100644 --- a/semantics/cpp/language/translation/value-category.k +++ b/semantics/cpp/language/translation/value-category.k @@ -56,7 +56,7 @@ module CPP-TRANSLATION-VALUE-CATEGORY rule ofSCatList(K:KItem cats:: L::SCatList) => ListItem(K) ofSCatList(L) [owise] - rule (ExprLoc(_, BraceInit(L::List)) => BraceInit(L)) cats:: _ + rule (BraceInitLoc(_, BraceInit(L::List)) => BraceInit(L)) cats:: _ rule (.K => cats(list(L))) ~> BraceInit(L::List) cats:: _