--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] arbitrary buffers in analysis



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