Возможности экспериментального образца

Расширенная поддержка строк на уровне спецификаций

Для работы со строками в инструменты верификации были добавлены следующие конструкции.

Именованные литеры

Перед строковой литерой в любом месте исходного кода можно использовать спецификацию вида /*@ id = */ "ab", которая означает объявление в текущей области видимости статической переменной типа const char * const с именем id, для которой определено два глобальных инварианта данных: первый - о содержимом этой переменной вида id[0] == 'a' && id[1] == 'b' && id[3] == '\0', второй - о равенстве адреса этой переменной и адреса того массива char[], который будет использоваться Jessie в коде вместо строковой литеры.

Пример:

char fstr[] = /*@ fstr_literal = */ "String constant";

//@ ghost int initialized = 0;

/*@ global invariant fstr_init:
      ! initialized ==> \forall integer i; \valid(&fstr[i]) ==> fstr[i] == fstr_literal[i];
*/

/*@ requires ! initialized;
  @ ensures initialized &&
  @           (\forall integer i; \valid(&fstr[i]) && i != 6 ==> fstr[i] == fstr_literal[i]) &&
  @           fstr[6] == '_';
  */
void initialize_fstr(void)
{
   fstr[6] = '_';
   //@ ghost initialized = 1;
}

Альтернативный способ задания именованных литер через атрибуты ghost переменных

Этот способ позволяет задавать именованные литеры без глобального инварианта о содержимом (при отсутствии атрибута __invariant).

Пример:

/*@ assigns \nothing;*/
int printf(const char *s, ...);

struct pair {
   int i;
   const char *s;
};

struct pair pair_arr[]  = {
   {1, "First global string"},
   {2, "Second global string"},
   {3, "Third global string"},
   {4, "Fourth global string"},
   {1, "Fifth global string"}
};

const char *str = "global string";
char str2[] = "global string 2";

const char *un = "unique str";

//@ ghost const char * const proxy1 __attribute__ (( __literal )) = "First glob...";
//@ ghost const char * const proxy2 __attribute__ (( __literal (0), __invariant )) = &"Sec...";
//@ ghost const char * const proxy3 __attribute__ (( __literal (0) )) = "Thi";
//@ ghost const char * const proxy4 __attribute__ (( __literal, __invariant )) = &"Four";


int f1(void)
{
   //@ ghost static const char * const proxy5 __attribute__ (( __literal (f1, 0) )) = "First ...";
   //@ ghost static const char * const proxy6 __attribute__ (( __literal (f1, 1) )) = "First ...";

   //@ ghost static const char * const proxy7 __attribute__ (( __literal (f2, 1) )) = "Fif...";
   //@ ghost static const int * const proxy8 __attribute__ (( __literal (f2) )) = L"First...";

   //@ assert proxy5 != \null && proxy7 != \null;

   //@ assert proxy6 != \null && proxy8 != \null;

   const char * s1 = "First local string";
   const char * s2 = "First local string";
   return 0;
}

int f2(void)
{
   const int * s1 = L"First local string";
   const char * s2 = "Fifth global string";
   const char * s3 = "Fifth global string";
   return 1;
}

//@ ghost static const wchar_t * const proxy9 __attribute__ (( __literal, __invariant )) = &L"The semi...";

int main(void)
{
   //@ ghost static const char * const non_proxy10 = "First";
   //@ ghost static const char * const proxy11 __attribute__ (( __literal (f2, 1), __invariant )) = "Fif...";

   //@ assert proxy11[3] == 't';

   //@ assert proxy1 != \null;
   //@ assert proxy2[0] == 'S';
   //@ assert proxy3 != 0;
   //@ assert *proxy4 == 'F';

   //@ assert proxy9[0] == 'T';
   const int * p = L"The seminar was completely screwed up!";
   printf("%s %S", "ssss");
}

Шаблонные спецификации для некоторых стандартных функций работы с памятью

Модель памяти инструментов верификации отличается от физической. В исходном коде, например, можно осуществлять побайтовое копирование структур. Для этого выполняет преобразование указателя на структуру в указатель (void *) или (char *). В модели памяти инструментов верификации подобное преобразование происходит с потерей информации: в их модели памяти отсутствует связь между представлением структуры как набора полей определённого типа и её представлением в виде отдельных байт. Выражение подобной связи чрезвычайно усложняет моделирование. Для того, чтобы в коде можно было использовать и описывать в инструменты верификации добавляются шаблонные спецификации.

