Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix some unused variable warnings. #645

Open
wants to merge 12 commits into
base: master
Choose a base branch
from
Open

Fix some unused variable warnings. #645

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
29d9693
Fix warnings
Dec 10, 2020
75da1f1
tmp
Dec 10, 2020
6441678
tmp
Dec 10, 2020
46e7b69
Tmp
Dec 14, 2020
388a3bf
tmp
Dec 15, 2020
669377d
tmp
Dec 15, 2020
b1f0100
tmp
Dec 16, 2020
c11f7d3
tmp
Dec 16, 2020
4f30526
tmp
Dec 16, 2020
9cd019b
tmp
Dec 16, 2020
eb6776b
tmp
Dec 16, 2020
0e4924f
tmp
Dec 16, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions semantics/c/language/translation/typing/canonicalization.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ module C-TYPING-CANONICALIZATION
requires cfg:reservedKeywordSupported(Tok)
[structural]
rule (.K => SE("TCANON2","Unsupported reserved identifier "+String Tok +String " (reserved variant of restrict)."))
~> addMods(Mods::List ListItem(RestrictReserved(Tok::String, Loc::CabsLoc)), T:Type)
~> addMods(_Mods::List ListItem(RestrictReserved(Tok::String, _::CabsLoc)), _:Type)
requires notBool cfg:reservedKeywordSupported(Tok)
[structural]
rule addMods(Mods::List ListItem(Restrict()), T:Type)
Expand Down Expand Up @@ -123,7 +123,7 @@ module C-TYPING-CANONICALIZATION
context addMods(_ ListItem(AlignasExpression(HOLE:KItem)), _)
rule addMods(_::List ListItem(AlignasExpression(tv(A:Int, _)) => alignas(A)), _)
[structural]
rule addMods(Mods::List (ListItem(S:KItem) => .List), _:KResult)
rule addMods(_Mods::List (ListItem(S:KItem) => .List), _:KResult)
requires notBool isModifier(S)
andBool notBool isQualifier(S)
andBool notBool isReducibleModifier(S)
Expand Down
6 changes: 3 additions & 3 deletions semantics/c/language/translation/typing/expr.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ module C-TYPING-EXPR
rule typeof(+ T:Type => tryPromote(T))
rule typeof(- T:Type => tryPromote(T))
rule typeof(~ T:Type => tryPromote(T:Type))
rule typeof(! T:Type => type(int))
rule typeof(! _:Type => type(int))

