View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001559 | Frama-C | Plug-in > Eva | public | 2013-11-19 10:18 | 2014-03-13 15:57 | ||||
Reporter | dpariente | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Fluorine-20130601 | ||||||||
Target Version | Fixed in Version | Frama-C Neon-20140301 | |||||||
Summary | 0001559: pointer comparable assert generated between void* and unsigned long | ||||||||
Description | [STANCE] The following code: /*------------------------------------------*/ typedef unsigned long size_t; struct apr_file_t; typedef struct apr_file_t apr_file_t; struct apr_file_t {char *fname ;}; int apr_file_write(apr_file_t *thefile, unsigned long *nbytes); int apr_file_write_full(apr_file_t *thefile, unsigned long nbytes, unsigned long *bytes_written) { int status; unsigned long a; a = nbytes; status = apr_file_write(thefile,& a); nbytes -= a; if (! (nbytes > (unsigned long)0)) return 0; return 1; } /*------------------------------------------*/ analyzed by: frama-c.exe -val -main apr_file_write_full -lib-entry foo.c -no-unicode generates an assert: [kernel] warning: pointer comparison: assert \pointer_comparable((void *)nbytes, (unsigned long)0); which, once the project is pretty-printed (-print -ocode ...), yields an error on the generated C file: [kernel] user error: no such predicate or logic function \pointer_comparable(void *, unsigned long) in annotation. (... indeed it might be an issue at Kernel level!) | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
yakobowski (manager) 2013-11-19 17:58 |
Although the attached patch fixes the kernel bug, a better fix is to write real assigns for function apr_file_write. The ones automatically created by the kernel are simultaneously too restrictive and too broad. Something like //@ ghost int FILESYSTEM; /*@ assigns \result, *nbytes, FILESYSTEM \from thefile->fname[0..], FILESYSTEM; */ int apr_file_write(apr_file_t *thefile, unsigned long *nbytes); should be much better. This is very generic in the sense that all write operations have an effect on the same memory zone, but is much more correct (and precise) for the contents of *nbytes. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2013-11-19 10:18 | dpariente | New Issue | |
2013-11-19 10:18 | dpariente | Status | new => assigned |
2013-11-19 10:18 | dpariente | Assigned To | => yakobowski |
2013-11-19 17:49 | yakobowski | File Added: patch-ptr-comparable | |
2013-11-19 17:51 | svn | ||
2013-11-19 17:51 | svn | Status | assigned => resolved |
2013-11-19 17:51 | svn | Resolution | open => fixed |
2013-11-19 17:58 | yakobowski | Note Added: 0004294 | |
2014-03-13 15:56 | signoles | Fixed in Version | => Frama-C Neon-20140301 |
2014-03-13 15:57 | signoles | Status | resolved => closed |
2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |