--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on December 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] linked lists?



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