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

[#11466] [jessie] Incorrect loop translation (mutable_*)

Date:
2010-11-24 11:43
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] Incorrect loop translation (mutable_*)

Detailed description
For this
while ((parent = rb_parent(node)) && node == parent->rb_right)
node = parent;


jessie generates safety obligation like this:


node_0: rb_node pointer
rb_node_node_25_alloc_table: rb_node alloc_table
rb_node_rb_right_node_25: (rb_node, rb_node pointer) memory
rb_node_rb_parent_node_25: (rb_node, rb_node pointer) memory
H1: (offset_min(rb_node_node_25_alloc_table, node_0) <= 0 and
offset_max(rb_node_node_25_alloc_table, node_0) >= 0 and
(forall node1:rb_node pointer.
(forall node2:rb_node pointer. same_block(node1, node2))))
H5: offset_min(rb_node_node_25_alloc_table, node_0) <= 0 and
0 <= offset_max(rb_node_node_25_alloc_table, node_0)
result: rb_node pointer
H6: result = select(rb_node_rb_parent_node_25, node_0)
H7: same_block(result, node_0) or result = null or node_0 = null
H11: result <> node_0
H12: offset_min(rb_node_node_25_alloc_table, node_0) <= 0 and
0 <= offset_max(rb_node_node_25_alloc_table, node_0)
result0: rb_node pointer
H13: result0 = select(rb_node_rb_right_node_25, node_0)
H14: same_block(result0, null) or result0 = null or null = null
H31: result0 = null
mutable_node_0: rb_node pointer
H32: true

----------
offset_min(rb_node_node_25_alloc_table, mutable_node_0) <= 0]



So, we have no information about mutable_mode_0.


But, if we replace this loop with equal one

parent = rb_parent (node);
while (parent)
{
if (node != parent->rb_right)
break;
node = parent;
}

Everything seems fine (alt-ergo can proove generated obligation):

node_0: rb_node pointer
rb_node_node_25_alloc_table: rb_node alloc_table
rb_node_rb_right_node_25: (rb_node, rb_node pointer) memory
rb_node_rb_parent_node_25: (rb_node, rb_node pointer) memory
H1: (offset_min(rb_node_node_25_alloc_table, node_0) <= 0 and
offset_max(rb_node_node_25_alloc_table, node_0) >= 0 and
(forall node1:rb_node pointer.
(forall node2:rb_node pointer. same_block(node1, node2))))
H5: offset_min(rb_node_node_25_alloc_table, node_0) <= 0 and
0 <= offset_max(rb_node_node_25_alloc_table, node_0)
result: rb_node pointer
H6: result = select(rb_node_rb_parent_node_25, node_0)
H7: same_block(result, node_0) or result = null or node_0 = null
H11: result <> node_0
H12: offset_min(rb_node_node_25_alloc_table, node_0) <= 0 and
0 <= offset_max(rb_node_node_25_alloc_table, node_0)
result0: rb_node pointer
H13: result0 = select(rb_node_rb_right_node_25, node_0)
H14: same_block(result0, null) or result0 = null or null = null
H31: result0 = null
H32: offset_min(rb_node_node_25_alloc_table, node_0) <= 0 and
0 <= offset_max(rb_node_node_25_alloc_table, node_0)
result1: rb_node pointer
H33: result1 = select(rb_node_rb_parent_node_25, node_0)
parent_5: rb_node pointer
H34: parent_5 = result1
H35: true
H37: same_block(parent_5, null) or parent_5 = null or null = null
H38: parent_5 <> null

-----------
offset_min(rb_node_node_25_alloc_table, parent_5) <= 0
Message  ↓
Date: 2010-11-24 12:21
Sender: Alexey Kravets

FIX typo in example

parent = rb_parent (node);
while (parent)
{
if (node != parent->rb_right)
break;
node = parent;
parent = node->rb_parent;
}

No Changes Have Been Made to This Item