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] Assign clauses with ghost variables

  • Subject: [Frama-c-discuss] Assign clauses with ghost variables
  • From: frank at dordowsky.de (Frank Dordowsky)
  • Date: Sun, 31 May 2015 14:21:01 +0200 (CEST)
  • In-reply-to: <mailman.5768.1432882366.22323.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.5768.1432882366.22323.frama-c-discuss@lists.gforge.inria.fr>
Responding to Virgile:

your proposal is very elegant. I understand that I need to define as
many "abstract regions" as there will be static variables of file
scope modified by that function. Another disadvantage is that you must
know about the internals of the function at the outside, specification
level, violating the information hiding principle to a certain extent.

Would it be possible to exempt static variables of file scope from
evaluation of the assigns clauses? Or to have another keyword for this
situation, something like "assigns \internals"?

Frank


> ------------------------------
>
> Message: 2
> Date: Thu, 28 May 2015 17:51:26 +0200
> From: Virgile Prevosto <virgile.prevosto at m4x.org>
> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
> Subject: Re: [Frama-c-discuss] Assign clauses with ghost variables
> Message-ID:
> 	<CA+yPOVhUwnZLdKMb6dPNZTFmamcACU=ydVMCSnbRr9g3cA4tRw at mail.gmail.com>
> Content-Type: text/plain; charset=UTF-8
>
> Hello David,
>
> 2015-05-28 9:52 GMT+02:00 David MENTRE <dmentre at linux-france.org>:
>>
>> In my humble opinion, there is lack of abstraction of Frama-C in such
>> situations. You need to mention every modified variable in contracts, even
>> those that you would like to be hidden. For example, I see no way to use
>> static variables (variable local to a file, but if used should be mentioned
>> in contract therefore seen from outside!).
>
> You're perfectly right, we lack an option of an abstract memory region
> (and probably some separation formulas saying that the visible part of
> the memory is separated from it). This shows up for static variables
> C, but would be much more widespread for private members of C++
> classes. I don't have any really satisfying solution for now, but the
> following work:
>
> --- static.h
> #define INITSTATE (1)
> //@ ghost int gState=INITSTATE;
>
> //@ logic int* abstract_region;
>
> /*@
>  @  assigns gState, *abstract_region;
>  @  ensures val == gState;
>  @*/
> void set_state(int val);
>
> --- static.c
> #include "static.h"
> static int the_state = 0;
>
> //@ axiomatic State { axiom internal_state: abstract_region == &the_state; }
>
> void set_state(int val) {
>  the_state = val;
> //@ ghost gState = the_state;
> }
>
> ---
> Note however that if you use static.h without static.c, you will need
> to add \separate(abstract_region,xxx) axioms for basically all your
> global variables[1] (a plug-in might help here, but this is still
> tedious), otherwise set_state will have the ability to write anywhere
> in memory. It would be interesting to investigate how to handle
> natively these kinds of abstract regions, but this is not an easy
> goal. In the mean time, Patrick's solution seems a more sensible
> workaround.
>
> Best regards,
> -- 
> E tutto per oggi, a la prossima volta
> Virgile
> [1] I make absolutely no warranty about whether this is sufficient to
> make WP happy
>