ID0000920: **This issue was created automatically from Mantis Issue 920. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000920 | Frama-C | Plug-in > Eva | public | 2011-08-11 | 2011-08-11 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | jrrk100 | **Assigned To** | pascal | **Resolution** | no change required | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - | ### Description : Using the following command line: frama-c -cpp-extra-args="-I`frama-c -print-share-path`/libc -nostdinc" `frama-c -print-share-path`/libc/fc_runtime.c -unspecified-access -val junk.c Bogus uninitialized value messages were produced for a trivial safe program. The attached program was extracted from a larger whole to demonstrate the issue. ### Additional Information : junk.c:18:[value] entering loop for the first time junk.c:19:[value] assigning non deterministic value for the first time junk.c:19:[kernel] warning: out of bounds write. assert \valid(ptr); junk.c:22:[value] Function print: precondition got status valid junk.c:10:[value] entering loop for the first time junk.c:10:[kernel] warning: accessing uninitialized left-value *ptr: assert(Ook) junk.c:11:[kernel] warning: accessing uninitialized left-value *tmp: assert(Ook) junk.c:10:[kernel] warning: out of bounds read. assert \valid(ptr); junk.c:11:[kernel] warning: out of bounds read. assert \valid(tmp); ## Attachments - [junk.c](/uploads/600421e2ff0cf80bf55ec15e23d2c405/junk.c)