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] Need help on C-code slicing

  • Subject: [Frama-c-discuss] Need help on C-code slicing
  • From: francois.armand at orange.fr (François Armand)
  • Date: Tue, 14 Jun 2011 16:25:58 +0200
  • In-reply-to: <BANLkTi=NVuC01B4Cm88qxpATpUqTC2JQqQ@mail.gmail.com>
  • References: <BANLkTi=eKHMSg8Sdq88OwqqO890tjdg+Cw@mail.gmail.com> <BANLkTikG=kiiqsZCCZvic1FW=Vc2cn2J6w@mail.gmail.com> <BANLkTinFUUT9m_9ek2nd7V7_-T-OY9UTjQ@mail.gmail.com> <BANLkTi=NVuC01B4Cm88qxpATpUqTC2JQqQ@mail.gmail.com>
Thanks for all these replies.

I've made some progress: I solved my "degeneration" issue by #ifdef'ing out
a few lines. Anyhow, they were of interest to me. The value analysis seems
now to reach the end without trouble.

I then discovered that what I really wanted was not really slicing but
rather "Scope analysis".

However, for some reason I have not fully discovered yet, some of the code
I'm interested in is marked as dead by the value analysis (strike through
and red background in the GUI).  By simplifying some of the original code,
I've made some progress to provide conditions which somehow prevent frama-c
to believe code is dead. But I can't succeed circumventing my current
problem, where a function is tagged as "NON TERMINATING FUNCTION". As far as
I can understand, Frama-C seems to stop right after. (Naive?) usage of
Frama_C_dump_each (with -slevel 1000) has not yet sched any light...

Any hint/hope  would really be appreciated!
Thanks in advance,

Fran?ois

2011/6/9 David MENTRE <dmentre at linux-france.org>

> Hello,
>
> 2011/6/9 Fran?ois Armand <francois.armand at orange.fr>:
> > I'm gonna spend some time on this learning curve and will very likely
> come
> > back later on
>
> If you plan to spent some time on learning Frama-C and especially the
> Value Analysis, I recommend reading the Frama-C blog. Pascal has made
> a lot of posts that detail the Value Analysis (amongst other points):
>  http://blog.frama-c.com/
>  http://blog.frama-c.com/index.php?tag/value
>
> Best regards,
> david
>
> _______________________________________________
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110614/7b408129/attachment.htm>