Шаблонные спецификации записываются на функцию со специальным именем вида fname__type, например void *memset__type(_type *dest, int val, size_t n);. Вместо соответствующих функций без __type (например, memset) подставляются функции с именем типа (например, memcpy_int или memset_struct_s). Спецификации последних получаются из спецификаций в файле jessie_spec_prolog.h путём подстановки соответствующего типа вместо __type.

Например:

/*@ requires n >= 0 &&
  @          n % (sizeof (_type)) == 0 &&
  @          \let _n = n / sizeof (_type);
  @          \valid(((_type *) dest)+(0 .. _n - 1)) &&
  @          \valid(((_type *) src)+(0 .. _n - 1)) &&
  @          separated__type{Pre, Pre}((_type *) dest,(_type *) src, n);
  @ assigns ((_type *) dest)[0 .. (n / sizeof (_type)) - 1] \from ((_type *) src)[0 .. (n / sizeof (_type)) - 1];
  @ allocates \nothing;
  @ ensures memcmp__type{Here, Here}((_type *) dest, (_type *) src, n) && \result == dest;
  @*/
extern _type *memcpy__type(_type *restrict dest, const _type *restrict src, size_t n);

Как можно видеть на примере данной спецификации, также возможно описывать шаблонные предикаты, например:

/*@ axiomatic memcpy__type {
  @   predicate memcmp__type{L1, L2}(_type *p1, _type *p2, size_t n) =
  @     n % (sizeof (_type)) == 0 &&
  @     \let _n = n / sizeof (_type);
  @     \valid{L1}(((_type *) p1)+(0 .. _n - 1)) &&
  @     \valid{L2}(((_type *) p2)+(0 .. _n - 1)) &&
  @     \forall integer k; 0 <= k="" _n="="> \at(p1[k], L1) == \at(p2[k], L2); @ } */ 

И использовать их в собственном коде, предварительно импортировав:

/*@ axiomatic memcmps {
  @   predicate memcmp_int{L1, L2}(int *a, int *b, size_t n);
  @   //predicate separated_int(int *a, int *b, unsigned int n);
  @ }
  @*/

int main(void)
{
   int *a, *b;
   a = malloc(sizeof (int));
   b = malloc(sizeof (int));
   memcpy(a, b, sizeof (int));
   //@ assert memcmp_int{Here, Here}(a, b, (unsigned long long) sizeof (int));
   return 0;
}

Шаблонные спецификации доступны по опции -jessie-specialize. Опция включена по умолчанию. Шаблоны хранятся в файле frama-c-plugin/share/jessie/jessie_spec_prolog.h и устанавливаются в файл $(PLUGIN_DIR)/share/jessie/ (PLUGIN_DIR, например, /usr/local/share/frama-c/).

Список функций с шаблонными спецификациями:

Поддержка функциональных указателей

Поддержка указателей на функции осуществляется через специальные фиктивные адреса. В модель памяти инструментов добавляются специальные адреса, в которых хранится информация о функциях, расширяется модельная операция сравнения функциональных указателей. Модель памяти в инструментах верификации не соответствует модели памяти физического компьютера, в ней не выполняется принцип хранения данных и инструкций в одной памяти архитектуры фон Неймана.

Следствием этого, а также того, что дедуктивная верификация - это статический метод, является то, что в спецификации функции, вызывающей функции по указателю, необходимо явно указывать все возможные функции, которые можно вызвать по указателю.

Пример:

/*@ requires (\typeof(p) <: \type(char *) ==> \valid((const char *)p)) && \valid(s) && flag1 == flag2 == 0;
  @ ensures \result == 0;
  @
 */
extern int dummy_callback1(int flag1, int flag2, void *p, const char *s);

/*@ requires (\typeof(p) <: \type(char *) ==> \valid((const char *)p)) && \valid(s) && flag1 == flag2 == 0;
  @ ensures \result == 0;
  @
 */
extern int dummy_callback2(int flag1, int flag2, void *p, const char *s);

/*@ ensures \result == 0;
 */
extern int dummy_callback3();

typedef int (*callback_t) (int, int, void *, const char *);

struct callbacks {
   callback_t cb1;
   int (*cb2) (void);
};

struct outer {
   struct callbacks *cbs;
};

/*@ requires \valid(pouter) && \valid(pouter->cbs);
  @ requires pouter->cbs->cb1 == &dummy_callback1 || pouter->cbs->cb1 == &dummy_callback2;
  @ requires pouter->cbs->cb2 == (int (*)(void))&dummy_callback3;
  @ ensures \result == 0;
*/
int caller (struct outer *pouter)
{
   char *s = "const char ";
   return pouter->cbs->cb1(0, 0, s, "const char") || pouter->cbs->cb2();
}

