Home My Page Projects The Why platform
Summary Activity Forums Tracker Lists Tasks Docs News SCM Files

[#11387] jessie plugin incorrect translation

Date:
2010-11-03 20:07
Priority:
3
State:
Open
Submitted by:
Alexey Kravets (kayrick)
Assigned to:
Nobody (None)
Hardware:
none
Product:
none
Operating System:
Linux
Component:
none
Version:
none
Severity:
none
Resolution:
none
URL:
Summary:
jessie plugin incorrect translation

Detailed description
I am getting incorrect pvs file while translating file with inductive predicate in annotation.

/*@
@ inductive present_in_tree{L}(struct rb_node * tree,
@ integer value) {
@ case same_nodes{L}:
@ \forall struct rb_node * p_tree;
@ \forall integer p_value;
@ \valid(p_tree) && p_tree->value == p_value
@ ==> present_in_tree (p_tree, p_value);
@ case left_child{L}:
@ \forall struct rb_node * p_tree;
@ \forall integer p_value;
@ \valid(p_tree) && p_tree->value > p_value
@ && present_in_tree (p_tree->rb_left, p_value)
@ ==> present_in_tree (p_tree, p_value);
@ case right_child{L}:
@ \forall struct rb_node * p_tree;
@ \forall integer p_value;
@ \valid(p_tree) && p_tree->value < p_value
@ && present_in_tree (p_tree->rb_right, p_value)
@ ==> present_in_tree (p_tree, p_value);
@ }
@
@
@
@ */

with this annotation I get warnings about recursive definitions (which I definitely have in predicate)


frama-c -jessie -jessie-atp pvs rbtree_stage2.c
[kernel] preprocessing with "gcc -C -E -I. -dD rbtree_stage2.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir rbtree_stage2.jessie
[jessie] File rbtree_stage2.jessie/rbtree_stage2.jc written.
[jessie] File rbtree_stage2.jessie/rbtree_stage2.cloc written.
[jessie] Calling Jessie tool in subdir rbtree_stage2.jessie
Generating Why function rb_search_node
Generating Why function rb_first
Generating Why function rb_last
Generating Why function rb_next
Generating Why function rb_prev
Warning: recursive definition of present_in_tree in generated file
Warning: recursive definition of present_in_tree in generated file
Warning: recursive definition of present_in_tree in generated file
Warning: recursive definition of present_in_tree in generated file
Warning: recursive definition of present_in_tree in generated file
[jessie] Calling VCs generator.
WHYLIB=/usr/local/lib/why why -pvs -dir pvs -pvs-preamble "IMPORTING why@jessie"; -split-user-conj -explain -locs rbtree_stage2.loc /usr/local/lib/why/why/jessie.why why/rbtree_stage2.why

But when I try to proove generated lemmas with PVS

pvs rbtree_stage2.jessie/pvs/rbtree_stage2_why.pvs

I get parse error
Found 'INDUCTIVE' when expecting 'END'

on this
%% Why axiom pointer_addr_of_void_P_of_pointer_address
pointer_addr_of_void_P_of_pointer_address: AXIOM
(FORALL (p: pointer[unit]):
p = pointer_address[void_P](void_P_of_pointer_address(p)))

INDUCTIVE present_in_tree(aux_8:pointer[rb_node], aux_9:int, %%on this line
aux_10:alloc_table[rb_node],
aux_11:memory[rb_node, uint32],
aux_12:memory[rb_node, pointer[rb_node]],
aux_13:memory[rb_node, pointer[rb_node]]) : bool =
(EXISTS (rb_node_tree_1_alloc_table_at_L: alloc_table[rb_node]):
(EXISTS (rb_node_value_0_tree_1_at_L: memory[rb_node, uint32]):

So, steps to reproduce

frama-c -jessie -jessie-atp pvs rbtree_stage2.c

pvs rbtree_stage2.jessie/pvs/rbtree_stage2_why.pvs

And M-x prove in opened emacs window

No Comments Have Been Posted

Attachments:
Size Name Date By Download
5 KiBrbtree_stage2.c2010-11-03 20:07kayrickrbtree_stage2.c
Field Old Value Date By
File Added2020: rbtree_stage2.c2010-11-03 20:07kayrick