No convenient way to specify shared library functions as assigns clauses
ID0001479: This issue was created automatically from Mantis Issue 1479. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001479 | Frama-C | Kernel > ACSL implementation | public | 2013-09-05 | 2016-07-05 |
| Reporter | pascal | Assigned To | pascal | Resolution | no change required |
| Priority | low | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | - |
Description :
Shared libraries functions store their entire state in a struct, in a pattern similar to that of the attached code.
It would be convenient to have a way to specify that while *ctx_p is computed \from *ctx_p, the pointer field(s) are used only by address and should not pollute the integer fields.
Currently:
$ ~/ppc/bin/toplevel.opt -val modular.c … [value] Values at end of function main: ctx ? {{ garbled mix of &{ctx} (origin: Misaligned {modular.c:21}) }} y ? {{ garbled mix of &{ctx} (origin: Misaligned {modular.c:21}) }}