--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on August 2015 ---
Hello Tim, Le 28/08/2015 06:46, Tim Newsham a écrit : > I looked into this and to my surprise frama-c's textual output > doesnt include a warning for this unverified assertion, but when > I loaded it up in the gui, it was clearly marked as yellow. I had > previously assumed that no warnings in the output meant that > everything was good. Is there a way to force warnings in the > output for all unverified assertions? This is very surprising. All GUI alarms should be in the output / log file. The recommended grep to do is: grep "got status [^v]" log_file [^v] is to avoid all "valid" statuses. Doing it on your original log file (http://www.thenewsh.com/~newsham/frama/big-analysis.txt.gz): FRAMAC_SHARE/libc/string.h:79:[value] Function memset: postcondition got status unknown. FRAMAC_SHARE/libc/string.h:59:[value] Function memcpy: postcondition got status unknown. auth.c:93:[value] Assertion got status unknown. FRAMAC_SHARE/libc/stdio.h:94:[value] Function fopen: postcondition got status unknown. auth.c:93 is "assert \initialized(buf + (32..40));". Best regards, david