Синтаксическая ошибка ACSL set logic / frama-c

Question

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

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

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

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

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

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

Эдуардо

Answer 1

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

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

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

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

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

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

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