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