suggest to suppress "Neither code nor specification" warning for __builtin_va_start
ID0001368: This issue was created automatically from Mantis Issue 1368. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001368 | Frama-C | Kernel | public | 2013-02-14 | 2016-07-05 |
| Reporter | Jochen | Assigned To | valentin.perrelle | Resolution | fixed |
| Priority | normal | Severity | text | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Oxygen-20120901 | Target Version | - | Fixed in Version | Frama-C Aluminium |
Description :
Running "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.