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] Information hiding: how to handle module's private static variables in Frama-C?

  • Subject: [Frama-c-discuss] Information hiding: how to handle module's private static variables in Frama-C?
  • From: moy at adacore.com (Yannick Moy)
  • Date: Wed, 27 Nov 2013 16:44:38 +0100
  • In-reply-to: <CAC3Lx=ZGN6AxDO93uhmkGsb8nkV2_kZcpv-ukjBN9cK=LCFEFg@mail.gmail.com>
  • References: <CAC3Lx=bqpi2v3cwLZ1bKeWPm262vt+44Ocw1DvQoh1OkGSLQhA@mail.gmail.com> <CAOH62Jg5uajSHmWa-ntPLMD9M9S4EtuFzjQ6nCqjy_=dpjoL5A@mail.gmail.com> <CAC3Lx=ZGN6AxDO93uhmkGsb8nkV2_kZcpv-ukjBN9cK=LCFEFg@mail.gmail.com>
-- David MENTRE (2013-11-27)
> 
> 
>> I think that Frama-C and ACSL should natively incorporate some of these
>> ideas, but as of yet, they do not.
> 
> Yes. B Method and SPARK 2014 probably have an advantage in this
> regard. For example, SPARK 2014 has a mechanism to abstract some
> internal module variables into abstract ones (see
> http://www.spark-2014.org/entries/detail/spark-2014-rationale-global-state).
> But I haven't played with this mechanism so I don't know how useful it
> is in practice.

Hi David,

It is a critical feature for current SPARK industrial users, to solve the scalability issue: when you have dozens or hundreds of global variables in different parts of your program, you want to be able to refer to them abstractly in the specifications, and it can also make a difference for the efficiency of the underlying analysis/proof tools.
--
Yannick Moy, Senior Software Engineer, AdaCore