Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000728Frama-CKernelpublic2011-02-17 18:222014-02-12 16:58
Reportervirgile 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000728: Arguments are not checked when function call precedes function declaration
DescriptionCil allows a function to be called before being defined but does not check that the number/types of argument correspond. See for instance
tests/misc/call_variadic.i, which fails with frama-c -check, while the error should be reported directly when type-checking.
TagsNo tags attached.
Attached Files

- Relationships
has duplicate 0001178closedvirgile Several types for the same function 

-  Notes
(0001597)
yakobowski (manager)
2011-03-11 13:29

 Here is also an example that confuses deeply the value analysis, because of the absence of cast:

int f();

void main () {
  char c = 1;
  f(c);
}

int f(int i) {
  return 2*i;
}
(0002402)
virgile (developer)
2011-10-20 15:19

 tests/misc/call_variadic.i was removed from svn. Here it is:

int G;

int H;
int main () {
  int T=99;
  H= f(2);
  return T; /* gcc -O0 -> 26; gcc -O3 -> 99 */
}

int f(int x,int y, int z, int t,int t1,int t2,int t3,int t4,int t5,int t6) {
  x = 17;
  y=18;
  z=19;
  t=20;
  t1= 21;
  t2 = 22;
  t3 = 23;
  t4= 24;
  t5 = 25;
  t6 = 26;
  return x;
}
(0004660)
yakobowski (manager)
2014-02-12 16:58

 Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-02-17 18:22 virgile New Issue
2011-02-17 18:22 virgile Status new => assigned
2011-02-17 18:22 virgile Assigned To => virgile
2011-03-11 13:29 yakobowski Note Added: 0001597
2011-10-20 15:19 virgile Note Added: 0002402
2012-04-05 01:03 yakobowski Relationship added related to 0000109
2012-04-12 13:49 svn Checkin
2012-04-12 13:49 svn Status assigned => resolved
2012-04-12 13:49 svn Resolution open => fixed
2012-05-07 10:50 virgile Relationship added has duplicate 0001178
2012-06-16 20:32 svn Checkin
2012-06-16 20:32 svn Note Added: 0003145
2012-06-16 20:33 yakobowski Note Deleted: 0003145
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2014-02-12 16:58 yakobowski Note Added: 0004660
2014-02-12 16:58 yakobowski Assigned To virgile => yakobowski
2014-02-12 16:58 yakobowski Status closed => resolved

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker