Skip to content

Commit 1ade876

Browse files
chathhornh0nzZik
chathhorn
authored and
h0nzZik
committed
A few MISRA-related checks (#588)
* A few UB and lint checks. * Distinguish signed-int from int (for bitfields). * Updating tests and OS test exclusions. * Minor conversion refactor. * More signed-int fixes. * Cast ptr to int: Impl behavior intead of lint. * Update test expected output. * Update test expected output. * More expected-output fixes. * Update tests. * Remove duplicate test. * j055e.c.ref: Update test expected output. * Update test expected output.
1 parent 64b9501 commit 1ade876

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

57 files changed

+239
-90
lines changed

‎examples/c/error-codes/Error_Codes.csv

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -220,6 +220,7 @@ CV-CTI3,The width of a bit field shall be an integer constant expression.,6.7.2.
220220
CV-CTI5,Structs containing a flexible array member must not be array elements.,6.7.2.1:2,Constraint Violation,
221221
IMPL-CCV2,Conversion to signed integer outside the range that can be represented.,"6.3.1.3:3, J.3.5:1 item 4",Implementation Defined Behavior,
222222
IMPL-CCV13,Conversion from an integer to non-null pointer.,"6.3.2.3:5",Implementation Defined Behavior,
223+
IMPL-CCVE4,Casting a pointer to an integer.,"6.3.2.3:6",Implementation Defined Behavior,
223224
IMPL-CEB8,The left operand in a bitwise right-shift is negative.,"6.5.7:5, J.3.5:1 item 5",Implementation Defined Behavior,
224225
IMPL-CEMX4,Modulus operator with a pointer value as an argument.,"6.3.2.3:6, J.3.7:1 item 1",Implementation Defined Behavior,
225226
IMPL-CTI4,"Bit-field with type other than signed int, unsigned int, or _Bool.","6.7.2.1:5, J.3.9:1 item 2",Implementation Defined Behavior,
@@ -230,6 +231,7 @@ IMPLUB-CEMX5,Division by an implementation-defined or unspecified value.,"6.5.5:
230231
IMPLUB-CEMX6,Modulus by an implementation-defined or unspecified value.,"6.5.5:5, J.2:1 item 45",Implementation-dependent undefined Behavior,
231232
UB-PTHREAD99,Unimplemented pthread function.,POSIX 2008,Implementation Defined Behavior,
232233
L-PTHREAD9,Terminating a thread while holding lock on mutexes.,,Possible unintended behavior,X
234+
L-RESTRICT1,Use of the restrict qualifier (a possible source of undefined behavior).,,Possible unintended behavior,X
233235
L-STDLIBE1,Called free() on a null pointer.,,Possible unintended behavior,X
234236
L-STDLIBE2,"Malloc overflows memory bound, returning null pointer.",,Possible unintended behavior,X
235237
L-STDLIBE3,"Realloc overflows memory bound, returning null pointer.",,Possible unintended behavior,X
@@ -240,6 +242,7 @@ L-CEIE2,File opened but never closed.,,Possible unintended behavior,X
240242
L-CER7,Dereferencing a native pointer.,,Possible unintended behavior,X
241243
L-CCVE1,Unsigned integer overflow.,,Possible unintended behavior,X
242244
L-CCVE2,Conversion to unsigned integer outside the range that can be represented.,,Possible unintended behavior,X
245+
L-CCVE3,Casting away qualifiers.,,Possible unintended behavior,X
243246
L-CMRE1,Reading a struct or union with uninitialized parts.,,Possible unintended behavior,X
244247
L-EFNCE1,"Stack might overflow specified bound on some compilers or ABIs.",,Possible unintended behavior,X
245248
L-EFNC3,"Recursive call to the function .",,Possible unintended behavior,X

‎examples/c/error-codes/implementation-defined/IMPL-CCVE4-bad.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
#include <stdint.h>
2+
3+
int main() {
4+
int p = 0;
5+
6+
(uintptr_t) &p;
7+
}

‎examples/c/error-codes/implementation-defined/IMPL-CCVE4-bad.output

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
Casting a pointer to an integer:
2+
> in main at IMPL-CCVE4-bad.c:6:7
3+
4+
Implementation defined behavior (IMPL-CCVE4):
5+
see C11 section 6.3.2.3:6 http://rvdoc.org/C11/6.3.2.3
6+
see MISRA-C section 8.11:4 http://rvdoc.org/MISRA-C/8.11
7+

‎examples/c/error-codes/implementation-defined/IMPL-CCVE4-good.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
#include <stdint.h>
2+
3+
int main() {
4+
int p = 0;
5+
6+
(uintptr_t) p;
7+
}

‎examples/c/error-codes/implementation-defined/IMPL-CEMX4-bad.output

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,10 @@
1+
Casting a pointer to an integer:
2+
> in main at IMPL-CEMX4-bad.c:5:7
3+
4+
Implementation defined behavior (IMPL-CCVE4):
5+
see C11 section 6.3.2.3:6 http://rvdoc.org/C11/6.3.2.3
6+
see MISRA-C section 8.11:4 http://rvdoc.org/MISRA-C/8.11
7+
18
Modulus operator with a pointer value as an argument:
29
> in main at IMPL-CEMX4-bad.c:5:7
310

‎examples/c/error-codes/lint/L-CCVE3-bad.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
int main() {
2+
const int * p = (void *) 0;
3+
(int *) p;
4+
}

‎examples/c/error-codes/lint/L-CCVE3-bad.output

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
Casting away qualifiers:
2+
> in main at L-CCVE3-bad.c:3:7
3+
4+
Possible unintended behavior (L-CCVE3):
5+
see CERT-C section EXP05-C http://rvdoc.org/CERT-C/EXP05-C
6+
see MISRA-C section 8.11:8 http://rvdoc.org/MISRA-C/8.11
7+

‎examples/c/error-codes/lint/L-CCVE3-good.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
int main() {
2+
const int * p = (void *)0;
3+
(const int *) p;
4+
}

‎examples/c/error-codes/lint/L-RESTRICT1-bad-static.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
int main() {
2+
int * restrict p;
3+
}

‎examples/c/error-codes/lint/L-RESTRICT1-bad-static.output

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
L-RESTRICT1-bad-static.c:2:7: warning: Use of the restrict qualifier (a possible source of undefined behavior).
2+
3+
Possible unintended behavior (L-RESTRICT1):
4+
see MISRA-C section 8.8:14 http://rvdoc.org/MISRA-C/8.8
5+

‎examples/c/error-codes/lint/L-RESTRICT1-bad.output

Whitespace-only changes.

‎examples/c/error-codes/lint/L-RESTRICT1-good.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
int main() {
2+
int * p;
3+
}

‎examples/c/error-codes/undefined/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ CHECK_RESULT_COMPILE = if [ $$? -eq 0 ] ; then echo "passed $<"; mv $@.tmp.out $
88
CHECK_RESULT_RUN = if [ $$? -eq 0 ] ; then echo "passed $<"; mv $@.tmp $@; else echo "failed $<"; cat $@.tmp; exit 1; fi
99

1010
KCC = kcc
11-
KCCFLAGS = -frecover-all-errors -fno-native-compilation -fno-diagnostics-color
11+
KCCFLAGS = -frecover-all-errors -fno-native-compilation -fno-diagnostics-color -Wno-implementation-defined
1212
CFLAGS = -fno-diagnostics-color -std=c11
1313

1414
.PHONY: clean comparison

‎examples/c/error-codes/undefined/UB-TEOFF1-bad-static.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
#include <stddef.h>
22
int main(void) {
3-
struct s { int m : 5; };
3+
struct s { signed int m : 5; };
44
return offsetof(struct s, m);
55
}

‎examples/c/error-codes/violates-constraint/nonfatal/CV-CDT5-bad-static.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
struct s {
2-
int a : 8;
3-
int b : 0;
2+
signed int a : 8;
3+
signed int b : 0;
44
};
55

66
struct s x[1] = {{0, 0}};

‎semantics/c/language/common/alignment.k

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ module C-ALIGNMENT
3434
rule byteAlignofType'(t(_, _, _:SimpleSignedCharType)) => cfg:alignofSignedChar
3535
rule byteAlignofType'(t(_, _, short-int)) => cfg:alignofShortInt
3636
rule byteAlignofType'(t(_, _, int)) => cfg:alignofInt
37+
rule byteAlignofType'(t(_, _, signed-int)) => cfg:alignofInt
3738
rule byteAlignofType'(t(_, _, long-int)) => cfg:alignofLongInt
3839
rule byteAlignofType'(t(_, _, long-long-int)) => cfg:alignofLongLongInt
3940
rule byteAlignofType'(t(_, _, oversized-int)) => cfg:alignofOversizedInt

‎semantics/c/language/common/conversion.k

Lines changed: 27 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -280,7 +280,8 @@ module C-CONVERSION
280280
need not be in the range of values of any integer type.
281281
}*/
282282
rule cast(integerUType #as T'::UType, tv(V::CValue, ut(... st: pointerType(_)) #as T::UType))
283-
=> checkUse(tv(cfg:pointerToInt(V, T'), castTypes(T', T)))
283+
=> implPointerToInt()
284+
~> checkUse(tv(cfg:pointerToInt(V, T'), castTypes(T', T)))
284285
requires notBool isBoolUType(T')
285286
andBool (byteSizeofType(T) <=Int byteSizeofType(T')
286287
orBool (V ==K NullPointer))
@@ -293,6 +294,9 @@ module C-CONVERSION
293294
andBool byteSizeofType(T) >Int byteSizeofType(T')
294295
[structural]
295296

297+
rule (.K => IMPL("CCVE4", "Casting a pointer to an integer."))
298+
~> implPointerToInt()
299+
296300
syntax Bool ::= isAbsolute(CValue) [function]
297301
rule isAbsolute(_) => false [owise]
298302

@@ -328,18 +332,34 @@ module C-CONVERSION
328332
}*/
329333
rule cast(ut(Mods'::Set, pointerType(T'::Type)), tv(Loc:SymLoc, ut(Mods::Set, pointerType(T::Type))))
330334
=> adjustPointerBounds(tv(Loc, castTypes(ut(Mods', pointerType(T')), ut(Mods, pointerType(T)))))
331-
requires Loc =/=K NullPointer andBool (notBool isCompleteType(T')
332-
orBool type(pointerType(T')) ==Type type(pointerType(T))
333-
orBool getAlignas(T') <=Int getAlign(Loc)
334-
orBool (isFunctionType(T) andBool isFunctionType(T')))
335+
requires Loc =/=K NullPointer
336+
andBool getAlignas(T') <=Int getAlign(Loc)
337+
andBool notBool (isFunctionType(T) andBool notBool isFunctionType(T'))
338+
andBool getQualifiers(T) <=Quals getQualifiers(T')
335339
//TODO(dwightguth): handle pointer alignment
336340
rule (.K => UNDEF("CCV11",
337341
"Conversion to a pointer type with a stricter alignment requirement (possibly undefined)."))
338342
~> cast(ut(_, pointerType(T'::Type)), tv(Loc:SymLoc, ut(_, pointerType(T::Type))))
339-
requires isCompleteType(T')
340-
andBool type(pointerType(T')) =/=Type type(pointerType(T))
343+
requires T' =/=Type T
344+
andBool notBool (isFunctionType(T) andBool notBool isFunctionType(T'))
341345
andBool getAlignas(T') >Int getAlign(Loc)
342346
[structural]
347+
rule (.K => UNDEF("CCV14",
348+
"Conversion of a function pointer to object pointer type."))
349+
~> cast(ut(_, pointerType(T'::Type)), tv(Loc:SymLoc, ut(_, pointerType(T::Type))))
350+
requires isFunctionType(T) andBool notBool isFunctionType(T')
351+
[structural]
352+
rule (.K => lintCastingAwayQuals())
353+
~> cast(ut(_, pointerType(T'::Type)), tv(Loc:SymLoc, ut(_, pointerType(T::Type => addQualifiers(getQualifiers(T'), stripQualifiers(T))))))
354+
requires getQualifiers(T) >Quals getQualifiers(T')
355+
[structural]
356+
357+
syntax Error ::= lintCastingAwayQuals()
358+
| implPointerToInt()
359+
rule lintCastingAwayQuals() => .K
360+
requires notBool hasLint
361+
rule implPointerToInt() => .K
362+
requires notBool hasLint
343363

344364
syntax UType ::= castTypes(UType, UType) [function]
345365
rule castTypes(ut(_, T'::SimpleUType), ut(Mods::Set, _)) => ut(Mods, T')

‎semantics/c/language/common/promotion.k

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,7 @@ module C-COMMON-PROMOTION
8181
rule rank(ut(_, short-int)) => 2
8282
rule rank(ut(_, unsigned-short-int)) => 2
8383
rule rank(ut(_, int)) => 3
84+
rule rank(ut(_, signed-int)) => 3
8485
rule rank(ut(_, unsigned-int)) => 3
8586
rule rank(ut(_, long-int)) => 4
8687
rule rank(ut(_, unsigned-long-int)) => 4
@@ -121,6 +122,7 @@ module C-COMMON-PROMOTION
121122
// things more convenient if it's total.
122123
rule isPromoted(ut(_, enumType(_))) => true
123124
rule isPromoted(ut(_, int)) => true
125+
rule isPromoted(ut(_, signed-int)) => true
124126
rule isPromoted(ut(_, unsigned-int)) => true
125127
rule isPromoted(ut(_, long-int)) => true
126128
rule isPromoted(ut(_, unsigned-long-int)) => true
@@ -141,7 +143,7 @@ module C-COMMON-PROMOTION
141143

142144
rule promote(ut(Mods::Set, bitfieldType(T::SimpleType, Len::Int)))
143145
=> utype(int)
144-
requires ((T ==K bool) orBool (T ==K int) orBool (T ==K unsigned-int))
146+
requires ((T ==K bool) orBool isSimpleIntType(T) orBool (T ==K unsigned-int))
145147
andBool min(utype(int))
146148
<=Int min(utype(bitfieldType(T, Len)))
147149
andBool max(utype(int))
@@ -157,7 +159,7 @@ module C-COMMON-PROMOTION
157159

158160
rule promote(ut(Mods::Set, bitfieldType(T::SimpleType, Len::Int)))
159161
=> utype(unsigned-int)
160-
requires (T ==K bool orBool T ==K int orBool T ==K unsigned-int)
162+
requires (T ==K bool orBool isSimpleIntType(T) orBool T ==K unsigned-int)
161163
andBool notBool (
162164
min(utype(int))
163165
<=Int min(utype(bitfieldType(T, Len)))

‎semantics/c/language/common/typing.k

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -122,10 +122,11 @@ module C-TYPING-SYNTAX
122122
// Basic types
123123
syntax SimpleBitfieldType ::= bitfieldType(SimpleType, Int)
124124

125-
syntax SimpleSignedType ::= "short-int" | SimpleSignedIntType
125+
syntax SimpleSignedType ::= "short-int" | SimpleIntType
126126
| "long-int" | "long-long-int" | "oversized-int"
127127
syntax SimpleFloatType ::= "float" | "double" | "long-double" | "oversized-float"
128-
syntax SimpleSignedIntType ::= "int"
128+
syntax SimpleIntType ::= "int" | SimpleSignedIntType
129+
syntax SimpleSignedIntType ::= "signed-int"
129130
syntax SimpleUnsignedType ::= SimpleBoolType | "unsigned-short-int"
130131
| SimpleUnsignedIntType | "unsigned-long-int"
131132
| "unsigned-long-long-int"
@@ -220,7 +221,7 @@ module C-TYPING-SYNTAX
220221
rule aggregateOrUnionUType => ut(?_, arrayUType(?_, ?_) #Or incompleteArrayUType(?_) #Or flexibleArrayUType(?_) #Or unspecifiedArrayUType(?_) #Or variableLengthArrayUType(?_, ?_) #Or structType(?_) #Or unionType(?_)) [macro]
221222
rule pointerOrArrayUType => ut(?_, arrayUType(?_, ?_) #Or incompleteArrayUType(?_) #Or flexibleArrayUType(?_) #Or unspecifiedArrayUType(?_) #Or variableLengthArrayUType(?_, ?_) #Or pointerType(?_)) [macro]
222223
rule integerUType => unsignedIntegerUType #Or signedIntegerUType #Or ut(?_, enumType(?_)) [macro]
223-
rule signedIntegerUType => ut(?_, short-int #Or int #Or long-int #Or long-long-int #Or oversized-int #Or signedCharType #Or bitfieldType(short-int #Or int #Or long-int #Or long-long-int #Or oversized-int #Or signedCharType, ?_)) [macro]
224+
rule signedIntegerUType => ut(?_, short-int #Or int #Or signed-int #Or long-int #Or long-long-int #Or oversized-int #Or signedCharType #Or bitfieldType(short-int #Or int #Or signed-int #Or long-int #Or long-long-int #Or oversized-int #Or signedCharType, ?_)) [macro]
224225
rule unsignedIntegerUType => ut(?_, bool #Or unsigned-short-int #Or unsigned-int #Or unsigned-long-int #Or unsigned-long-long-int #Or unsigned-oversized-int #Or unsignedCharType #Or bitfieldType(bool #Or unsigned-short-int #Or unsigned-int #Or unsigned-long-int #Or unsigned-long-long-int #Or unsigned-oversized-int #Or unsignedCharType, ?_)) [macro]
225226
rule charUType => ut(?_, signedCharType #Or unsignedCharType) [macro]
226227
rule arithmeticUType => integerUType #Or ut(?_, float #Or double #Or long-double #Or oversized-float) [macro]
@@ -230,7 +231,7 @@ module C-TYPING-SYNTAX
230231
rule aggregateOrUnionType => t(?_, ?_, arrayType(?_, ?_) #Or incompleteArrayType(?_) #Or flexibleArrayType(?_) #Or unspecifiedArrayType(?_) #Or variableLengthArrayType(?_, ?_) #Or structType(?_) #Or unionType(?_)) [macro]
231232
rule pointerOrArrayType => t(?_, ?_, arrayType(?_, ?_) #Or incompleteArrayType(?_) #Or flexibleArrayType(?_) #Or unspecifiedArrayType(?_) #Or variableLengthArrayType(?_, ?_) #Or pointerType(?_)) [macro]
232233
rule integerType => unsignedIntegerType #Or signedIntegerType #Or t(?_, ?_, enumType(?_)) [macro]
233-
rule signedIntegerType => t(?_, ?_, short-int #Or int #Or long-int #Or long-long-int #Or oversized-int #Or signedCharType #Or bitfieldType(short-int #Or int #Or long-int #Or long-long-int #Or oversized-int #Or signedCharType, ?_)) [macro]
234+
rule signedIntegerType => t(?_, ?_, short-int #Or int #Or signed-int #Or long-int #Or long-long-int #Or oversized-int #Or signedCharType #Or bitfieldType(short-int #Or int #Or signed-int #Or long-int #Or long-long-int #Or oversized-int #Or signedCharType, ?_)) [macro]
234235
rule unsignedIntegerType => t(?_, ?_, bool #Or unsigned-short-int #Or unsigned-int #Or unsigned-long-int #Or unsigned-long-long-int #Or unsigned-oversized-int #Or unsignedCharType #Or bitfieldType(bool #Or unsigned-short-int #Or unsigned-int #Or unsigned-long-int #Or unsigned-long-long-int #Or unsigned-oversized-int #Or unsignedCharType, ?_)) [macro]
235236
rule charType => t(?_, ?_, signedCharType #Or unsignedCharType) [macro]
236237
rule arithmeticType => integerType #Or t(?_, ?_, float #Or double #Or long-double #Or oversized-float) [macro]

‎semantics/c/language/common/typing/common.k

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,7 @@ module C-TYPING-COMMON
7878
rule Qs::Quals -Qual _ => Qs [owise]
7979

8080
rule quals(Qs::Set) <=Quals quals(Qs'::Set) => Qs <=Set Qs'
81+
rule quals(Qs::Set) >Quals quals(Qs'::Set) => notBool (Qs <=Set Qs')
8182

8283
rule quals(Qs::Set) +Quals quals(Qs'::Set) => quals(Qs Qs')
8384

@@ -133,6 +134,7 @@ module C-TYPING-COMMON
133134
rule numBytesArithmetic(_:SimpleSignedCharType) => cfg:sizeofSignedChar
134135
rule numBytesArithmetic(short-int) => cfg:sizeofShortInt
135136
rule numBytesArithmetic(int) => cfg:sizeofInt
137+
rule numBytesArithmetic(signed-int) => cfg:sizeofInt
136138
rule numBytesArithmetic(long-int) => cfg:sizeofLongInt
137139
rule numBytesArithmetic(long-long-int) => cfg:sizeofLongLongInt
138140
rule numBytesArithmetic(oversized-int) => cfg:sizeofOversizedInt
@@ -233,6 +235,7 @@ module C-TYPING-COMMON
233235
rule showTypeSpecifier(signed-char) => "signed char"
234236
rule showTypeSpecifier(short-int) => "short"
235237
rule showTypeSpecifier(int) => "int"
238+
rule showTypeSpecifier(signed-int) => "signed int"
236239
rule showTypeSpecifier(long-int) => "long"
237240
rule showTypeSpecifier(long-long-int) => "long long"
238241
rule showTypeSpecifier(oversized-int) => "__kcc_oversized_int"

‎semantics/c/language/common/typing/compatibility.k

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -60,8 +60,16 @@ module C-TYPING-COMPATIBILITY
6060

6161
syntax Bool ::= #areCompat(Type, Type, Set) [function]
6262
rule #areCompat(
63-
t(Qs::Quals, Mods::Set, T:SimpleBasicType),
64-
t(Qs, Mods'::Set, T), _)
63+
t(Qs::Quals, _, T:SimpleBasicType),
64+
t(Qs , _, T), _)
65+
=> true
66+
rule #areCompat(
67+
t(Qs::Quals, _, signed-int),
68+
t(Qs , _, int), _)
69+
=> true
70+
rule #areCompat(
71+
t(Qs::Quals, _, int),
72+
t(Qs , _, signed-int), _)
6573
=> true
6674

6775
// TODO(chathhorn): should be a setting.

‎semantics/c/language/common/typing/misc.k

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,7 @@ module C-TYPING-MISC
4949
rule flipSignedness(_:SimpleSignedCharType) => unsigned-char
5050
rule flipSignedness(short-int) => unsigned-short-int
5151
rule flipSignedness(int) => unsigned-int
52+
rule flipSignedness(signed-int) => unsigned-int
5253
rule flipSignedness(long-int) => unsigned-long-int
5354
rule flipSignedness(long-long-int) => unsigned-long-long-int
5455
rule flipSignedness(oversized-int) => unsigned-oversized-int

‎semantics/c/language/common/typing/predicates.k

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,7 @@ module C-TYPING-PREDICATES
107107
rule isReadFrom(_) => false [owise]
108108

109109
rule isTruthValue(tv(V::CValue, ut(_, T::SimpleUType)))
110-
=> T ==K int andBool (V ==K 0 orBool V ==K 1)
110+
=> isSimpleIntType(T) andBool (V ==K 0 orBool V ==K 1)
111111

112112
rule isFlexibleType(dynamicType(T::Type)) => isFlexibleType(T)
113113
rule isFlexibleType(t(... st: structType(_)) #as T::Type) => isFlexibleStruct(getFields(T))

‎semantics/c/language/translation/function-def.k

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -119,11 +119,11 @@ module C-FUNCTION-DEF
119119
[structural]
120120
rule (.K => UNDEF("FD5", "Function main must return an int.") )
121121
~> checkMainDef(t(_, _, functionType(ut(_, T::SimpleUType), _)))
122-
requires T =/=K int
122+
requires notBool isSimpleIntType(T)
123123
[structural]
124124
rule (.K => UNDEF("FD6", "If main has parameters, the type of the first parameter must be equivalent to int.") )
125125
~> checkMainDef(t(_, _, functionType(_, ListItem(t(_, _, T::SimpleType)) _)))
126-
requires T =/=K int andBool T =/=K void
126+
requires notBool isSimpleIntType(T) andBool T =/=K void
127127
[structural]
128128
rule (.K => UNDEF("FD7", "If main has parameters, the type of the second parameter must be equivalent to char**.") )
129129
~> checkMainDef(t(_, _, functionType(_, ListItem(_) ListItem(T:Type))))

‎semantics/c/language/translation/literal.k

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,7 @@ module C-LITERAL
1616
rule simplifyForHex(S:String) => simplifyForHex(butFirstChar(S))
1717
requires (firstChar(S) ==String "0")
1818
andBool (lengthString(S) >Int 1)
19-
rule simplifyForHex(S:String) => S
20-
requires (firstChar(S) =/=String "0")
21-
orBool (lengthString(S) ==Int 1)
19+
rule simplifyForHex(S:String) => S [owise]
2220

2321
syntax IntConstant ::= hexOrOctalConstant(Int)
2422
rule HexConstant(S:String)

0 commit comments

Comments
 (0)