2021-03-05 07:11 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001368Frama-CKernelpublic2016-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)

__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)

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)

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)

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

~0006225

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