Stack overflow with WP in MemTyped.Layout.compare_slot
Running frama-c -wp file.c
causes a stack overflow when file.c
contains:
int a;
fn() { struct b *c = &a; }
The stack trace is:
[kernel] Parsing file.c (with preprocessing)
[kernel:CERT:MSC:37] file.c:2: Warning:
Body of function fn falls-through. Adding a return statement
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[kernel] Current source was: file.c:2
The full backtrace is:
Raised by primitive operation at MemTyped.Layout.clayout in file "src/plugins/wp/MemTyped.ml", line 773, characters 19-29
Called from MemTyped.Layout.compare_slot in file "src/plugins/wp/MemTyped.ml", line 796, characters 33-45
<repeated around 1000 times>
Called from MemTyped.Layout.compare in file "src/plugins/wp/MemTyped.ml", line 812, characters 20-36
Unexpected error (Stack overflow).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 23.1 (Vanadium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
This C program looks a bit strange so I don't know how interesting this is but since I discovered it while searching for a simpler example of #2582, I thought I might as well report it.
Contextual information
- Frama-C installation method: opam
- Frama-C version: 23.1
- Plug-in used: WP + RTE
- OS Name: Fedora
- OS Version: 34