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



Hello,

On Fri, May 7, 2010 at 10:48 AM, Tom Hawkins <tomahawkins at gmail.com> wrote:
>?Is this possible in ACSL without resorting to detailed
> assign annotations for every function in the program?

If we assume for the moment that the answer is no,
you can still generate assigns for all your functions
from any convenient format with a Frama-C plug-in.

At the moment I cannot find a good plug-in to copy
the skeleton from in order to do that
(when we encourage someone to write their own plug-in,
we usually recommend a simple, existing plug-in to use
as a model, but I'm not sure we have the "iterate on all
functions and insert a specification" variety. Perhaps
Aora?, but it provides sophisticated features, so it may
be hard to use as a model:
http://amazones.gforge.inria.fr/aorai/ ).

Still, Frama-C has a module to generate assigns clauses
for external functions for which only a type is known.
This is implemented in file src/logic/infer_annotations.ml .
You can experiment with it but we will need to provide
proper APIs if you decide this is the way to go.

The key part is:

  match kf.spec.spec_behavior with
  | [] ->
  ...
      kf.spec.spec_behavior <- [{b_name = "generated"; b_post_cond = [] ;
                                 b_assumes = [];
                                 b_assigns = Lazy.force generated_assigns}]
  | _ ->
      List.iter
        set_assigns
        kf.spec.spec_behavior

Pascal