--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on May 2015 ---
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