Frama-C Bug Tracking System - Frama-C
View Issue Details
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.
has duplicate 0001178closed virgile Several types for the same function 
Attached Files

Notes
(0001597)
yakobowski   
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   
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   
2014-02-12 16:58   
Fix committed to stable/neon branch.

Issue History
2011-02-17 18:22virgileNew Issue
2011-02-17 18:22virgileStatusnew => assigned
2011-02-17 18:22virgileAssigned To => virgile
2011-03-11 13:29yakobowskiNote Added: 0001597
2011-10-20 15:19virgileNote Added: 0002402
2012-04-12 13:49svn
2012-04-12 13:49svnStatusassigned => resolved
2012-04-12 13:49svnResolutionopen => fixed
2012-05-07 10:50virgileRelationship addedhas duplicate 0001178
2012-06-16 20:32svn
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2013-12-19 01:11yakobowskiSource_changeset_attached => framac master 85258885
2014-02-12 16:54yakobowskiSource_changeset_attached => framac stable/neon 85258885
2014-02-12 16:58yakobowskiNote Added: 0004660
2014-02-12 16:58yakobowskiAssigned Tovirgile => yakobowski
2014-02-12 16:58yakobowskiStatusclosed => resolved