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] WP - How to represent duplicate assumes?

  • Subject: [Frama-c-discuss] WP - How to represent duplicate assumes?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • Date: Sun, 26 Jan 2014 18:25:54 -0500
Hi,

For this example, some of my behaviors share a set of assumes. For example, HighSaO2, LowSaO2, and RoundSaO2 share the assumes !Is_Adv_or_Mon_Failed predicate.

Is there a possibility to declare assumes that are shared by a set of behaviors only once, just to make the behavioral spec lean?


Thanks a lot.
Dharma



 behavior HighSaO2: // SaO2 exceeds max
    assumes !Is_Adv_or_Mon_Failed(mbMonitorFailed, mtstAdvisoryStatus.tenumState);
    assumes mtenumPruStatus == PRU_OFF;
    ensures mfSaO2 > nPULSEOX_MAX_VALUE ==> mtenumDataValidity == DATA_INVALID;
 
   behavior LowSaO2: // SaO2 below min
    assumes !Is_Adv_or_Mon_Failed(mbMonitorFailed, mtstAdvisoryStatus.tenumState);
    assumes mtenumPruStatus == PRU_OFF;
    ensures mfSaO2 < nPULSEOX_MIN_VALUE ==> mtenumDataValidity == DATA_INVALID;

   behavior RoundSaO2: // SaO2 rounded to the nearest int
     assumes !Is_Adv_or_Mon_Failed(mbMonitorFailed, mtstAdvisoryStatus.tenumState);
     ensures is_rounded(\old(mfSaO2), mfSaO2);

   behavior Reset:
    ensures mfSaO2 > nPULSEOX_MAX_VALUE ==> mfSaO2 == nPULSEOX_MAX_VALUE;