Fix include and most unused variable warnings.

Author: Virgil Serbanuta

.build/k

@@ -1,5 +1,5 @@
-require "kast.k"
-require "domains.k"
+require "kast.md"
+require "domains.md"
 
 require "cpp/linking.k"
 

semantics/c-cpp-linking.k

@@ -1,5 +1,5 @@
-require "kast.k"
-require "domains.k"
+require "kast.md"
+require "domains.md"
 
 require "c/language/common/common.k"
 require "c/language/execution/configuration.k"

semantics/c-cpp.k

@@ -1,5 +1,5 @@
-require "kast.k"
-require "domains.k"
+require "kast.md"
+require "domains.md"
 
 require "c/language/common/common.k"
 require "c/language/translation/configuration.k"

semantics/c-translation.k

@@ -78,15 +78,15 @@ module C-BINDING
           ~> bind(.List, _, ListItem(_) _)
      rule (.K => UNDEF("CB4", "Function defined with no parameters "
                +String "called with arguments."))
-          ~> bind(ListItem(typedDeclaration(t(... st: void) #as T::Type, _)), _, ListItem(_) _)
+          ~> bind(ListItem(typedDeclaration(t(... st: void) #as _T::Type, _)), _, ListItem(_) _)
      // Variadic.
      rule bind(ListItem(variadic), ListItem(variadic), Vs:List)
           => bindVariadics(Vs, 0)
           [structural]
      // No params.
      rule bind(ListItem(t(... st: void)), .List, .List) => .K
           [structural]
-     rule bind(ListItem(typedDeclaration(t(... st: void) #as T::Type, _)),
+     rule bind(ListItem(typedDeclaration(t(... st: void) #as _T::Type, _)),
                .List, .List) => .K
           [structural]
      // Builtins -- they don't have named parameters.
@@ -112,8 +112,8 @@ module C-BINDING
           <next-unnamed> N:Int => N +Int 1 </next-unnamed>
           requires T =/=K variadic
           [structural]
-     rule bind(ListItem(t(... st: void) #as T::Type),
-               ListItem(t(... st: void) #as T'::Type), .List) => .K
+     rule bind(ListItem(t(... st: void) #as _T::Type),
+               ListItem(t(... st: void) #as _T'::Type), .List) => .K
           [structural]
      rule bind(.List, .List, .List) => .K
           [structural]

semantics/c/language/common/binding.k

@@ -43,13 +43,13 @@ module C-CHECK-USE
           [structural]
 
      syntax Error ::= "errorLinkUnresolved"
-     rule <k> checkLoc(loc(Base:LinkBase, _))
+     rule <k> checkLoc(loc(_Base:LinkBase, _))
                => EXT-UNDEF("TDR2", "No definition for symbol with external linkage.")
                ~> errorLinkUnresolved
           ...</k>
           requires currentSemantics() ==K ExecutionSemantics()
           [structural]
-     rule <k> checkLoc(loc(Base:LinkBase, _, _))
+     rule <k> checkLoc(loc(_Base:LinkBase, _, _))
                => EXT-UNDEF("TDR2", "No definition for symbol with external linkage.")
                ~> errorLinkUnresolved
           ...</k>

semantics/c/language/common/check-use.k

@@ -78,7 +78,7 @@ module C-CONVERSION
           => tv(V, castTypes(T', T))
           requires T' =/=Type T andBool notBool isBoolUType(T') andBool intInRange(V, T')
 
-     rule cast(integerUType #as T'::UType, tv(encodedPtr(L:SymLoc, N::Int, M::Int), integerUType #as T::UType))
+     rule cast(integerUType #as T'::UType, tv(encodedPtr(L:SymLoc, N::Int, M::Int), integerUType #as _T::UType))
           => tv(encodedPtr(L, N, M), T')
           requires notBool isBoolUType(T')
                andBool M -Int N <=Int bitSizeofType(T')
@@ -272,7 +272,7 @@ module C-CONVERSION
      a trap representation.
      }*/
      rule (.K => IMPL("CCV13", "Conversion from an integer to non-null pointer."))
-          ~> cast(ut(... st: pointerType(_)) #as T'::UType, tv(V:CValue, integerUType #as T::UType))
+          ~> cast(ut(... st: pointerType(_)) #as _T'::UType, tv(V:CValue, integerUType #as T::UType))
           requires notBool isNullPointerConstant(tv(V, T))
 
      /*@ \fromStandard{\source[n1570]{\para{6.3.2.3}{6}}}{
@@ -348,11 +348,11 @@ module C-CONVERSION
           [structural]
      rule (.K => UNDEF("CCV14",
                "Conversion of a function pointer to object pointer type."))
-          ~> cast(ut(_, pointerType(T'::Type)), tv(Loc:SymLoc, ut(_, pointerType(T::Type))))
+          ~> cast(ut(_, pointerType(T'::Type)), tv(_Loc:SymLoc, ut(_, pointerType(T::Type))))
           requires isFunctionType(T) andBool notBool isFunctionType(T')
           [structural]
      rule (.K => lintCastingAwayQuals())
-          ~> cast(ut(_, pointerType(T'::Type)), tv(Loc:SymLoc, ut(_, pointerType(T::Type => addQualifiers(getQualifiers(T'), stripQualifiers(T))))))
+          ~> cast(ut(_, pointerType(T'::Type)), tv(_Loc:SymLoc, ut(_, pointerType(T::Type => addQualifiers(getQualifiers(T'), stripQualifiers(T))))))
           requires getQualifiers(T) >Quals getQualifiers(T')
           [structural]
 

semantics/c/language/common/conversion.k

@@ -169,7 +169,7 @@ module C-COMMON-EXPR-ADDITIVE
           requires ifFromArrayInBounds(Loc, utype(pointerType(type(char))), I) ==K true
      rule (.K => UNDEF("CEA1",
                "A pointer (or array subscript) outside the bounds of an object."))
-          ~> addToIntptr(Loc:SymLoc, T::UType, I:Int)
+          ~> addToIntptr(Loc:SymLoc, _T::UType, I:Int)
           requires notBool ifFromArrayInBounds(Loc, utype(pointerType(type(char))), I)
 
      syntax SymLoc ::= newFromArray(SymLoc, UType, Int) [function]

semantics/c/language/common/expr/additive.k

@@ -59,7 +59,7 @@ module C-COMMON-EXPR-EVAL
           requires notBool isArrayOrFunctionType(T)
           [structural]
 
-     rule <k> lv(Loc::SymLoc => resolveLinking(Loc, Linkings), T::Type) ...</k>
+     rule <k> lv(Loc::SymLoc => resolveLinking(Loc, Linkings), _T::Type) ...</k>
           <linkings> Linkings::Map </linkings>
           requires Loc =/=K NullPointer andBool (base(Loc) in_keys(Linkings))
           [structural]

semantics/c/language/common/expr/eval.k

@@ -61,7 +61,7 @@ module C-COMMON-EXPR-MEMBERS
           requires notBool isNoType(findFieldTypeU(F, T))
           [structural]
      rule (.K => unknownMemberAccess)
-          ~> tv(agg(L:List), structOrUnionUType #as T::UType) . F:CId
+          ~> tv(agg(_L:List), structOrUnionUType #as T::UType) . F:CId
           requires isNoType(findFieldTypeU(F, T))
 
      syntax Type ::= findFieldTypeU(CId, UType) [function]