Frama-C-discuss mailing list archives

frank at dordowsky.de (Frank Dordowsky) · Thu, 28 May 2015 09:28:05 +0200 (CEST)

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

On Wed, 27 May 2015, frama-c-discuss-request at lists.gforge.inria.fr wrote:

> Send Frama-c-discuss mailing list submissions to
> 	frama-c-discuss at lists.gforge.inria.fr
>
> To subscribe or unsubscribe via the World Wide Web, visit
> 	http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> or, via email, send a message with subject or body 'help' to
> 	frama-c-discuss-request at lists.gforge.inria.fr
>
> You can reach the person managing the list at
> 	frama-c-discuss-owner at lists.gforge.inria.fr
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Frama-c-discuss digest..."
>
>
> Today's Topics:
>
>   1. Assign clauses with ghost variables (Frank Dordowsky)
>   2. Re: Assign clauses with ghost variables (BAUDIN Patrick)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Tue, 26 May 2015 22:24:04 +0200 (CEST)
> From: Frank Dordowsky <frank at dordowsky.de>
> To: Frama-C Mailing List <frama-c-discuss at lists.gforge.inria.fr>
> Subject: [Frama-c-discuss] Assign clauses with ghost variables
> Message-ID: <alpine.LNX.2.03.1505262221440.728 at dordowsky.de>
> Content-Type: TEXT/PLAIN; format=flowed; charset=US-ASCII
>
> I have got a problem with assign clauses and ghost variables. WP
> generates a goal for the assign clause which cannot be proven by
> Alt-Ergo and Coq. I will use my former example from a previous thread.
> This is the header file:
>
> #define INITSTATE (1)
> //@ ghost int gState=INITSTATE;
>
> /*@
>   @  assigns gState;
>   @  ensures val == gState;
>   @*/
> void set_state(int val);
>
> The corresponding C source is
>
> #include "intstate_ghost.h"
> static int the_state = 0;
>
> void set_state(int val) {
>   the_state = val;
> //@ ghost gState = the_state;
> }
>
> Interestingly, the generated goal file set_state_assign_Alt-Ergo.mlw
> contains the following goal which I cannot explain:
>
> goal set_state_assign: false
>
> This is my frama-c command
>
> frama-c \
>   -cpp-command 'clang -C -E -I.' \
>   -cpp-extra-args=-nostdinc \
>   -cpp-extra-args=-I`frama-c -print-share-path`/libc \
>   -pp-annot -no-unicode \
>   -wp -wp-rte -wp-model Typed+var+ref+cint+real \
>   -wp-out out -wp-timeout 2000 -wp-fct set_state intstate_ghost.c
>   intstate_ghost.h
>
> I could not find an explanation on the net. Can anybody help me with
> this problem?
>
> Thanks in advance
> Frank
>
>
> ------------------------------
>
> Message: 2
> Date: Wed, 27 May 2015 08:38:12 +0200
> From: BAUDIN Patrick <Patrick.Baudin at cea.fr>
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: Re: [Frama-c-discuss] Assign clauses with ghost variables
> Message-ID: <55656654.8020703 at cea.fr>
> Content-Type: text/plain; charset=windows-1252; format=flowed
>
> Your function does not only assigns the ghost variable!
> That is the explanation.
>
> Patrick.
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
> ------------------------------
>
> End of Frama-c-discuss Digest, Vol 84, Issue 11
> ***********************************************
>