--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Restricting write access to globals in ACSL



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.