Integer-to-bool cast
In C, casting integers to booleans are special: 0 is interpreted as false, and non-zero values are interpreted as true. For example:
[[rc::returns("true @ boolean<bool_it>")]]
bool test() {
return 0xFFFF;
}
Because the integer 0xFFFF
is a non-zero value, this function should return the boolean value true
. Currently, the above cannot be verified, as RefinedC asks you to show 0xFFFF ∈ bool_it
and 0xFFFF = 1
(by the integer cast typing rule), which are (both) impossible.
In fact, the above example equals to (or desugar to):
[[rc::returns("true @ boolean<bool_it>")]]
bool test() {
return 0 != 0xFFFF;
}
RefinedC can prove this without additional tactics.
Goal: support integer-to-bool cast in RefinedC, so that examples like this one (original version) can be verified.
Possible solutions:
- Introduce a new operator for integer-to-bool cast, and have its own typing rules, so that we distinguish it with casting integers of different
int_type
s (e.g. castu8
tou16
). - Modify the frontend to generate code that explicitly contains the comparison with 0 (i.e.
0 != ...
in the example).
p.s. see also #35
Edited by Fengmin Zhu