--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on May 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Assign clauses with ghost variables



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