Расширенная поддержка побитовой арифметики на уровне спецификационных операций

На уровне спецификаций используются неограниченные числа, в то время как диапазон целого числа в языке Си ограничен его типом. Если в какой-то момент в ходе математических операций происходит выход за пределы диапазона, это влечёт за собой ошибку, известную как "целочисленное переполнение". Согласно стандарту C99, при целочисленном переполнении компилятор может вести себя как угодно. Согласно стандарту, если переменная unsigned типа не может вместить в себя какое то значение, то происходит следующее преобразование: usigned_toobig_number = usigned_toobig_number % (unsigned_max_value+1) Однако, для знаковой арифметики подобное преобразование не всегда имеет место быть.

Ошибка переполнения целого числа сама по себе не очень опасна, опасны возможные последствия к которым она может привести. Это, например, выход за пределы границ массива, если ошибка произошла в переменной, в которой хранится индекс массива:

int avr(int a, int b) { return (a + b) / 2 }
int bsearch(int a[], int size, int val) {
   int l = 0, h = size - 1;
   ...
   int mval = a[avr(l, h)];
   ...
}

Так как арифметическое переполнение считается ошибкой, то инструментами верификации генерируются условия верификации, связанные с ним. Это заложено в модели целых чисел, которая используется инструментами. Чтобы доказать полную корректность кода, необходимо показать отсутствие в нём ошибок, связанных с переполнением. Однако, существует ряд алгоритмов, которые целенаправленно используют указанные особенности переполнения чисел. Подобные алгоритмы широко распространены, например, в криптографии. Часть стандартных функций также иногда реализуются через манипуляцию с битовой арифметикой с целью оптимизации и уменьшения ветвлений:

unsigned abs(int x) {
   int const mask = x >> sizeof(int) * CHAR_BIT - 1;
   return ((x + mask) ^ mask);
}

Соответственно, так как в таких случаях не нужно генерировать условие верификации на переполнение, то необходимо явно сообщить об этом инструменту. В таких случается к знаку операции на уровне спецификаций приписывается %. Например:

a + /*@%*/ b;
a >> /*@%*/ b;

Если же в самих спецификациях требуется выразить операцию по модулю на целых числах, то сначала необходимо записать явно перетипирование от неограниченных чисел в тип языка Си, во вторых использовать знак арифметической операции с суффиксом в виде %, для битовых операций этого не требуется: //@ assert (((int ) 334553453 +% (int) 3487934) | ~(int)434511) == -41285;

Также в спецификация можно использовать приведения типов специального вида, как можно увидеть в предыдущем примере. Например, (int %) - приведение к int32 с возможностью переполнения, то есть дополнение битвектора нулями слева (транслируется в операцию конкатенации битвекторов). Если же написать просто (int), то будет двойное приведение - сначала к типу неограниченному integer, а потом к int32 (транслируется в пару применений не интерпретируемых функций of_int/to_int). В коде приведение типа всегда транслируется сразу в обе операции (с возможным добавлением проверки переполнения).

Переинтерпретация типа указателя между целочисленными типами, в том числе разного размера

В системном коде, как, например, в коде ядра операционной системы, часто используется перетипизация указателей. Чаще всего в случаях, когда происходит сериализация/десериализация структур данных при считывании аргументов системных вызовов, атрибутов файловых систем, пользовательских данных. В языке Си для этого используется явное приведение типа, что легко отражается на физическую модель памяти. Однако, инструменты верификации используют другую модель памяти, в которой структуры данных представлены не просто набором байт, разные типы обрабатываются по разному и не могут свободно преобразовываться друг к другу.

Для того, чтобы указать инструментам верификации что определённую память с какого-то момента следует рассматривать как память другого типа используется конструкция //@ jessie pragma __mem__ :> __type__. Ввиду ограничений текущей модели памяти подобное преобразование только для целочисленных типов.

Пример:

/*@ requires n >= 0 && \valid(p + (0..n-1));
 */
void int_access(int *p, int n) {
   if (n > 0)
      p[n-1] = 0;
}

