Add warnings about missing function declarations#1911
Conversation
This is allowed by older versions of C. These functions are assumed to return int, etc, which can cause internal type mismatches for standard functions.
There was a problem hiding this comment.
Pull request overview
This PR adds analyzer warnings for calls to functions that lack a proper prior declaration/prototype (old-C implicit declarations / non-prototype declarations), because the assumed default types can lead to internal type mismatches (e.g., incorrect casts and ikind errors). It also updates many regression tests to include the relevant headers (and adjusts golden outputs) so that standard/library function prototypes are available.
Changes:
- Emit warnings when calling a function whose CIL type is marked with the
missingprotoattribute. - Extend special-casing of known globals and adjust race analysis handling of
freecasts. - Update a broad set of regression tests by adding missing
#includes and updating expected outputs/locations.
Reviewed changes
Copilot reviewed 264 out of 264 changed files in this pull request and generated 5 comments.
| File | Description |
|---|---|
| src/framework/constraints.ml | Emits warnings (msg_final + per-callsite warning) when a called function has missingproto. |
| src/framework/control.ml | Treats __mb_cur_max as a special global (MacOS compatibility). |
| src/analyses/raceAnalysis.ml | Strips outer implicit void* cast for free access events to preserve underlying pointer type. |
| tests/regression/** | Adds missing standard/Goblint headers and updates golden outputs/line numbers to account for the new warnings and include shifts. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 264 out of 264 changed files in this pull request and generated 1 comment.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
This is allowed by older versions of C.
These functions are assumed to return
int, etc, which can cause internal type mismatches for standard functions.For example, it's a problem if
llabsgets return typeintby CIL, but Goblint assumes it to belong long. This causes missing/extra/wrong implicit casts to be inserted, leading to ikind errors and whatnot.