Skip to content

Checking number of arguments passed to C functions

ID0000552: This issue was created automatically from Mantis Issue 552. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000552 Frama-C Kernel public 2010-08-02 2010-12-17
Reporter pascal Assigned To virgile Resolution fixed
Priority normal Severity feature Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Boron-20100401 Target Version - Fixed in Version Frama-C Carbon-20101201-beta1

Description :

There currently isn't much checking of function arguments in the front-end. The following program is accepted, although it passes the wrong number of arguments for both calls to retint:

int retint(int x ) { int __retres ; __retres = 42 + x; return (__retres); }

int main(int c ) { int x ; int tmp ; x = retint(); tmp = retint(c,c); return (tmp); }

Arguments for not implementing this feature: there are perfectly good compilers to check for this, and not having rigid rules in place may even help with older code containing variadic functions. I am not sure when the current convention for declaring variadic functions became standardized, and it may not have been from the beginning.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information