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: anne.pacalet at inria.fr (Anne Pacalet)
- Date: Thu, 09 Jun 2011 11:15:22 +0200
- In-reply-to: <BANLkTi=eKHMSg8Sdq88OwqqO890tjdg+Cw@mail.gmail.com>
- References: <BANLkTi=eKHMSg8Sdq88OwqqO890tjdg+Cw@mail.gmail.com>
Le 09/06/2011 10:46, Fran?ois Armand a ?crit : > I get a "Degeneration occurred" banner in the window title bar.. and seem to be > unable to get any usable result from this point. This is a message from the value analysis part of Frama-C which runs because you used the [-val] option, but would be started anyway before any slicing request since the slicing uses the value analysis results. I don't know all the details about the context of the "Degeneration" messages but it is probably because the analysis doesn't have enough context to compute something interesting on your file. You said that you are only interested in one file, but do your have an entry point in this file ? If not, you should write a "dummy" main function to be used as entry point for the analysis. I think that a good starting point to find the source of your problem is to read the Value analysis documentation : http://frama-c.com/download/frama-c-value-analysis.pdf Hope this helps, -- Anne.
- References:
- [Frama-c-discuss] Need help on C-code slicing
- From: francois.armand at orange.fr (François Armand)
- [Frama-c-discuss] Need help on C-code slicing
- Prev by Date: [Frama-c-discuss] Need help on C-code slicing
- Next by Date: [Frama-c-discuss] Need help on C-code slicing
- Previous by thread: [Frama-c-discuss] Need help on C-code slicing
- Next by thread: [Frama-c-discuss] Need help on C-code slicing
- Index(es):