2021-03-05 07:11 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001368Frama-CKernelpublic2016-07-05 17:17
Assigned Tovalentin.perrelle 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0001368: suggest to suppress "Neither code nor specification" warning for __builtin_va_start
DescriptionRunning "frama-c -val ftest.c" on the attached program results in a "[kernel] warning: Neither code nor specification for function __builtin_va_start, generating default assigns from the prototype".
(1) it is impossible to provide a fully general definition of that function;
(2) providing a special version adapted to our example results in a declaration-mismatch error, (which disappears when the name is changed to e.g. "__builtin_va_star2", so the name "__builtin_va_start" is in fact known to Frama-C).
I suggest to suppress the former warning "Neither code nor specification..." for __builtin_va_start(), and similar for va_end(), etc.
TagsNo tags attached.
Attached Files
  • c file icon ftest.c (313 bytes) 2013-02-14 14:47 -
    #include <stdarg.h>
    //@ assigns \nothing;
    //extern void __builtin_va_start(va_list ap,int b) { }
      extern void __builtin_va_star2(va_list ap,int b) { }
    static int a = 5;
    static va_list ap;
    void main(int b,...)
    	/*@ assert a == 5; */
    c file icon ftest.c (313 bytes) 2013-02-14 14:47 +




yakobowski (manager)

__builtin_va_start is indeed a built-in known by Frama-C for some machdeps, including all those currently released. The correct user-accessible declaration is
extern void __builtin_va_start(__builtin_va_list);

With this declaration, the warning disappears. Note that calls to __builtin_va_(start|arg|end) are entirely ignored by value anyway.


Jochen (reporter)

Boris, thank you for your above note; your hints made our warnings about __builtin_va_xxx disappear. It may be sufficient to include these hints at an appropriate place in the Acsl manual.


yakobowski (manager)

This is not really related to ACSL, but to the plugins that need a spec for the _builtin_va_ functions. An internship related to variadic C functions is ongoing. Notice that _builtin_va_start and its friends are not proper C functions wrt. the types of their arguments, so we will need to change the AST anyway.


yakobowski (manager)

Variadic functions will be handled automatically in Frama-C Aluminium.


yakobowski (manager)

Builtin variadic (option -va) will transform variadic functions into non-variadic ones, and add specifications when possible. I'm not fond of Changing the ACSL manual because this issue is quite Frama-C centric.

-Issue History
Date Modified Username Field Change
2013-02-14 14:47 Jochen New Issue
2013-02-14 14:47 Jochen File Added: ftest.c
2013-02-14 14:59 signoles Status new => assigned
2013-02-14 14:59 signoles Assigned To => virgile
2013-02-14 15:38 yakobowski Note Added: 0003694
2013-02-15 11:01 Jochen Note Added: 0003695
2013-05-23 13:40 yakobowski Note Added: 0003879
2013-05-23 13:40 yakobowski Assigned To virgile => yakobowski
2015-08-03 20:20 yakobowski Note Added: 0005995
2015-08-03 20:20 yakobowski Assigned To yakobowski => valentin.perrelle
2016-07-05 17:17 yakobowski Note Added: 0006225
2016-07-05 17:17 yakobowski Status assigned => closed
2016-07-05 17:17 yakobowski Resolution open => fixed
2016-07-05 17:17 yakobowski Fixed in Version => Frama-C Aluminium
+Issue History