2021-03-05 07:11 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001368Frama-CKernelpublic2013-02-14 14:472016-07-05 17:17
ReporterJochen 
Assigned Tovalentin.perrelle 
PrioritynormalSeveritytextReproducibilityalways
StatusclosedResolutionfixed 
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 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,...)
{
	__builtin_va_start(ap,b);
	__builtin_va_star2(ap,b);
	/*@ assert a == 5; */
}
    c file icon ftest.c (313 bytes) 2013-02-14 14:47 +

-Relationships
+Relationships

-Notes

~0003694

yakobowski (manager)

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 (reporter)

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 (manager)

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 (manager)

2015-08-03 20:20

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

~0006225

yakobowski (manager)

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

-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