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}) }} ## Attachments - [modular.c](/uploads/d23c0d7f1d7d0eef2b867422055b0869/modular.c)