--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on February 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to annotate list structure in ACSL



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>