pointer comparable assert generated between void* and unsigned long
ID0001559: This issue was created automatically from Mantis Issue 1559. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001559 | Frama-C | Plug-in > Eva | public | 2013-11-19 | 2014-03-13 |
| Reporter | dpariente | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | Frama-C Neon-20140301 |
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!)