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] Behavior specification with ghost variables

  • Subject: [Frama-c-discuss] Behavior specification with ghost variables
  • From: frank at dordowsky.de (Frank Dordowsky)
  • Date: Sun, 27 Apr 2014 20:58:22 +0200 (CEST)
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)