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. ## Attachments - [ftest.c](/uploads/e9165646a4e7b8fd718d1b64bea5964e/ftest.c)