Relation and equality operators in C have int as return type

[sakehl]

In C relational (<, >, <=, >=) and equality operators actually have resulting type int. It has 0 for false value and 1 for true value. (See Section 6.5.8.6 and 6.5.9.3 of (1)).

E.g. int x = 1 == 0; would yield x=0.

But in VerCors this currently does not type check, as these operators return type bool.

To be more precise the type bool (or actually _Bool) is ranked lower than any integer type (the least precision) (See 6.3.1.1.1 of (1) ).

But _Boolmay be used anywhere, where an int or uint maybe used. (See 6.3.1.1.2 of (1) ).

I think we could support this with custom operators like CEq, CNeq etc which would give back the type CInt. And then fix everything in the the CFloatIntCoercion (and rename that pass).

Furthermore we could add rules in coercion to coerce from TCInt to TBool and vica versa.

Although maybe it would then be better to have the TCBool type? Such that a TBool cannot convert to integer normally, but a TCBool can convert.

Similarly a pointer can be converted to a boolean value in C as well. E.g. int* x = NULL if(!x) return -1 is valid to write.

Anyway I wanted to report this, it does have a big impact I think, but is nice to be complete.

(1) C11 standard: https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1548.pdf

[pieter-bos]

I'd say it's fine if TBool is coercible into TCInt and vice versa (and not TInt), that seems like expected C behaviour as it relates to specification-level expressions that generate booleans (so you can do (\forall ...) == 0 if you really insist)