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.
|Product Version||Frama-C Oxygen-20120901||Target Version||-||Fixed in Version||Frama-C Aluminium|
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.