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] Restricting write access to globals in ACSL
- Subject: [Frama-c-discuss] Restricting write access to globals in ACSL
- From: tomahawkins at gmail.com (Tom Hawkins)
- Date: Fri, 7 May 2010 08:33:43 -0500
- In-reply-to: <z2vb15d09071005070512j60901143q6717c26665d21495@mail.gmail.com>
- References: <v2z594c1e831005070148k75e706f3tbbb467aa67f1095e@mail.gmail.com> <z2vb15d09071005070512j60901143q6717c26665d21495@mail.gmail.com>
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.
- Follow-Ups:
- [Frama-c-discuss] Restricting write access to globals in ACSL
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Restricting write access to globals in ACSL
- References:
- [Frama-c-discuss] Restricting write access to globals in ACSL
- From: tomahawkins at gmail.com (Tom Hawkins)
- [Frama-c-discuss] Restricting write access to globals in ACSL
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Restricting write access to globals in ACSL
- Prev by Date: [Frama-c-discuss] binaries for linux?
- Next by Date: [Frama-c-discuss] Uncaught exception
- Previous by thread: [Frama-c-discuss] Restricting write access to globals in ACSL
- Next by thread: [Frama-c-discuss] Restricting write access to globals in ACSL
- Index(es):