Frama-C Bug Tracking System - Frama-C
View Issue Details
0001471Frama-CKernelpublic2013-08-29 12:062019-07-05 12:00
pascal 
signoles 
lowminoralways
closedsuspended 
Frama-C GIT, precise the release id 
 
0001471: r23410: unsound reporting of pre-condition status
Consider the program below. The pre-condition of f() is not true for all calls. /*@ ensures l <= \result <= u ; */ int Frama_C_interval(int l, int u); /*@ requires \valid(p+(0..30)); */ void f(char * p) { *(p + Frama_C_interval(0,30)) = 1; } int x; void (*pf)(char*) = f; void g(char *p) { x = 1; pf(p); } main(){ char t[31]; g(t); g(t+Frama_C_interval(0,1)); } Yet: $ frama-c -val t.c -report … -------------------------------------------------------------------------------- --- Properties of Function 'f' -------------------------------------------------------------------------------- [ Valid ] Pre-condition (file t.c, line 4) by Call Preconditions. And frama-c-gui -val t.c similarly shows a green icon for f's contract when the body of f is displayed.
No tags attached.
c t.c (298) 2013-08-29 12:06
https://bts.frama-c.com/file_download.php?file_id=514&type=bug
Issue History
2013-08-29 12:06pascalNew Issue
2013-08-29 12:06pascalFile Added: t.c
2013-08-29 22:35yakobowskiStatusnew => assigned
2013-08-29 22:35yakobowskiAssigned To => yakobowski
2013-08-30 11:19svnCheckin
2013-08-30 11:30yakobowskiAssigned Toyakobowski => signoles
2013-08-30 11:30yakobowskiStatusassigned => feedback
2013-08-30 15:17yakobowskiPrioritynormal => low
2013-08-30 15:17yakobowskiSeveritymajor => minor
2013-09-26 11:14signolesStatusfeedback => acknowledged
2019-07-05 11:57signolesNote Added: 0006812
2019-07-05 11:57signolesStatusacknowledged => closed
2019-07-05 11:57signolesResolutionopen => suspended
2019-07-05 12:00signolesNote Edited: 0006812View Revisions

Notes
(0006812)
signoles   
2019-07-05 11:57   
(edited on: 2019-07-05 12:00)
Unobservable bug.