C front-end: hide our use of single-bit bool within sizeof

[tautschnig]

In C, Boolean operations are of type int. Rejecting sizeof expressions
of Boolean operations breaks building the Linux kernel.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #5723 (5f86851) into develop (111b51e) will not change coverage.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #5723   +/-   ##
========================================
  Coverage    73.55%   73.55%           
========================================
  Files         1431     1431           
  Lines       155248   155248           
========================================
  Hits        114189   114189           
  Misses       41059    41059           

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_expr.cpp	74.98% <100.00%> (+0.03%)	⬆️
src/ansi-c/parser.y	77.77% <100.00%> (-0.07%)	⬇️
src/ansi-c/scanner.l	61.63% <100.00%> (+0.03%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 276b8d7...5f86851. Read the comment docs.

[martin-cs]

Wasn't this why there was a distinction between bool and c_bool. I thought they were 1 bit and 8 bit respectively and C defaulted to generating c_bool with __CPROVER_bool needed to generate actual ID_bool. Perhaps I have got very confused.

[kroening]

I would probably drop the check of the operator.
Say ?: is missing.

[tautschnig]

There's ID_if in the above, but I agree this could easily be missing some other operator. When writing this code I was wondering whether to just always cast, or whether some cases should be considered illformed input and be rejected by the type checker?

[kroening]

I think it's the right thing to always use int whenever "proper bool" is encountered in sizeof.

[tautschnig]

Ok, done!

[tautschnig]

Wasn't this why there was a distinction between bool and c_bool. I thought they were 1 bit and 8 bit respectively and C defaulted to generating c_bool with __CPROVER_bool needed to generate actual ID_bool. Perhaps I have got very confused.

You are absolutely right, except the C front-end nowadays readily makes various "Boolean" operations (such as comparisons) a bool rather than an int. In some distant past we used to generate type casts in all sorts of places, but I think we stopped doing that. Or maybe I'm wrong and we never did that.