Replies: 1 comment
-
|
Hi @zezo003, ESBMC supports cross-functional memory safety analysis, but its cross-file memory security detection capabilities are more limited and may depend on how the source code is compiled and fed into the tool. For cross-function memory safety detection, ESBMC can analyze memory safety issues across different functions within a single translation unit (i.e., a single compiled source file). For example, it checks for:
For cross-file analysis, ESBMC generally analyzes one translation unit at a time, typically a .c file with all includes and macros expanded by a preprocessor. To achieve cross-file analysis, the usual approach is:
ESBMC doesn’t handle separate compilation units or link-time memory analysis by default like some static analyzers (e.g., Coverity or CodeQL). In summary, cross-function detection is supported. However, cross-file detection is limited and requires workarounds, such as flattening code into a single file. Please let me know if you have further questions. Best, |
Beta Was this translation helpful? Give feedback.
Uh oh!
There was an error while loading. Please reload this page.
-
does ESBMC support cross-file and cross-function memory security issue detection?
Beta Was this translation helpful? Give feedback.
All reactions