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

Hi,

The use of the nonfree ACSL importer plug-in is the industrial solution 
to that scoping problem.
It solves most of the real industrial needs since industrials use naming 
rules.

In your example, an alternative based on the merge of several contracts 
done by Frama-C tool could help ;
but that functionality is undocumented :
Just add
     //@assigns the_state;
in your C source file between line
    static int the_state = 0;
and
    void set_state(int val) {

Then, Frama-C tool will generate the clause
    //@assigns the_state, gState;
for the contract of the function set_state.

As you see, there are some ways to solve that kind of problems for the 
use and deployment of Frama-C in industrial contexts.
Patrick.

Le 28/05/2015 09:28, Frank Dordowsky a ?crit :
> Thank you for the explanation. But I then have a follow on: How can
> you handle variables of file scope in general? To be more specific:
>
> 1. separate header and source (.c) file
> 2. header contains declaration of a function with assign clauses in
>    ACSL annotations
> 3. definition of function in the source file modifies variable of file
>    scope not listed in the assigns clause because not visible in the
>    header.
>
> What is the best way to handle this situation with assigns clauses? 
> Has it been discussed somewhere else (pointer welcome)
>
> Thanks in advance
> Frank
>