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!) ## Attachments - [patch-ptr-comparable](/uploads/93c9deb5551e847fe57e42df72977385/patch-ptr-comparable)