Указание ссылочной прозрачности в ACSL

Я хочу найти аннотацию ACSL, которую можно применить к функции или указателю функции, чтобы указать, что она обладает свойством ссылочной прозрачности. Какой-то способ сказать, что «эта функция всегда будет возвращать одно и то же значение при задании одних и тех же аргументов». Пока я не нашел такого способа. Может ли кто-нибудь указать мне способ выразить это?

Может быть, как-то сослаться на произвольную логическую функцию? Если бы я мог назвать неизвестную logic boolean uknown_function(void* a, void* b) = /* this is unkown */;, то я мог бы задокументировать функцию как имеющую постусловие, что \result равно этой произвольной/неизвестной логической функции?

Более широкий контекст пытается выполнять сравнения с стертым типом. Я хочу в целом выразить концепцию «пользователь дал мне void* для работы и bool (*)(void const*, void const*) для их сравнения, и пользователь гарантирует мне, что предоставленная функция действительно является строгим частичным порядком того, на что указывают эти указатели. " Если бы у меня это было, то я мог бы начать описывать свойства этих стертых типов объектов, которые сортируются, например.


frama-c acsl
person user1243488    schedule 12.11.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

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

/*@ logic boolean unknown_function{L}(int* a, int* b) reads a[0 .. 1], b[2 .. 3]; */

но если вы работаете с void *, не зная размера базовых объектов, это может быть сложно указать: если только результат unknown_function не зависит исключительно от значения указателя, а не содержимого указанного объекта, и в этом случае вы не нужен этот reads трюк.

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

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

person Virgile    schedule 14.11.2018
comment
Спасибо. RPP выглядит захватывающим, и я с нетерпением жду этого. Я был удивлен, увидев, что подход логических функций работает, потому что у меня не было большого успеха локально. Но похоже, что моей установке frama-c уже пару лет. Я получил хлор от опама, и теперь он работает, как вы сказали. У меня все еще есть пути, чтобы пойти, но это похоже именно то, что я хочу. - person user1243488; 15.11.2018