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

[#15964] [Krakatoa] Assertion failure while using "null"

Date:
2013-06-28 22:15
Priority:
3
State:
Open
Submitted by:
Eugene Kornykhin (kornevgen)
Assigned to:
Claude Marché (marche)
Hardware:
none
Product:
none
Operating System:
Linux
Component:
none
Version:
none
Severity:
none
Resolution:
Accepted As Bug
URL:
Summary:
[Krakatoa] Assertion failure while using "null"

Detailed description
Why3 platform, version 0.81 (build date: Mon Jun 10 01:23:58 MSK 2013)
Krakatoa / Jessie version 2.33, compiled on Mon Jun 10 01:20:29 MSK 2013

class A {
public void f() {
Object x = null;
}
}

Warning: A is not a subpackage of .
Parsing OK.
Typing OK.
Generating JC function A_f for method A.f
Generating JC function cons_A for constructor A
Done.
Calling Jessie...
Generating Why function A_f
(nulltype)
File "jc/jc_pervasives.ml", line 864, characters 6-6:
Uncaught exception: File "jc/jc_pervasives.ml", line 864, characters 6-12: Assertion failed
Jessie failed, abort.

No Comments Have Been Posted

Field Old Value Date By
assigned_tonone2014-02-12 20:21marche
ResolutionNone2014-02-12 20:21marche