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

[#9608] [Jessie/Krakatoa]: alloc_extends missing after constructor call

Date:
2010-02-12 19:23
Priority:
3
State:
Open
Submitted by:
Peter Trommler (trp)
Assigned to:
Nobody (None)
Hardware:
PC
Product:
none
Operating System:
Linux
Component:
none
Version:
none
Severity:
normal
Resolution:
none
URL:
Summary:
[Jessie/Krakatoa]: alloc_extends missing after constructor call

Detailed description
SimpleApplet contains code to install a Java Card Applet in Global Platform
compliant manner. The constructor allocates a single byte array.

Running
$krakatoa #(v2.23)
$jessie
$make -f SimpleApplet.makefile coq

produces the attached SimpleApplet_why.v for Coq.

In proof obligation SimpleApplet_install_safety_po_5 (see below)
there is no alloc_extends predicate for Object_alloc_table1 at (* here *).
So the PO cannot be discharged.

Everything is fine when we remove the allocation from the constructor of
SimpleApplet.

Extract from SimpleApplet_why.v
(* Why obligation from file "SimpleApplet.jc", line 150, characters 44-81: *)
(*Why goal*) Lemma SimpleApplet_install_safety_po_5 :
forall (bArray_1: (pointer Object)),
forall (bOffset_1: short),
forall (bLength_1: byte),
forall (Object_alloc_table: (alloc_table Object)),
forall (HW_1: (left_valid_struct_byteM bArray_1 0 Object_alloc_table) /\
(* JC_127 *)
((* JC_121 *) (Non_null_byteM bArray_1 Object_alloc_table) /\
(* JC_122 *)
((offset_max Object_alloc_table bArray_1) + 1) <= 32767 /\
(* JC_123 *) (integer_of_short bOffset_1) >= 0 /\
(* JC_124 *) (integer_of_short bOffset_1) <
((offset_max Object_alloc_table bArray_1) + 1) /\
(* JC_125 *) (integer_of_byte bLength_1) <= 127 /\
(* JC_126 *) (integer_of_byte bLength_1) >= 0)),
forall (HW_2: 1 >= 0),
forall (result: (pointer Object)),
forall (Object_alloc_table0: (alloc_table Object)),
forall (Object_tag_table: (tag_table Object)),
forall (HW_3: (strict_valid_struct_SimpleApplet
result 0 (1 - 1) Object_alloc_table0) /\
(alloc_extends Object_alloc_table Object_alloc_table0) /\
(alloc_fresh Object_alloc_table result 1) /\
(instanceof Object_tag_table result SimpleApplet_tag)),
forall (HW_4: (offset_max Object_alloc_table0 result) >= 0),
forall (Object_alloc_table1: (alloc_table Object)),
(* here *)
forall (HW_6: (-2147483648) <= ((integer_of_short bOffset_1) + 1) /\
((integer_of_short bOffset_1) + 1) <= 2147483647),
forall (result0: int32),
forall (HW_7: (integer_of_int32 result0) =
((integer_of_short bOffset_1) + 1)),
forall (HW_8: (-32768) <= (integer_of_int32 result0) /\
(integer_of_int32 result0) <= 32767),
forall (result1: short),
forall (HW_9: (integer_of_short result1) = (integer_of_int32 result0)),
((offset_min Object_alloc_table1 bArray_1) <=
(integer_of_short bOffset_1) /\ (integer_of_short bOffset_1) <=
(offset_max Object_alloc_table1 bArray_1)).
Proof.
intuition.
(* FILL PROOF HERE *)
Save.

No Comments Have Been Posted

Attachments:
Size Name Date By Download
990 bytesSimpleApplet.java2010-02-12 19:23trpSimpleApplet.java
32 KiBSimpleApplet_why.v2010-02-12 19:23trpSimpleApplet_why.v
10 KiBkrakatoa.log2010-02-12 19:23trpkrakatoa.log
34 KiBjessie.log2010-02-12 19:23trpjessie.log
Field Old Value Date By
File Added1717: SimpleApplet.java2010-02-12 19:23trp
File Added1718: SimpleApplet_why.v2010-02-12 19:23trp
File Added1719: krakatoa.log2010-02-12 19:23trp
File Added1720: jessie.log2010-02-12 19:23trp