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] How to annotate list structure in ACSL

  • Subject: [Frama-c-discuss] How to annotate list structure in ACSL
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Thu, 27 Feb 2014 00:46:21 -0500
Hi all,
?? I come across some problem when I try to annotate list structure using ACSL. The "acsl mini-tutorial" seems to be clear about it. it provides sample code,? as shown below.

typedef struct _list { int element; struct _list* next; } list;

/*@
inductive reachable{L} (list* root, list* node) {
? case root_reachable{L}:
????? \forall list* root; reachable(root,root);
? case next_reachable{L}:
????? \forall list* root, *node; \valid(root) ==> reachable(root->next, node) ==>reachable(root,node);
}
*/

??? I copied this code and annotated a simply function in_list(), that is attached in llist.c, I got this output:

$ frama-c -wp -wp-prover z3 llist.c 
[kernel] preprocessing with "gcc -C -E -I.? llist.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
llist.c:16:[wp] warning: Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
File "/tmp/wp9365c2.dir/typed/Axiomatic.why", line 15, characters 47-72:
Bad arity: symbol p_reachable must be applied to 4 arguments, but is applied to 2
------------------------------------------------------------
[wp] [Z3] Goal typed_in_list_post : Failed
???? Error: Why3 exits with status [1]


??? Any idea on how to correct the error? Thank you.

Xiao-lei 		 	   		  
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: llist.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140227/d0ea8834/attachment.c>