Frama-C-discuss mailing list archives

stephane.duprat at atos.net (DUPRAT Stephane) · Mon, 2 Apr 2012 20:09:40 +0000

Hi Boris,

Thanks for the quick answer.
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.

Regards,

St?phane

> -----Message d'origine-----
> De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-
> discuss-bounces at lists.gforge.inria.fr] De la part de Boris Yakobowski
> Envoy? : lundi 2 avril 2012 18:05
> ? : Frama-C public discussion
> Objet : Re: [Frama-c-discuss] use of -val-print-callstacks option
>
> 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
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

________________________________

Ce message et les pi?ces jointes sont confidentiels et r?serv?s ? l'usage exclusif de ses destinataires. Il peut ?galement ?tre prot?g? par le secret professionnel. Si vous recevez ce message par erreur, merci d'en avertir imm?diatement l'exp?diteur et de le d?truire. L'int?grit? du message ne pouvant ?tre assur?e sur Internet, la responsabilit? du groupe Atos ne pourra ?tre engag?e quant au contenu de ce message. Bien que les meilleurs efforts soient faits pour maintenir cette transmission exempte de tout virus, l'exp?diteur ne donne aucune garantie ? cet ?gard et sa responsabilit? ne saurait ?tre engag?e pour tout dommage r?sultant d'un virus transmis.

This e-mail and the documents attached are confidential and intended solely for the addressee; it may also be privileged. If you receive this e-mail in error, please notify the sender immediately and destroy it. As its integrity cannot be secured on the Internet, the Atos group liability cannot be triggered for the message content. Although the sender endeavors to maintain a computer virus-free network, the sender does not warrant that this transmission is virus-free and will not be liable for any damages resulting from any virus transmitted.