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: Tue, 3 Apr 2012 11:04:03 +0200
  • In-reply-to: <569C6D7D26484241A530B87F45ADE1F88BC3C0@AOFRWMBXRSC004.resources.atosorigin.local>
  • References: <569C6D7D26484241A530B87F45ADE1F88BC223@AOFRWMBXRSC004.resources.atosorigin.local> <CABbVA-CFwGgKX=3OsqkqxHgVpmW=voy04E2RcYCDwSUr4VuJzg@mail.gmail.com> <569C6D7D26484241A530B87F45ADE1F88BC3C0@AOFRWMBXRSC004.resources.atosorigin.local>
Hi St?phane,

On Mon, Apr 2, 2012 at 10:09 PM, DUPRAT Stephane
<stephane.duprat at atos.net> wrote:
> As for us, we are interested in this information in two ways:
> ?1/ to help user in analysing causes of warning in going back in the call tree
> I previously used logs like " [value] computing for function f1 <- f2 <- main." processed by a awk file that displays the last path preceding a warning. Useful, when we have a lot of warnings at a memcpy call, for example.
> So, the callstack in that form will be very useful for us and certainly for others that are using Frama-C/Value.
> ?2/ The second reason will be to process them in the IDE integration (FCDT) in order to display a marker at each stage of a warning in the callstack, and perhaps, by providing navigation features to inspect warnings in the full project.
>
> In both usage, I just need to have all path for all warnings. I don't know if I need to get the information, each time an assertion is analysed.

I have added callstacks to all warnings that give rise to ACSL
assertions, which should improve things significantly. The remaining
ones will have to be converted one by one; this will happen gradually
before the release of Oxygen, as we clean up some parts of this code.

Note that option -val-print-callstacks may outlive its usefulness with
the Fluorine release (and might be subsequently removed), as we plan
to rewrite major parts of the emission of alarms. If this succeeds,
the good approach will be to use a lightweigtht plugin that will
listen to all emitted alarms, and decide what it wants to see printed.

-- 
Boris