Bogus uninitialized value messages for trivial safe program
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="-Iframa-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);