0001559: pointer comparable assert generated between void* and unsigned long

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

Platform

OS Version

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

patch-ptr-comparable [^] (581 bytes) 2013-11-19 17:49 [Show Content] [Hide Content]

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 _ ->

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.

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	Checkin
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