WedX - журнал о программировании и компьютерных науках

Назначает пункт для локальных переменных в Frama-C

Я пытаюсь проверить следующий фрагмент кода, используя frama-c

/*@ ensures \result != \null; 
  @ assigns \nothing;
  @*/
extern int *new_value();

//@ assigns *p;
void f(int* p){
  *p = 8;
}
//@ assigns \nothing;
int main(void){
 int *p = new_value(); 
 f(p);
}

Доказывающая сторона не может доказать, что main ничего не присваивает, что имеет смысл, поскольку main присваивает *p через функцию f. Однако как мне указать это в предложении \assigns, поскольку p является локальной переменной и к ней нельзя получить доступ в аннотации.

27.10.2014

Ответы:


1

assigns nothing действительно ложно. Переменная p является локальной, но эффект выполняется для *p, который является произвольным указателем.

контрпример

Если new_value определяется следующим образом:

int g;

int *new_value(){
  return &g;
}

Он удовлетворяет спецификации, и значение g равно 8 в конце файла main.

Чтобы пойти дальше

Если проблема состоит в том, чтобы дать присваивание функции main без каких-либо знаний о поведении функции new_value, вы можете сделать результат new_value доступным из логического пространства:

Например :

//@ logic int * R ;
//@ ensures \result == R && \valid(R) ; assigns \nothing ;
extern int *new_value();

//@ assigns *p;
void f(int * p) { … }

//@ assigns *R ;
int main(void) { … }

Более общим решением было бы иметь набор указателей для R вместо уникального.

31.10.2014
  • Спасибо за ответ. При использовании плагина wp он ломается. Теперь я устанавливаю плагин Jessie, чтобы посмотреть, работает ли он. Какой из них вы использовали? 04.11.2014
  • Пробовал с Джесси. Мне пришлось поместить объявление R в аксиоматический блок. После этого я получил опечатку: несвязанный идентификатор R. @François, у вас нет подобной проблемы? Какую версию Джесси вы используете? 04.11.2014
  • извините за путаницу, была какая-то другая техническая проблема. Идея с введением логического R работает с wp. 07.11.2014
  • Новые материалы

    Как создать диаграмму градиентной кисти с помощью D3.js
    Резюме: Из этого туториала Вы узнаете, как добавить градиентную кисть к диаграмме с областями в D3.js. Мы добавим градиент к значениям SVG и применим градиент в качестве заливки к диаграмме с..

    Я хотел выучить язык программирования MVC4, но не мог выучить его раньше, потому что это выглядит сложно…
    Просто начните и учитесь самостоятельно Я хотел выучить язык программирования MVC4, но не мог выучить его раньше, потому что он кажется мне сложным, и я бросил его. Это в основном инструмент..

    Лицензии с открытым исходным кодом: руководство для разработчиков и создателей
    В динамичном мире разработки программного обеспечения открытый исходный код стал мощной парадигмой, способствующей сотрудничеству, инновациям и прогрессу, движимому сообществом. В основе..

    Объяснение документов 02: BERT
    BERT представил двухступенчатую структуру обучения: предварительное обучение и тонкая настройка. Во время предварительного обучения модель обучается на неразмеченных данных с помощью..

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

    Работа с цепями Маркова, часть 4 (Машинное обучение)
    Нелинейные цепи Маркова с агрегатором и их приложения (arXiv) Автор : Бар Лайт Аннотация: Изучаются свойства подкласса случайных процессов, называемых дискретными нелинейными цепями Маркова..

    Crazy Laravel Livewire упростил мне создание электронной коммерции (панель администратора и API) [Часть 3]
    Как вы сегодня, ребята? В этой части мы создадим CRUD для данных о продукте. Думаю, в этой части я не буду слишком много делиться теорией, но чаще буду делиться своим кодом. Потому что..


    Для любых предложений по сайту: [email protected]