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

[Frama-c-discuss] inductive annotations on list structure



Hi all,
?? I followed ACSL-mini Tutorial chapter 8, as I annotate linked-list structure. ? 

?? The error message followed was reported by WP:

-----------------------------
[kernel] preprocessing with "gcc -C -E -nostdinc -I/home/cuix/projects/workspace/acsl_szos/h \
???????????????? -I/home/cuix/projects/workspace/acsl_szos/h/kernel -DCPU=SPARC_V7 -Dfor_jessie? -dD src/util/dllremove1.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
File "/tmp/wp8d3f1a.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_dll_remove_post : Failed
???? Error: Why3 exits with status [1]
------------------------------

?? Not very clear about the error message. And I can not find anything suspicious in the code, which is attached. I removed the function body for simplicity.
?? Any clues? 
?? Thanks very much.

xiaolei 		 	   		  
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: list_remove.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140217/b6d3c336/attachment.c>