--- layout: fc_discuss_archives title: Message 6 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



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;