Известные проблемы в Krakatoa

Jessie failed, File "jc/jc_pervasives.ml", line 864, characters 6-6:

(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.

Пример, на котором проявляется проблема:

class X {

     public void f(int[] m);

     /*@ requires x != null; */
     public static void test01(X x) {
               x.f(null);
     }
}

Причина в том, что Jessie не умеет работать с nulltype - она пытается определить, на объект какого класса указывает выражение null - параметр метода f в методе test01, и это не получается. Если вместо null написать выражение, тип которого определяется однозначно, проблема не проявляется. Т.е. исправление может быть таким:

class X {

      public void f(int[] m); 

      //@ ghost static int[] _int_arr_null;
      //@ static invariant _null_valid: _int_arr_null == null;

      /*@ requires x != null; */
      public static void test01(X x) {
                    x.f(X._int_arr_null);
      }
}

Krakatoa fatal error, Array struct for type int (name : int) not found

Array struct for type int (name : int) not found: File "", line 0, characters -1--1:

Fatal error: exception Not_found

Пример, на котором проявляется проблема:

class X {
     int[][] mm;
}

Krakatoa пытается свести все массивы к одномерным массивам, выделяя некоторые части типа массива в отдельные новые типы. Например, в данном примере используется ссылка на массив ссылок на массив из чисел, Krakatoa должен представить его как ссылку на массив "структур", где "структура" - это массив чисел. Но делает он это некорректно: предполагает, что "структура" уже сгенерирована и остается только определить тип массива из "структур", а сам не генерирует предварительно "структуру" (массив чисел). Т.е. если Krakatoa перед тем, как встретит двумерный массив, встретит одномерный массив, проблема исчезнет. Т.е. исправление может быть таким:

class X {
     //@ ghost int[] dummy;

     int[][] mm;
}

Последнее изменение: пятница, 29 ноября 2013, 15:12