void example(void) {
   int p[1000];

   //@ jessie pragma p :> char *;
   // Теперь к памяти, на которую указывает p можно обращаться как
   // к массиву char размером 4000,
   // но нельзя - как к массиву int (то есть p не валиден, в
   // то время как (char *)p - валиден).
   char *q = (char *) p;
   //@ assert \base_addr(q) == q;
   //@ assert \valid(q + (0..3999));
   //@ jessie pragma q :> int *;

   // Теперь к (int *)q (и, например, к p) можно снова обращаться
   // как к массиву char (но не как к массиву int).
   // При этом значения по соответствующим адресам памяти
   // соответствующим образом преобразуются
   // (учитывая endianness, с которым запущена Frama-c).

   int_access(p, 1);
}

Явное указание типа на уровне спецификаций

Зачастую в коде используется указатель 'void *', что эквивалентно типу 'char *' и означает указатель на участок памяти, который следует рассматривать как набор байт. Дальше по коду этот указатель может приводиться к структуре и последующая работа будет вестись уже с другим типом. Подобная ситуация означает, что в коде неявно заложена информация о типе участка памяти. При преобразовании типа возможна ошибка, когда новый тип не вмешается в тот участок памяти, который до этого рассматривался как простой набор байт.

На уровне спецификаций можно явно указать к какому типу возможно приводить память по указателю 'void *'. В таком случае также будет проверяться, что размер выделенной памяти достаточен для того, чтобы вместить в него желаемую структуру.

Пример:

struct s { int a; int b};
/*@ requires \typeof(m) <: \type(struct *s);
    requires \valid(m+(0..n-1));
 */
int f(void *m, size_t n) {
   struct s *t = (struct s *) m;
   ...
}

Импорт лемм

Когда одновременно верифицируется большой объём кода, солверам приходится делать большое количество шагов, чтобы доказать одно утверждение, потому как модель детализируется и усложняется. Если при доказательстве спецификации функции необходимо использовать какую-то конкретную лемму, то ранее солверам необходимо было угадывать путём подбора, какую именно лемму из множества сформулированных лучше использовать. Зачастую, при увеличении объёма верифицируемого кода, солверы переставали укладываться в заданные временные интервалы, и ранее доказываемые утверждения на меньшем объеме кода, в данном случае переставали доказываться. Для того, чтобы указать какие леммы использовать при доказательстве спецификаций определённых функций балы добавлена возможность импорта лемм. Леммы, которые определены вне конструкции axiomatic автоматически импортируются всеми спецификациями, то есть добавляются в модели верификационных условий, которые подаются на вход автоматических солверам. Леммы, определённые в аксиоматиках по умолчанию не включаются ни в какие-модели. Однако потребность в них для доказательства конкретной спецификации можно явно указать, используя какое-либо определение функции или предиката из того же аксиоматика, например:

/*@ axiomatic lemma1 {
  @   lemma lemma1: \true != \false;
  @   predicate lemma1 = \true;
  @ }
  @*/

/*@ axiomatic axs {
  @   logic boolean prd;
  @   axiom ax1: prd == \true;
  @   lemma lemma2: prd == \true ;
  @ }
  @*/

//@ requires lemma1;
int main(void)
{
   return 0;
}

В примере для функции main будет импортирована лемма lemma1, но не lemma2.

Поддержка произвольного порядка определений логических сущностей

Изначально инструменты поддерживали исключительно прямой порядок определения логических сущностей (функций, предикатов, типов, конструкторов и модельных полей). Это означает, что для того чтобы использовать, например, какой-либо предикат в спецификации для функции, он должен быть определён выше по коду. Точно такой же порядок используется в самом языке Си. В инструменты была добавлена поддержка произвольного порядка определения логических сущностей. Кроме того, в язык ACSL были добавлены две новые конструкции для импорта логических сущностей из других файлов: //@ import "имя файла" (имя1, имя2, ..., имяn); и её альтернативная форма //@ import "имя файла" (*); Обе конструкции могут использоваться в любом месте файла, где допустима глобальная логическая декларация. Первая из них позволяет использовать в некотором файле, подаваемом на вход внешнему интерфейсу Frama-C, логические сущности с именами имя1, имя2, ..., имяn, определенные в файле с именем "имя файла", который также подается на вход Frama-C, и имя которого в командной строке Frama-C в точности совпадает с указанным (это позволяет использовать, к примеру, имена "../file.c", "d/file.c", "../d/file.c" и т.д). Импортируемые имена не различаются по видам и типам, то есть указание, к примеру, имени some_name, импортирует сразу и функции, и предикаты, и типы, и конструкторы с этим именем, причем в случае с перегруженными функциями/предикатами импортируются все определения с одинаковым именем. Перегрузка функций поддерживается только внутри одного файла, нет возможности, к примеру, импортировать одну из перегруженных функций из одного файла, а другую -- из другого или перегрузить уже импортированную функцию. Конфликты имен при импортировании не допускаются, порядок импортирования значения не имеет. Конструкция импортирования "по требованию" (*) импортирует из указанного файла все имена, которые не определены в импортирующем файле, однако другие импортирования при этом не учитываются и при повторении импортируемых имен будет возникать конфликт.

