Объявления логической структуры ACSL не работают, как в справочном руководстве

Я хотел бы иметь способ описать структуры уровня логики/спецификации, которые включают абстрактные списки. Пример 2.2.7 на странице 27 Справочное руководство ACSL предполагает, что существует способ сделать это, и это выглядит следующим образом:

//@ type point = struct { real x; real y; };
//@ type triangle = point[3];
//@ logic point origin = { .x = 0.0 , .y = 0.0 };
/*@ logic triangle t_iso = { [0] = origin,
@ [1] = { .y = 2.0 , .x = 0.0 }
@ [2] = { .x = 2.0 , .y = 0.0 }};
@*/
/*@ logic point centroid(triangle t) = {
@ .x = mean3(t[0].x,t[1].x,t[2].x);
@ .y = mean3(t[0].y,t[1].y,t[2].y);
@ };
@*/
//@ type polygon = point[];
/*@ logic perimeter(polygon p) =
@ \sum(0,\length(p)-1,\lambda integer i;d(p[i],p[(i+1) % \length(p)])) ;
@*/

Если я скопирую/вставлю этот точный код в текстовый редактор и попытаюсь запустить этот код с плагином wp с помощью:

frama-c -wp -wp-rte -wp-prover alt-ergo shapes.c

Я получаю сообщение об ошибке:

[kernel:annot-error] shapes.c:1: Warning: unexpected token '{'

Если я откажусь от попыток написать объявления типов структур на уровне логики/спецификации, но все же хотел бы написать выражения на уровне логики/спецификации, которые создают экземпляры структур, определенных в C, следующим образом:

struct somestruct {
     int x;
     int y;
 };

/*@
     logic struct somestruct foo = { .x = 3, .y = 4 };
*/

Я все еще получаю сообщение об ошибке:

[kernel:annot-error] aggregate_err.c:7: Warning:
  unsupported aggregated field construct. Ignoring global annotation

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

Если я покопаюсь в исходниках frama-C 20.0, чтобы попытаться найти часть кода парсера-генератора для объявлений /*@ type, окажется, что синтаксис в Ex 2.2.7 на самом деле не реализован. Похоже, что синтаксис для объявлений уровня типа - это строка 799 frama-c-20.0-Calcium/src/kernel_internals/parsing/logic_parser.mly (называется type_spec). И правило анализа для объявлений уровня типа структур:

| STRUCT exit_rt_type identifier_or_typename { LTstruct $3 }

который, похоже, будет поддерживать

//@ type foo = struct c_struct;

но не что-то вроде того, что есть в Ex 2.2.7, как в:

//@ type point = struct { real x; real y; };

Есть ли что-то еще, что я должен сделать, чтобы улучшить поддержку структур в ACSL/Frama-C? Спасибо!


frama-c acsl
person Andrew Ferraiuolo    schedule 23.12.2019    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Не все конструкции ACSL поддерживаются текущей реализацией Frama-C. С каждым выпуском Frama-C поставляется руководство по реализации ACSL, в котором описываются конструкции, которые еще не реализованы. Для Frama-C 20.0 Calcium это можно найти здесь . В этом документе неподдерживаемые конструкции выделены красным в соответствующем правиле BNF. Обратите внимание, однако, что другие части руководства остались нетронутыми. Примечательно, что тот факт, что пример включен в руководство по реализации, не означает, что ожидается, что он будет успешно проанализирован текущей версией Frama-C. В вашем случае это правила рисунка 2.17 на стр. 57, которые показывают, что действительно записи не реализованы.

Как вы уже сами обнаружили, действительно возможно определить из него C struct (возможно ghost) и тип ACSL. Конечно, поскольку struct живет в мире C, его поля должны иметь типы C (типы ACSL в декларациях-призраках также не поддерживаются).

Точно так же вы можете имитировать отсутствие прямого определения записи путем обновления (конструкция \with) всех полей произвольной записи, как в следующем примере:

//@ ghost struct c_s { float x; float y; };

//@ type point = struct c_s;

//@ axiomatic Arbitrary_point { logic point empty; }

//@ logic point my_point = {{ empty \with .x = (float)1. } \with .y = (float)2.};
person Virgile    schedule 27.12.2019
comment
Спасибо за ваш ответ. Пример, который вызывает синтаксическую ошибку, на самом деле все еще находится в руководстве по реализации, на которое вы ссылаетесь (это пример 2.12 в разделе 2.2.7 на странице 27). Если я скопирую и вставлю этот пример дословно, я все равно получу ту же ошибку. Из текста не следует, что этот пример не должен работать. frama-c -version дает 20.0 (кальций), и я запускаю команду frama-c -wp -wp-prover alt-ergo ex2.12.c. Можете ли вы (или кто-то) повторить мою ошибку? Или моя среда делает что-то неожиданное? - person Andrew Ferraiuolo; 07.01.2020
comment
Я также получаю другие синтаксические ошибки, которые меня удивляют. Например: 99 /*@ 100 логика struct mpool abs_mpool_free(struct mpool *p, struct mpool_entry *ptr) = 101 { *p \with 102 .entry_list = { p-›entry_list \with {.next = *p } } 103 }; 104 */ выдает ошибку: [kernel:annot-error] mpool.spec:102: Предупреждение: неожиданный токен '{', хотя согласно справочному руководству это выглядит допустимым. Отбрасывание фигурных скобок вокруг выражения справа от entry_list кажется мне недопустимым и также выдает ошибку о непредвиденном. - person Andrew Ferraiuolo; 07.01.2020
comment
@AndrewFerraiuolo относительно вашего первого комментария, это то, что я пытался передать в своем ответе, говоря, что только описания BNF содержат детали реализации. Примеры оставлены в руководстве по реализации нетронутыми, но нет никаких обязательств, что они будут проанализированы Frama-C, если соответствующие записи BNF указывают на неподдерживаемые функции. Я отредактировал свой ответ, чтобы сделать больший акцент на этом факте. Что касается вашего второго комментария, я думаю, что он заслуживает отдельного вопроса, поскольку формат комментариев SO затрудняет обсуждение какого-либо нетривиального фрагмента кода. - person Virgile; 07.01.2020
comment
Спасибо! Извиняюсь за неправильное прочтение. Я внимательно прочитал его вскоре после того, как вы ответили первоначально, а затем забыл эту деталь, когда я вернулся, чтобы снова просмотреть руководство по реализации намного позже. - person Andrew Ferraiuolo; 07.01.2020