Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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