type имя_типа

Альтернативный способ указания имени типа. Используется с импортированными типами или типами, которые определяются после их использования. Решает проблему с неоднозначной грамматикой ACSL, в которой конфликт между именами типов и идентификаторами (например, именами конструкторов) разрешается прямо во время синтаксического разбора с помощью хеш-таблицы ранее объявленных имен типов. Например, по умолчанию:

//@ type a = b;
//@ type b = Max | Min;

разбирается как два алгебраических типа с конструкторами b, Min и Max соответственно. Чтобы сделать a синонимом b можно указать:

//@ type a = type b;
//@ type b = Max | Min;

Поддержка container_of

Макрос container_of - это макрос специального вида, который широко используется в ядре Linux:

#ifdef __compiler_offsetof
#define offsetof(TYPE, MEMBER)  __compiler_offsetof(TYPE, MEMBER)
#else
#define offsetof(TYPE, MEMBER)  ((size_t)&((TYPE *)0)->MEMBER)
#endif

/**
 * container_of - привести указатель на на поле структуры к объемлющей его структуре
 * @ptr:        указатель на поле структуры.
 * @type:       тип объемлющей структуры.
 * @member:     имя поля структуры, на которую ссылается указатель.
 *
 */
#define container_of(ptr, type, member) ({                      \
        const typeof( ((type *)0)->member ) *__mptr = (ptr);    \
        (type *)( (char *)__mptr - offsetof(type,member) );})

container_of выражается через offsetof. offsetof возвращает смещение в байтах от начала структуры для одного из её полей. В инструменты верификации была добавлена поддержка container_of и он может использоваться в спецификациях. В спецификациях макрос offsetof не подставляется, а разбирается как конструкция. При выделениях памяти соответствующие предикаты добавляются только для тех вложенных структур, для которых где-либо в спецификациях встречается соответствующий offsetof.

Поддержка возвращения ошибки в kmalloc

Функция kmalloc - стандартная функция выделения памяти в ядре Linux. Функции выделения и освобождения памяти инструментами верификации обрабатываются специальным образом. Спецификации на них содержатся в моделях памяти самих инструментов. Стандартная спецификация на malloc, заложенная в инструментах, всегда предполагает что память успешно выделяется. Однако, в реальности это может быть не так. В коде ядра операционной системы особенно важно обрабатывать ситуации, когда память не может быть выделена, так как в обратном случае это может сказаться на стабильности работы операционной системы. Инструменты были расширены с целью поддержки операций выделения/освобождения памяти kmalloc/kfree, причём kmalloc может возвращать NULL.

Поддержка asm и asm goto в С-коде

Достаточно часто функции содержат вставки ассемблерного кода. Инструменты верификации не предназначены для работы с ним. Верификация таких функций на текущей момент не возможна и не предполагается. Однако в коде, подаваемом на вход инструментам верификации могут содержаться ассемблерные вставки по той причине, что он содержится в отдельных функциях в заголовочных функциях ядра. Последние никак не используются и не вызываются из функций, дедуктивная верификация которых производится. В инструменты верификации была добавлена возможность разбора синтаксических конструкций ассемблерных вставок и расширения gcc по поддержке asm goto конструкций, которые также используются в коде ядра Linux. Сталкиваясь с подобными конструкциями инструменты верификации расценивают их как вызов подставных функции с вырожденным предусловием \false.

Экстрактор кода

Быстродействие инструментов верификации зависит от объёма кода, с которым они работают, так как любая новая сущность в коде влечёт за собой усложнение и разрастание моделей, которые порождаются инструментами при работе. Однако, не всегда весь код, который подаётся инструментам на вход содержит спецификации (предусловия, постусловия, спецификации иного вида), не всегда весь код даже связан вызовами функций. В таком случае, возможно отбросить на каком-то из промежуточных этапов тот код, который не содержит спецификаций, без потери в качестве анализа, зато сильно упростив модели, которые подаются на вход автоматическим солверам и значительно увеличив итоговое быстродействие самих инструментов. Данная функциональность была реализована в инструментах и доступна по опции -jessie-extract. Экстрактор включён по умолчанию. Он убирает функции, которые не имеют спецификаций, убирает структуры, которые не используются, заменяет неиспользуемые поля структур на соответствующее количеством байт, ими занимаемых, и производит иные операции упрощения кода, которые не влияют на качество и корректность дедуктивной верификации.

