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] linked lists?
- Subject: [Frama-c-discuss] linked lists?
- From: Claude.Marche at inria.fr (Claude Marche)
- Date: Thu, 01 Dec 2011 10:16:04 +0100
- In-reply-to: <A462DFA8-0824-4A6B-AB64-56FF1F9861FA@udel.edu>
- References: <A462DFA8-0824-4A6B-AB64-56FF1F9861FA@udel.edu>
Hi, On 30/11/2011 20:42, Stephen Siegel wrote: > Hi, I was trying to do something with this example taken from one of the ACSL manuals, but got an unimplemented feature error. I'm still using Carbon release. > > Does anyone understand what the feature is that's missing? It is not Frama-C that misses a feature, but the Jessie plugin. The message > State_builder.aborted because of unimplemented feature. > Please send a feature request at http://bts.frama-c.com with: > 'Interp.terms Tcomprehension'. > list$ says that set comprehensions are not supported > Could this example work in Nitrogen release? Not better. But if you just remove the assigns clauses, it should work both in Carbon and Nitro > Does anyone know any examples applying Frama-C to dynamic data structures such as linked lists? Yes, there are, although these are far from the simplest examples to start with. You may quickly face difficult issues regarding memory separation. A recent resource regarding these issues in the context of Frama-C and Jessie is the forthcoming PhD thesis : Fran?ois Bobot. Logique de s?paration et v?rification d?ductive. Th?se de doctorat, Universit? Paris-Sud, 2011. For older resources but immediately available, in the context of Caduceus which is a predecessor of the Jessie plugin: J.-C. Filli?tre, C. March?.Multi-Prover Verification of C Programs, in: 6th International Conference on Formal Engineering Methods, Seattle, WA, USA, J. Davies, W. Schulte, M. Barnett (editors), Lecture Notes in Computer Science, Springer, November 2004, vol. 3308, p. 15-29.http://www.lri.fr/~filliatr/ftp/publis/caduceus.ps.gz T. Hubert, C. March?.A case study of C source code verification: the Schorr-Waite algorithm, in: 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), Koblenz, Germany, B. K. Aichernig, B. Beckert (editors), IEEE Comp. Soc. Press, September 2005.http://www.lri.fr/~marche/hubert05sefm.ps T. Hubert, C. March?.Separation Analysis for Deductive Verification, in: Heap Analysis and Verification (HAV'07), Braga, Portugal, March 2007, p. 81-93.http://www.lri.fr/~marche/hubert07hav.pdf Hope this helps, - Claude
- Prev by Date: [Frama-c-discuss] Some question concerning code transformation using Cil and Frama_c_visitors.
- Next by Date: [Frama-c-discuss] using floating-point + in spec
- Previous by thread: [Frama-c-discuss] linked lists?
- Next by thread: [Frama-c-discuss] Some question concerning code transformation using Cil and Frama_c_visitors.