Логическая ошибка набора ACSL / синтаксическая ошибка frama-c

Я использую азотную версию Frama-c на Mac и, похоже, не могу использовать логику "set", как описано в руководстве ACSL, например, я не могу объявить призрачную переменную, как в "// @ набор призраков ‹integer› someSet; ".

Программа frama-c всегда жалуется на синтаксическую ошибку в строке, где объявлен набор, несмотря ни на что.

Я также пробовал «Set» вместо «set», другие типы вместо «integer» (например, «char *») и указание «// @ open set;» чтобы импортировать модуль.

Может мне нужно указать какой-нибудь параметр командной строки? Выполнение "frama-c -kernel-help" неясно, что это будет.

Или, может быть, версия для Mac (я скачал двоичную версию Intel) устарела, и я должен скомпилировать последний исходный код?

Спасибо, с наилучшими пожеланиями,

Эдуардо


frama-c
person edrdo    schedule 31.03.2012    source источник

Ответы (1)


arrow_upward
2
arrow_downward

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

  • Функция должна быть частью языка ACSL.
  • Он должен быть доступным текущим интерфейсом Frama-C. Не все функции языка ACSL сразу реализуются во внешнем интерфейсе.
  • Плагин, который вы собираетесь использовать, должен использовать это преимущество.

Другое объяснение того же различия - здесь.

Я не могу объявить переменную-призрак, как в "// @ ghost set someSet;".

В вашем случае кажется, что частично реализованная функция - это не столько наборы (которые, кажется, реализованы во внешнем интерфейсе после беглого взгляда), сколько фантомный код, который в настоящее время может использовать только конструкции и типы C.

Или, может быть, версия для Mac (я скачал двоичную версию Intel) устарела, и я должен скомпилировать последний исходный код?

На данный момент у вас установлена ​​последняя версия.

person Pascal Cuoq    schedule 31.03.2012