85521b0263
goto-gcc now runs the ls_parse.py script whenever the target codebase is being compiled with a custom linker script (specified with the -T option). goto-gcc then synthesizes the linker script definitions that ls_parse reported, and adds them to the goto-program as if those definitions were defined in the target C program rather than the linker script. This solves a problem where the values of some C variables are inaccessible from CBMC because those variables are defined in the linker script rather than the C codebase. It also solves the problem of CBMC not knowing what memory regions are accessible to the C program, again because the memory regions are declared to be valid in the linker script. This commit also introduces three tests for this functionality. This commit also fixes a small bug in ls_parse.py that made it reject some valid linker scripts. |
||
|---|---|---|
| .. | ||
| main.c | ||
| script.ld | ||
| test.desc | ||