rule typeof(SizeofExpression(T:Type) => SizeofType(T, .K))
rule typeof(SizeofType(T:Type, _)
Expand Down Expand Up @@ -257,10 +257,10 @@ module C-TYPING-EXPR
requires stripQualifiers(T) ==Type stripQualifiers(T')
andBool SizeofExpression(...) :/=K K

rule elaborateDone(V:K, V':K) ~> typeof(_ ? t(...) : (t(...) #as T'::Type))
rule elaborateDone(V:K, _V':K) ~> typeof(_ ? t(...) : (t(...) #as T'::Type))
=> typeof(stripQualifiers(T'))
requires isNPC(V) andBool isPointerType(T')
rule elaborateDone(V:K, V':K) ~> typeof(_ ? (t(...) #as T::Type) : t(...))
rule elaborateDone(_V:K, V':K) ~> typeof(_ ? (t(...) #as T::Type) : t(...))
=> typeof(stripQualifiers(T))
requires isNPC(V') andBool isPointerType(T)

Expand Down
2 changes: 1 addition & 1 deletion semantics/c/language/translation/typing/interpretation.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ module C-TYPING-INTERPRETATION
~> ArrayType(_, tv(_:Float, _), _)
[structural]
rule (.K => CV("CTI2", "Arrays must have positive length."))
~> ArrayType(T:Type, tv(Len:Int, _), _)
~> ArrayType(_:Type, tv(Len:Int, _), _)
requires Len <=Int 0
[structural]
rule (.K => CV("CTI5", "Structs containing a flexible array member must not be array elements."))
Expand Down
8 changes: 4 additions & 4 deletions semantics/common/bits.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,11 +84,11 @@ module BITS
[owise]

syntax Bool ::= piecesJoinable(Bits, Bits) [function]
rule piecesJoinable(piece(N:Int, _), piece(N':Int, _)) => true
rule piecesJoinable(piece(unknown(N:Int), _), piece(unknown(N':Int), _)) => true
rule piecesJoinable(piece(_N:Int, _), piece(_N':Int, _)) => true
rule piecesJoinable(piece(unknown(_N:Int), _), piece(unknown(_N':Int), _)) => true
rule piecesJoinable(piece(trap, _), piece(trap, _)) => true
rule piecesJoinable(piece(encodedPtr(N::PtrValue, From::Int, To::Int), _), piece(encodedPtr(N, To, _), _)) => true
rule piecesJoinable(piece(encodedValue(N::EncodableValue, From::Int, To::Int), _), piece(encodedValue(N, To, _), _)) => true
rule piecesJoinable(piece(encodedPtr(N::PtrValue, _From::Int, To::Int), _), piece(encodedPtr(N, To, _), _)) => true
rule piecesJoinable(piece(encodedValue(N::EncodableValue, _From::Int, To::Int), _), piece(encodedValue(N, To, _), _)) => true
rule piecesJoinable(_, _) => false [owise]

syntax Bits ::= joinPieces(Bits, Bits) [function]
Expand Down
2 changes: 1 addition & 1 deletion semantics/common/compat.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ module COMPAT-KAST [kast]
imports BOOL
imports K-EQUAL

rule some(.Map::Map, Lbl:K) => false
rule some(.Map::Map, _Lbl:K) => false
rule some(K1:KItem |-> K2:KItem M::Map, #klabel(Lbl:KLabel)) => Lbl(K1, K2) orBool some(M, #klabel(Lbl)) [owise]

rule mapList(ListItem(K:KItem) L:List, #klabel(Lbl:KLabel)) => ListItem(Lbl(K)) mapList(L, #klabel(Lbl))
Expand Down
2 changes: 1 addition & 1 deletion semantics/common/symloc.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -288,7 +288,7 @@ module SYMLOC
rule stripFromArray(Loc:SymLoc) => Loc [owise]

rule getFromArray(loc(_, _, SetItem(fromArray(...) #as F::Provenance) _)) => F
rule getFromArray(Loc::SymLoc) => .K [owise]
rule getFromArray(_::SymLoc) => .K [owise]

rule stripProv(loc(Base:SymBase, Offset:Int, _)) => loc(Base, Offset)
rule stripProv(loc(Base:SymBase, Offset:Int)) => loc(Base, Offset)
Expand Down
16 changes: 8 additions & 8 deletions semantics/cpp/language/translation/decl/class.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1196,7 +1196,7 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)]
<class-id> C </class-id>
<class-type> Key::ClassKey </class-type>
<cenv> CE::Map => CE[X, T <- classOffset(NaOffset, Offset)] </cenv>
<dsize> V::Int => Offset +Int #if isBaseClass(X) #then nvSizeof(T) #else bitSizeofType(T) #fi </dsize>
<dsize> _::Int => Offset +Int #if isBaseClass(X) #then nvSizeof(T) #else bitSizeofType(T) #fi </dsize>
<align> M::Int => maxInt(M, #if isBaseClass(X) #then nvAlignof(T) #else byteAlignofType(T) #fi) </align>
<sizeof> V2::Int => maxInt(V2, Offset +Int #if isBaseClass(X) #then nvSizeof(T) #else bitSizeofType(T) #fi) </sizeof>
...</class>
Expand Down Expand Up @@ -1271,11 +1271,11 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)]
rule getTypesAtOffsetForLayout(t(... st: classType(_ :: Class(Union(), _, _))) #as T::CPPType, 0)
=> SetItem(utype(T)) getTypesAtOffsetForLayoutInUnion(T, getClassInfo(T), 0)

rule getTypesAtOffsetForLayout(t(... st: arrayType(InnerT::CPPType, _)) #as T::CPPType, Offset::Int)
rule getTypesAtOffsetForLayout(t(... st: arrayType(InnerT::CPPType, _)) #as _::CPPType, Offset::Int)
=> getTypesAtOffsetForLayout(InnerT, Offset %Int bitSizeofType(InnerT))
requires Offset >Int 0

rule getTypesAtOffsetForLayout(t(... st: incompleteArrayType(InnerT::CPPType)) #as T::CPPType, Offset::Int)
rule getTypesAtOffsetForLayout(t(... st: incompleteArrayType(InnerT::CPPType)) #as _::CPPType, Offset::Int)
=> getTypesAtOffsetForLayout(InnerT, Offset %Int bitSizeofType(InnerT))
requires Offset >Int 0

Expand Down Expand Up @@ -1305,9 +1305,9 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)]
rule getTypesAtOffsetForLayoutInStruct(_, <class>...
<non-static-data-members>... ListItem(Class.DataMember(X::CId, T::CPPType)) => .List </non-static-data-members>
<cenv>... X |-> (_::Map stripType(T) |-> (_, uninitialized)) ...</cenv>
...</class>, Offset::Int)
...</class>, _Offset::Int)

rule getTypesAtOffsetForLayoutInStruct(T::CPPType, <class>...
rule getTypesAtOffsetForLayoutInStruct(_::CPPType, <class>...
<non-static-data-members>... ListItem(Class.DataMember(X::CId, T'::CPPType)) </non-static-data-members>
<cenv>... X |-> (_::Map stripType(T') |-> (_, classOffset(_, FOffset::Int))) ...</cenv>
...</class>, Offset::Int)
Expand All @@ -1318,18 +1318,18 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)]
<base-classes>... ListItem(C:Class) => ListItem(type(classType(C))) </base-classes>
...</class>, _)

rule getTypesAtOffsetForLayoutInStruct(T::CPPType, <class>...
rule getTypesAtOffsetForLayoutInStruct(_::CPPType, <class>...
<base-classes>... ListItem(t(... st: classType(C::Class)) #as T'::CPPType) => .List </base-classes>
<non-static-data-members> .List </non-static-data-members>
<cenv>... baseClass(C) |-> (_::Map stripType(T') |-> (_, classOffset(_, FOffset::Int))) ...</cenv>
...</class>, Offset::Int)
requires FOffset >Int Offset

rule getTypesAtOffsetForLayoutInStruct(T::CPPType, <class>...
rule getTypesAtOffsetForLayoutInStruct(_::CPPType, <class>...
<base-classes>... ListItem(t(... st: classType(C::Class)) #as T'::CPPType) => .List </base-classes>
<non-static-data-members> .List </non-static-data-members>
<cenv>... baseClass(C) |-> (_::Map stripType(T') |-> (_, uninitialized)) ...</cenv>
...</class>, Offset::Int)
...</class>, _Offset::Int)

rule getTypesAtOffsetForLayoutInStruct(T::CPPType, <class>...
<base-classes>... ListItem(t(... st: classType(C::Class)) #as T'::CPPType) </base-classes>
Expand Down
25 changes: 12 additions & 13 deletions semantics/cpp/language/translation/decl/declarator.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
rule getPreviousLinkage(_, _, _, _) => .K [owise]

// @ref n4296 3.5:3.1
rule getLinkage(S::Set, _, _:NamespaceScope, Q::Quals, _, _) => InternalLinkage
rule getLinkage(S::Set, _, _:NamespaceScope, _::Quals, _, _) => InternalLinkage
requires Static() in S

// @ref n4296 3.5:3.2
Expand All @@ -140,7 +140,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
requires Static() in S
orBool isFunctionDeclarationType(Type)

rule getLinkage(_, C:Class, _, _, L:Linkage, _) => L
rule getLinkage(_, _:Class, _, _, L:Linkage, _) => L

// @ref n4296 3.5:4
rule getClassLinkage(Parent:Namespace :: _) => getNamespaceLinkage(Parent)
Expand All @@ -151,7 +151,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
rule getClassLinkage(_:LocalQualifier :: _) => NoLinkage

// @ref n4296 3.5:4
rule getNamespaceLinkage(N:UnnamedNamespace) => InternalLinkage
rule getNamespaceLinkage(_:UnnamedNamespace) => InternalLinkage

rule getNamespaceLinkage(GlobalNamespace()) => ExternalLinkage

Expand All @@ -173,7 +173,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
rule getDuration(S::Set, _) => ThreadStorage
requires ThreadLocal() in S

rule getDuration(S::Set, Scope:BlockScope) => AutoStorage
rule getDuration(S::Set, _:BlockScope) => AutoStorage
requires notBool Static() in S andBool notBool Extern() in S

rule getDuration(_, _) => StaticStorage [owise]
Expand All @@ -199,9 +199,9 @@ module CPP-TRANSLATION-DECL-DECLARATOR

syntax CId ::= getCName(CPPType, CId, CId, LanguageLinkage, Set) [function]

rule getCName(T::CPPType, X::CId, _, CLinkage, _) => X
rule getCName(_::CPPType, X::CId, _, CLinkage, _) => X

rule getCName(t(... st: functionType(...)) #as T::CPPType, X::CId, Mangled::CId, LangLinkage::LanguageLinkage, Opts::Set) => Mangled
rule getCName(t(... st: functionType(...)) #as _::CPPType, X::CId, Mangled::CId, LangLinkage::LanguageLinkage, Opts::Set) => Mangled
requires (LangLinkage =/=K CLinkage) andBool (X =/=K Mangled)
andBool notBool (NoNativeFallback() in Opts)

Expand Down Expand Up @@ -277,10 +277,10 @@ module CPP-TRANSLATION-DECL-DECLARATOR
~> lazyDefineObject(N, X, CName, T, Init, Type, S, Base)

// ExternalLinkage, StaticStorage, redeclare incomplete array
rule <k> declareObjectWithLinkage(N::Namespace, LN::Namespace, X::CId, t(... st: _:CPPSimpleArrayType) #as T::CPPType, Init::Init, Type::DeclarationType, StaticStorage, S::Set, _, ExternalLinkage) ...</k>
rule <k> declareObjectWithLinkage(_::Namespace, LN::Namespace, X::CId, t(... st: _:CPPSimpleArrayType) #as T::CPPType, _::Init, _::DeclarationType, StaticStorage, _::Set, _, ExternalLinkage) ...</k>
<curr-tr-tu> Tu::String </curr-tr-tu>
<tu-id> Tu </tu-id>
<externals>... LN :: X |-> ((_::CPPType => stripType(T)) |-> (T'::CPPType => T, declState(Base::SymBase, _))) ...</externals>
<externals>... LN :: X |-> ((_::CPPType => stripType(T)) |-> (T'::CPPType => T, declState(_::SymBase, _))) ...</externals>
requires isCPPArrayType(T') andBool notBool isCompleteType(T') andBool innerType(T) ==Type innerType(T') andBool getQuals(T) ==K getQuals(T')

// ExternalLinkage, StaticStorage, redeclare complete type
Expand Down Expand Up @@ -417,7 +417,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR

syntax CPPType ::= completeDeclaration(CPPType, Init) [function]

rule completeDeclaration(T::CPPType, (ExprLoc(_, I:Init) => I))
rule completeDeclaration(_::CPPType, (ExprLoc(_, 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))
Expand Down Expand Up @@ -478,7 +478,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR

syntax Decl ::= lazyDefineObject(NNSVal, CId, CId, CPPType, Init, DeclarationType, Set, SymBase)

rule lazyDefineObject(N::NNSVal, X::CId, CName::CId, T::CPPType, Init::Init, Type::DeclarationType, S::Set, Base::SymBase)
rule lazyDefineObject(N::NNSVal, X::CId, CName::CId, T::CPPType, Init::Init, Type::DeclarationType, S::Set, _::SymBase)
=> defineObject(N, X, CName, T, Init, Type, S)
requires notBool isInitOnlyIfOdrUsed(Init)

Expand All @@ -492,8 +492,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
scope(namespaceScope(GlobalNamespace()), clearScope() ~> defineObject(N, X, CName, T, Init, Type, S))
)
...</k>
<curr-tr-scope> Sc::Scope </curr-tr-scope>

<curr-tr-scope> _::Scope </curr-tr-scope>

rule defineObject(_, _, _, _, NoInit(), Function(_), _) => .K

Expand Down Expand Up @@ -539,7 +538,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR

syntax Decl ::= defineLocalStaticObject(CId, SymBase, CPPType, Init, DeclarationType, Set)

rule defineLocalStaticObject(X::CId, Base::SymBase, T::CPPType, Init::Init, Var(Type::InitType), S::Set)
rule defineLocalStaticObject(X::CId, Base::SymBase, T::CPPType, Init::Init, Var(Type::InitType), _::Set)
=> addToEnv(NoNamespace() :: X, T, Base, false)
~> Odr.newDef(NoNamespace() :: X, T, Base)
~> Odr.newDecl(#NoName, NoNamespace() :: X, T, Base)
Expand Down
10 changes: 5 additions & 5 deletions semantics/cpp/language/translation/decl/enum.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ module CPP-TRANSLATION-DECL-ENUM

syntax KItem ::= enumContext(CId, CPPType, List, fixed: Bool, ut: CPPType, opaque: Bool)

rule enumContext(X::CId, E::CPPType, Enumerators:List, Fixed::Bool, UT::CPPType, Opaque:Bool)
rule enumContext(X::CId, E::CPPType, Enumerators:List, Fixed::Bool, _UT::CPPType, Opaque:Bool)
=> newEnum(getEnumId(E), E, Fixed, Opaque)
~> addEnumToEnv(X, E)
~> #if Opaque #then .K #else inEnumScope(E, declareEnumerators(E, 0, 0, 0, int, Enumerators, Fixed, true)) #fi
Expand Down Expand Up @@ -178,13 +178,13 @@ module CPP-TRANSLATION-DECL-ENUM
// Type of an enumerator inside the declaration is enum's underlying type
// if it is fixed, and type of initializing expression otherwise,
// Hence we need to store the type of underlying expression...
rule declareEnumerators(T::CPPType, Min::Int, Max::Int, Next::Int, _, ListItem(Enumerator(X::CId, prv(V::Int, _, t(_, _, EType:CPPSimpleType)) #as Pr::PRVal)) L::List, Fixed:Bool, First:Bool)
rule declareEnumerators(T::CPPType, Min::Int, Max::Int, _Next::Int, _, ListItem(Enumerator(X::CId, prv(V::Int, _, t(_, _, EType:CPPSimpleType)) #as Pr::PRVal)) L::List, Fixed:Bool, First:Bool)
=> declareEnumerator(getEnumId(T), X, Pr, Fixed, underlyingType(T))
~> declareEnumerators(T, #if First #then V #else minInt(Min, V) #fi, #if First #then V #else maxInt(Max, V) #fi, V +Int 1, EType, L, Fixed, false)
requires notBool isCPPSimpleUnscopedEnumType(EType)

// Enums with fixed underlying type are finished by now.
rule declareEnumerators(T::CPPType, _, _, _, _, .List, true, _) => .
rule declareEnumerators(_::CPPType, _, _, _, _, .List, true, _) => .

rule declareEnumerators(T::CPPType, Min::Int, Max::Int, _, _, .List, false, _) => calculateEnumValues(T, Min, Max)

Expand Down Expand Up @@ -302,7 +302,7 @@ module CPP-TRANSLATION-DECL-ENUM

syntax SetEnumMinMaxUt ::= setEnumMinMaxUt(CPPType, min: Int, max: Int, ut: CPPType)

rule <k> setEnumMinMaxUt(t(_, _, unscopedEnum(_ :: Enum(X::CId) #as E::Enum, _, Fixed:Bool)) #as T::CPPType, Min::Int, Max::Int, cppIntegerType #as UT::CPPType)
rule <k> setEnumMinMaxUt(t(_, _, unscopedEnum(_ :: Enum(X::CId) #as E::Enum, _, Fixed:Bool)) #as _::CPPType, Min::Int, Max::Int, cppIntegerType #as UT::CPPType)
=> addEnumToEnv(X, t(noQuals, .Set, unscopedEnum(E, UT, Fixed))) ... </k>
<enum-id> E </enum-id>
<enum-type> _ => t(noQuals, .Set, unscopedEnum(E, UT, Fixed)) </enum-type>
Expand All @@ -312,7 +312,7 @@ module CPP-TRANSLATION-DECL-ENUM


// @ref n4296 7.2/3: ... An opaque-enum-declaration is either a redeclaration of an enumeration in the current scope...
rule <k> OpaqueEnumDeclaration(X::CId, Scoped::Bool, UT::CPPType) => . ...</k>
rule <k> OpaqueEnumDeclaration(X::CId, _Scoped::Bool, _UT::CPPType) => . ...</k>
<curr-tr-scope> namespaceScope(N::Namespace) </curr-tr-scope>
<enum-id> N::Namespace :: Enum(X) </enum-id>

Expand Down
Loading