Frama-C Bug Tracking System

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 
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 file icon ftest.c [^] (313 bytes) 2013-02-14 14:47 [Show Content]

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

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker