Frama-C Bug Tracking System - Frama-C
View Issue Details
0001368Frama-CKernelpublic2013-02-14 14:472016-07-05 17:17
ReporterJochen 
Assigned Tovalentin.perrelle 
PrioritynormalSeveritytextReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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".
However,
(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 Filesc ftest.c (313) 2013-02-14 14:47
https://bts.frama-c.com/file_download.php?file_id=471&type=bug

Notes
(0003694)
yakobowski   
2013-02-14 15:38   
__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.
(0003695)
Jochen   
2013-02-15 11:01   
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.
(0003879)
yakobowski   
2013-05-23 13:40   
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.
(0005995)
yakobowski   
2015-08-03 20:20   
Variadic functions will be handled automatically in Frama-C Aluminium.
(0006225)
yakobowski   
2016-07-05 17:17   
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
2013-02-14 14:47JochenNew Issue
2013-02-14 14:47JochenFile Added: ftest.c
2013-02-14 14:59signolesStatusnew => assigned
2013-02-14 14:59signolesAssigned To => virgile
2013-02-14 15:38yakobowskiNote Added: 0003694
2013-02-15 11:01JochenNote Added: 0003695
2013-05-23 13:40yakobowskiNote Added: 0003879
2013-05-23 13:40yakobowskiAssigned Tovirgile => yakobowski
2015-08-03 20:20yakobowskiNote Added: 0005995
2015-08-03 20:20yakobowskiAssigned Toyakobowski => valentin.perrelle
2016-07-05 17:17yakobowskiNote Added: 0006225
2016-07-05 17:17yakobowskiStatusassigned => closed
2016-07-05 17:17yakobowskiResolutionopen => fixed
2016-07-05 17:17yakobowskiFixed in Version => Frama-C Aluminium