--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on December 2011 ---
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