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: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Mon, 27 Jan 2014 09:15:54 +0100
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7660449AE@Mail1.FCMD.local>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C7660449AE@Mail1.FCMD.local>
Hello,

2014/1/27 Dharmalingam Ganesan <dganesan at fc-md.umd.edu>:
> 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?
>

Not quite: there is no notion of "sub-behavior" in ACSL. The closest
you can have is, as you did, to define a predicate for the common
part. A somehow contrived specification could use statement contracts
for the whole body of the function and the 'for foo:' clause, but
statement contracts cannot use the \result keyword in their ensures
clause, and the returns clause is not well supported by WP (this is
also the case for 'for foo:'), so that this approach will not work
very well in practice. Here is nevertheless an example:

/*@ behavior foo:
  assumes a == 0;
*/
int foo(int a, int b) {
  /*@ for foo: behavior foo_1:
    assumes b == 0;
    returns \result == 0;
    behavior foo_2:
    assumes b > 0;
    returns \result == 1;
    behavior foo_3:
    assumes b < 0;
    returns \result == -1;
    complete behaviors;
    disjoint behaviors;
  */
  { if (a==0) {
      if (b == 0) return 0;
      if (b<0) return -1;
      else return 1;
    }
    return 2;
  }
}


Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile