--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on April 2014 ---
The behaviour of the function I am trying to specify with ACSL depends on the value that is returned by a call to a lower level function that is not visible at the point of declaration. I use a ghost variable to alias this internal value and use that ghost variable in the assume clauses of the behavior specifications, as shown here: // file: ifbvr.h //@ ghost int inp; /*@ @ behavior Higher: @ assumes inp >= 0; @ ensures \result == 'p'; @ behavior Lower: @ assumes inp < 0; @ ensures \result == 'n'; @ complete behaviors; @ disjoint behaviors; @*/ char foo (); In the definition of the function, I equate the ghost variable with the internal variable as shown in the code below: // file: ifbhv.c #include "ifbhv.h" extern int getval(); char foo () { int iv; char retv; iv = getval(); //@ ghost inp = iv; if (iv >= 0) { //@ assert inp >= 0; retv = 'p'; } else { //@ assert inp < 0; retv = 'n'; } //@ assert (inp >= 0 ) ==> (retv == 'p'); //@ assert (inp < 0 ) ==> (retv == 'n'); return retv; } When I try to prove this with the wp plugin, all assertions are proven, but not the post conditions of the two ensure clauses in the behavior clauses. What is the reason for that? And, is there a better way to specify a function for which its behavior depends on internal values? Here is my frama-c call with log: frama-c -cpp-command 'clang -C -E -I.' -cpp-extra-args=-nostdinc -cpp-extra-args=-I`frama-c -print-share-path`/libc -wp -wp-rte -pp-annot ifbhv.c [kernel] preprocessing with "clang -C -E -I. -I/usr/share/frama-c/libc -nostdinc -dD ifbhv.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function foo [kernel] warning: Neither code nor specification for function getval, generating default assigns from the prototype [wp] 8 goals scheduled [wp] [Qed] Goal typed_foo_complete_Lower_Higher : Valid [wp] [Qed] Goal typed_foo_disjoint_Lower_Higher : Valid [wp] [Qed] Goal typed_foo_assert : Valid [wp] [Qed] Goal typed_foo_assert_2 : Valid [wp] [Qed] Goal typed_foo_assert_3 : Valid (3ms) [wp] [Qed] Goal typed_foo_assert_4 : Valid [wp] [Alt-Ergo] Goal typed_foo_Lower_post : Unknown (Qed:3ms) [wp] [Alt-Ergo] Goal typed_foo_Higher_post : Unknown (Qed:3ms)