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)
- Follow-Ups:
- [Frama-c-discuss] Behavior specification with ghost variables
- From: anne.pacalet at free.fr (Anne Pacalet)
- [Frama-c-discuss] Behavior specification with ghost variables
- Prev by Date: [Frama-c-discuss] Opening GUI on a specific file and function?
- Next by Date: [Frama-c-discuss] Internal state represented by ghost variable not provable
- Previous by thread: [Frama-c-discuss] Opening GUI on a specific file and function?
- Next by thread: [Frama-c-discuss] Behavior specification with ghost variables
- Index(es):