Массивы нулевой длины

В ядре Linux распространено использование расширений GCC стандартов языка C. Одним из таких расширений являются массивы нулевой длины. Они используются как последний элемент в структуре, которая является заголовком для объекта произвольной длины.

struct line {
   int length;
   char contents[0];
};

В инструменты верификации была добавлена поддержка данного расширения. Массивы нулевой длины в конце структуры интерпретируется так же, как и открытые массивы int arr[]. Не поддерживается доказательство валидности памяти таких массивов после выделения соответствующих структур.

Специальные предикаты вида uintdd_unitdd

Модель памяти в инструментах верификации не содержит в себе побайтового представления типов. Поэтому когда требуется узнать, как раскладываются значения многобайтовых типов на значения типов меньшего размера байт возникает ситуация, что нельзя формально показать соответствие. Для решения подобной проблемы в частном случае использования целочисленных типов в инструменты были добавлены предикаты специального вида.

Пример:

// Импортирование предиката.
// Предикат возвращает true, если соответствующая двухбайтная переменная a
// раскладывается на две однобайтных переменных a1 и a2 в соответствии с порядком байт,
// используемой данной компьютерной архитектурой.
/*@ axiomatic casts {
  @   predicate uint16_as_uint8(unsigned short a, unsigned char a1, unsigned char a2);
  @ }
  @*/

/*@ requires \typeof(p) <: \type(unsigned short *) && \valid((unsigned short *)p);
  @ allocates \nothing;
  @ assigns *((unsigned short *)p);
  @ ensures uint16_as_uint8(*(unsigned short *)p, (unsigned char) (v & (unsigned short)0xff), (unsigned char) ((v >> (unsigned short)8) & (unsigned short)0xff));
  @*/
void set_w16(void *p, unsigned short v)
{
   //@ jessie pragma ((unsigned short *) p) :> unsigned char *;
   unsigned char *ptr = (unsigned char *) p;

   ptr[0] = v & 0xff;
   ptr[1] = (v >> 8) & 0xff;
   //@ jessie pragma ptr :> unsigned short *;
   /*@ assert \forall unsigned short *q; \base_addr(q) == \base_addr(p) ==>
     @        (0 <= p - q <= 0 <==> p == q);
     @*/
}

Инструментами поддерживаются следующие предикаты:

Улучшения интерактивной среды Why3ide

Подсветка потока управления для условий верификации

При порождении моделей для условий верификации в них закладывается путь, который прошёл поток управления в коде до "места проверки". Так как в коде могут имеется ветвления, то зачастую возникает ситуация, когда одни и те же условия верификации проверяются на разных путях управления. Если для одного из таких условий верификации не удаётся доказать выполнимость, то имеется вероятность того, что в коде на данном пути содержится ошибка. Для упрощения работы человека, осуществляющего дедуктивную верификации кода, каждая точка возможного ветвления пути подсвечивается специальным образом. Красный цвет означает, что условие не выполнено, зелёный - выполнено. Жёлтым цветом подсвечивается спецификации, выполнимость которых инструмент пытается доказать.

Скрытие пустых теорий

В Why3 IDE по умолчанию скрываются пустые (без VC) теории/модули, их можно показать через меню View->Hide theories/modules without goals или по сочетанию клавиш Ctrl-h.

Поиск по моделям

В Why3 IDE в окне Task добавлена возможности искать и подсвечивать вхождения выделенного идентификатора (новое меню Edit в окне Task и комбинаций клавиш Ctrl-m, Ctrl-f, Ctrl-g, Ctrl-G, ESC)

Автономный (headless) запуск доказательств

В инструменты верификации добавлена возможность запуска процесса верификации без запуска интерактивной среды Why3Ide. Это часто бывает необходимо для передоказательства на новом коде уже ранее доказанных спецификаций. В таком случае в командной строке указывается -jessie-target why3prove, параметры преобразований и использование солверов также регулируются опциями командной строки.

Пример:

$ frama-c -jessie -jessie-target why3prove -jessie-why3-opt "\ -a split_goal_wp -P alt-ergo" test.c