On Sun, May 9, 2010 at 12:54 AM, Lee Pike
Tom,
Have you used any of these tools? They're pretty cool. I'd be interested to hear you opinion.
Not yet. We were considering using them for a C security-analysis, but rolled-our-own stuff in Haskell.
Do you guys support ACSL or something similar? One major short comings of Frama-C is its inability to prove a formula false. As such, the tool will not return any counter examples to help with debugging.
I'll ask around Galois if there's been any experience with it.
Did anyone respond to your post about a Haskell interface?
Negative. I'm looking into writing a bit of OCaml to dump out the Cil+ACSL stuff, which I can then read with Haskell. One thing I really like about Frama-C is its use of multiple solvers. Some work better than others, and it's very easy to see this in the gWhy GUI, as well as overall proof coverage. It would be nice to have a Haskell library where we could stream in a bunch of proof obligations and it would farm it out to different solvers, possibly running on different machines. It could also keep track of which obligations have proved true or false, so it doesn't wast time running the obligation on other solvers -- gWhy doesn't currently do this. You kind of alluded to these benefits when you recommended using SMT-LIB instead of Yices for AFV, but I didn't appreciated it until now. -Tom
Hi Tom Quite a while ago I interfaced Haskell and Ocaml/CIL through both ATerms and ASDL pickles. I can look at digging out this code if you like - it was fairly complete, but it had a bug somewhere and will probably be a few revisions behind the current CIL. Best wishes Stephen
On Thu, May 13, 2010 at 11:58 AM, Stephen Tetley
Hi Tom
Quite a while ago I interfaced Haskell and Ocaml/CIL through both ATerms and ASDL pickles.
I can look at digging out this code if you like - it was fairly complete, but it had a bug somewhere and will probably be a few revisions behind the current CIL.
Thanks Stephen, I'd like to see it. I almost have something working. I created a little OCaml parser to read the cil_types.mli file from Frama-C, which I then use to automatically generate a Frama-C plugin that dumps the database, and a Haskell module that reads it. I should have something released to Hackage by next week. But if anyone is curious, here is the repo I'm working from: http://github.com/tomahawkins/cil
Hi Tom I can't really make out what-is-what from the git-repository. Is it just hosting the generator and not the generated code at the moment? Also I don't know Frama-C, are you generating the whole CIL syntax tree from cli_types.mli? By the look of things it is CIL to line 1116 - (** Types of logic terms. *) - then Frama-C. My code is mostly here: http://code.google.com/p/copperbox/source/browse/#svn/trunk/libs/_old/cil-pi... Best wishes Stephen
participants (2)
-
Stephen Tetley -
Tom Hawkins