2021-03-01 05:58 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000728Frama-CKernelpublic2011-02-17 18:222014-02-12 16:58
Reportervirgile 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
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 
+Relationships

-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.
+Notes

-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-12 13:49 svn
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
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master 85258885
2014-02-12 16:54 yakobowski Source_changeset_attached => framac stable/neon 85258885
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
+Issue History