Support skipping variadic functions

[r-ross]

Applying CN to source code with variadic functions always fails. For example

$ cat hi.c
extern int printf (const char *format, ...);
/*@ spec printf(pointer format);
    requires true;
    ensures true;
@*/

int main (void)
{
   printf("Hi world");
   return 0;
}

$ cn verify hi.c
cn: internal error, uncaught exception:
    File "backend/cn/lib/wellTyped.ml", line 2064, characters 14-20: Assertion failed
    Raised at Cn__WellTyped.BaseTyping.infer_expr in file "backend/cn/lib/wellTyped.ml", line 2064, characters 14-38
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
...

Running cn verify --skip=printf hi.c has the same result. Using /*@ trusted; @*/ {} results in error: unsupported variadic functions which is better, but I don't see how to completely skip checking a function including its prototype. Please provide a way to completely skip variadic functions, either by extending trusted or by adding something new such as /*@ skip; @*/.

[peterohanley]

For something you can use immediately, you can do this in a file you --include which processes it before beginning the rest of the file. You need the initial arguments so these defines can hit the system headers without crashing.

// define out things we can't handle yet
#define WAR_NO_VARIADICS
#ifdef WAR_NO_VARIADICS
#define fprintf(a,b,...) fprintf(a,b)
#define fscanf(a,b,...) fscanf(a,b)
#define printf(a,...) printf(a)
#define sprintf(a,b,...) sprintf(a,b)
#define snprintf(a,b,...) snprintf(a,b)
#define scanf(a,...) scanf(a)
#define sscanf(a,b,...) sscanf(a,b)
#endif

The definition is present so you can insert more conditional workarounds in the file in question, although it sounds like that won't be a concern for this one.

[r-ross]

Thanks! That worked with the example above with #define printf(a,...) printf_(a) and /*@ trusted; @*/ {}. I had to use printf_ instead of printf to avoid error: Unknown function 'printf_proxy'.

[peterohanley]

duplicate of #301

[r-ross]

Related to #301 but not a duplicate since the ask is smaller (not full stdio.h support) and since this ticket is applicable beyond stdio.h (variadics in wchar.h and application specific variadics).

[dc-mak]

FYI, new issues for CN should be on www.github.com/rems-project/cn