--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on May 2010 ---
On Fri, May 7, 2010 at 7:12 AM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote: > Hello, > > On Fri, May 7, 2010 at 10:48 AM, Tom Hawkins <tomahawkins at gmail.com> wrote: >>?Is this possible in ACSL without resorting to detailed >> assign annotations for every function in the program? > > If we assume for the moment that the answer is no, > you can still generate assigns for all your functions > from any convenient format with a Frama-C plug-in. Yes, I'd like to write some Frama-C plug-ins. We have some verification methods we need with regard to how we perform task scheduling -- this would be another good plug-in canidate. I don't suppose a Haskell interface is available? Thanks. I'll start looking at Aorai.