--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on February 2014 ---
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>