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