Skip to content

Commit 80fbf37

Browse files
committed
Remove some errors, add some tests.
1 parent 892e4a4 commit 80fbf37

File tree

6 files changed

+15
-29
lines changed

6 files changed

+15
-29
lines changed

semantics/language/execution/expr/function-call.k

-29
Original file line numberDiff line numberDiff line change
@@ -204,33 +204,4 @@ module C-EXPR-FUNCTION-CALL
204204
rule _:KResult := tv(_:CValue, T:Type => stripConstants(T))
205205
requires fromConstantExpr(T)
206206

207-
rule (.K => CV("EFNC2", "incompatible types in function call arguments.", "6.5.16.1:1"))
208-
~> L:KResult := R:RValue
209-
requires type(L) =/=Type type(R) andBool ((isPointerType(type(L)) andBool notBool isPointerType(type(R))
210-
andBool notBool isNullPointerConstant(R))
211-
orBool (isArithmeticType(type(L)) andBool notBool isBoolType(type(L)))
212-
andBool notBool isArithmeticType(type(R))
213-
orBool isStructOrUnionType(type(L))
214-
andBool notBool areCompatible(stripQualifiers(type(L)), type(R))
215-
orBool isBoolType(type(L)) andBool notBool isPointerType(type(R)) andBool notBool isArithmeticType(type(R))
216-
orBool notBool (isPointerType(type(L))
217-
orBool isArithmeticType(type(L))
218-
orBool isStructOrUnionType(type(L))
219-
orBool isBoolType(type(L))))
220-
[structural] //TODO(dwightguth): this tag is needed for confluence with null pointer constants. Might want to find a better way.
221-
222-
rule (.K => CV("EFNC3", "incompatible pointer types in function call arguments.", "6.5.16.1:1"))
223-
~> L:KResult := R:RValue
224-
requires (isPointerType(type(L)) andBool isPointerType(type(R)))
225-
andBool notBool isVoidType(innerType(type(L)))
226-
andBool notBool isVoidType(innerType(type(R)))
227-
andBool (
228-
notBool areCompatible(
229-
stripQualifiers(stripAlignas(innerType(type(L)))),
230-
stripQualifiers(stripAlignas(innerType(type(R)))))
231-
orBool notBool (getQualifiers(innerType(type(R)))
232-
<=Set getQualifiers(innerType(type(L))))
233-
orBool getAlignas(innerType(type(L)))
234-
>Int getAlignas(innerType(type(R)))
235-
)
236207
endmodule
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
File: dup_params2.c
2+
Line: 1
3+
Error: CV-TDL4
4+
Description: redeclaration of x with no linkage.
5+
Type: Constraint violation.
6+
See also: C11 sec. 6.7:3
7+
Translation failed. Run kcc -d dup_params2.c to see commands run.
File renamed without changes.

tests/unit-fail/j039d-link1.ref

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
Error: UB-CB1
2+
Description: types of function call arguments aren't compatible with declared types after promotions.
3+
Type: Undefined behavior.
4+
See also: C11 sec. 6.5.2.2:6, J.2:1 item 39
5+
at foo(j039d-link1.c:4)
6+
at main(j039d-link1.c:4)
7+
at <file-scope>(<unknown>)
8+
Execution failed (configuration dumped)
File renamed without changes.

0 commit comments

Comments
 (0)