How do I get Polyspace Code Prover to recognize the printf function?

When I try to verify some code that simply includes a call to "printf()", it throws the error below.

"Error: missing required prototype for varargs. procedure 'printf'."

How can I get Polyspace Code Prover to recognize this stdio call? I've tried to add the path to the stdio.h file to the "Include" section of my project.

Answer 1

[Christian Bard]

For this question, there are many answers like for instance relaunching with -D __polyspace_no_printf. It depends mainly of the options, log file and includes that have been added. I recommend you to contact Technical Support with complete log file. A plus would also to provide a small sample that reproduces behavior.