2021-02-27 11:28 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001559Frama-CPlug-in > Evapublic2013-11-19 10:182014-03-13 15:57
Reporterdpariente 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001559: 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!)
TagsNo tags attached.
Attached Files
  • ? file icon patch-ptr-comparable (581 bytes) 2013-11-19 17:49 - 
    Index: cil/src/logic/logic_utils.ml
===================================================================
--- cil/src/logic/logic_utils.ml	(revision 24484)
+++ cil/src/logic/logic_utils.ml	(working copy)
@@ -1867,7 +1867,6 @@
              | TPtr(TFun _,_) ->
                  Logic_const.term ~loc (TCastE(cfct_ptr,t)) fct_ptr, fct_ptr
              | TPtr _  -> t, obj_ptr
-             | TInt _ when Cil.isLogicZero t -> t, obj_ptr
              | TVoid _ | TInt _ | TFloat _ | TFun _ | TNamed _
              | TComp _ | TEnum _ | TBuiltin_va_list _
              | TArray _ ->
    ? file icon patch-ptr-comparable (581 bytes) 2013-11-19 17:49 +

-Relationships
+Relationships

-Notes

~0004294

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.
+Notes

-Issue History
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
+Issue History