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 03:48:46 -0500
For better or worse, our embedded applications makes heavy use of global variables for communicating between different parts of the program. In general, any function is allowed to read from these globals, but we want to restrict which functions can write to which variables. Is this possible in ACSL without resorting to detailed assign annotations for every function in the program? I can image the notion of variable contracts could be useful, where you could define which functions can write to variables, which functions can read from variables, and even specify valid temporal sequences for reads and writes. For example: /*@ assigned-by sensorProcessing; referenced-by controlLoop, faultManagement, signalProbing; */ double swashAngle1Feedback; /*@ assigned-by modeLogic; referenced-by \nothing; */ volatile bool isolationValveSolenoidDriver;
- 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
- Prev by Date: [Frama-c-discuss] Uncaught exception
- Next by Date: [Frama-c-discuss] binaries for linux?
- Previous by thread: [Frama-c-discuss] Uncaught exception
- Next by thread: [Frama-c-discuss] Restricting write access to globals in ACSL
- Index(es):