Replace int -> _Bool in goblint stubs arguments #1684
Conversation
Based on 00-sanity/01-assert. Related to #1682 (comment).
This matters when applied directly to pointers: #1682 (comment).
|
Doing the Having the assert analysis query with the cast added back (but not printed) seems to fix the issue, but I don't know of good of an idea that is. One possibility to having |
|
I now merged in master and used @michael-schwarz This reveals a problem in the bitfield domain. In particular, it doesn't handle casts to The overflow warning there is also spurious. It has to do with the fact that we consider |
CHANGES: Functionally equivalent to Goblint in SV-COMP 2026. * Add sequential portfolio for SV-COMP (goblint/analyzer#1845, goblint/analyzer#1867, goblint/analyzer#1877). * Add struct bitfield support (goblint/analyzer#1739, goblint/analyzer#1823). * Improve bitwise operations for integer domains (goblint/analyzer#1739). * Reimplement HTML output in OCaml (goblint/analyzer#1752). * Remove YAML witness version 0.1 support (goblint/analyzer#1812, goblint/analyzer#1817, goblint/analyzer#1852, goblint/analyzer#1853, goblint/analyzer#1855). * Fix incorrect invariants in witnesses (goblint/analyzer#1818, goblint/analyzer#1876). * Simplify relational invariants in witnesses (goblint/analyzer#1826, goblint/analyzer#1871, goblint/analyzer#1873). * Fix argument types in Goblint stubs (goblint/analyzer#1684, goblint/analyzer#1814, goblint/analyzer#1779, goblint/analyzer#1820).
Follow-up on #1682 (comment).
The replacement is straightforward but many tests seem to have failed, so this change is not as easy as it seemed.
TODO
Are there pre-C11 compatibility issues?Nevermind,_Boolexists since C99._Boolcasts? Try inLibraryFunctions.eval_booleverywhere._Boolcasts #1814.