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] use of -val-print-callstacks option

  • Subject: [Frama-c-discuss] use of -val-print-callstacks option
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Mon, 2 Apr 2012 18:05:25 +0200
  • In-reply-to: <569C6D7D26484241A530B87F45ADE1F88BC223@AOFRWMBXRSC004.resources.atosorigin.local>
  • References: <569C6D7D26484241A530B87F45ADE1F88BC223@AOFRWMBXRSC004.resources.atosorigin.local>
Hi St?phane,

On Mon, Apr 2, 2012 at 5:02 PM, DUPRAT Stephane
<stephane.duprat at atos.net> wrote:
> I'm trying to use -val-print-callstacks option in order to have the calling context in each warning of frama-C/Value, but I don't see any difference in logfile with or without this function.
> Is there any misunderstood at my side ?

Option -val-print-callstacks is in a preliminary state for the moment,
for both technical reasons and some questioning on our side.
Currently, you can see its effects on the following code:

--------------
int i;
int t[18];

void f1() {
  while(1) {
    t[i] = 1;
    i++;
  }
}

void f2() {
  f1();
}

void main () {
  f2();
}
------------'

With -val-print-callstacks, you get 'stack: f1 :: cs.c:12 <- f2 ::
cs.c:16 <- main' after the message 'cs.c:6:[value] Assertion got
status unknown.'. However, you do _not_ get a message the first time
the alarm is emitted. The two warnings are emitted by two different
parts of Value, and it is not trivial to add the call-stack when the
alarm is emitted first. This should be corrected for Oxygen, though.

Regarding the verbosity of this option, we have been wondering which
version would be the most interesting:
- a message, with the stack, is emitted each time Value analyzes a
statement with an assertion (can possibly result in huge logs)
- identical messages (including stack and the status of the assertion)
are emitted only once, the first time the assertion is evaluated with
this stack and status (shorted, may be more complicated to
understand).

Do you have an opinion on this question? We coul implement both
versions, but this would further complicate the command-lines.

Regards,

-- 
Boris