Skip to content

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:

  1. 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_types (e.g. cast u8 to u16).
  2. 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