Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001471Frama-CKernelpublic2013-08-29 12:062019-07-05 12:00
Reporterpascal 
Assigned Tosignoles 
PrioritylowSeverityminorReproducibilityalways
StatusclosedResolutionsuspended 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0001471: r23410: unsound reporting of pre-condition status
DescriptionConsider 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.
TagsNo tags attached.
Attached Filesc file icon t.c [^] (298 bytes) 2013-08-29 12:06 [Show Content]

- Relationships

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

Unobservable bug.

- Issue History
Date Modified Username Field Change
2013-08-29 12:06 pascal New Issue
2013-08-29 12:06 pascal File Added: t.c
2013-08-29 22:35 yakobowski Status new => assigned
2013-08-29 22:35 yakobowski Assigned To => yakobowski
2013-08-30 11:19 svn Checkin
2013-08-30 11:30 yakobowski Assigned To yakobowski => signoles
2013-08-30 11:30 yakobowski Status assigned => feedback
2013-08-30 15:17 yakobowski Priority normal => low
2013-08-30 15:17 yakobowski Severity major => minor
2013-09-26 11:14 signoles Status feedback => acknowledged
2019-07-05 11:57 signoles Note Added: 0006812
2019-07-05 11:57 signoles Status acknowledged => closed
2019-07-05 11:57 signoles Resolution open => suspended
2019-07-05 12:00 signoles Note Edited: 0006812 View Revisions


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker