frama-c

0зной

2ответ

Ошибка при установке плагина hello_world на ubuntu 16.04

Я установил frama-c с использованием opam (на Ubuntu 16.04). я пытаюсь установить «hello_world.ml» в качестве плагина (в руководстве по разработке плагинов) с помощью Makefile FRAMAC_SHARE :=$(shell f

2зной

1ответ

Нарезка для нескольких утверждений

Возможно ли использовать плагин для резки Frama-C для разрезания для более чем одного утверждения? E.g. с учетом следующего кода: #include "assert.h" int main() { double a=3; double b=4;

0зной

1ответ

Frama-C-Plugin: Resolve Указатель на указатель

Я разрабатываю фрейм-c-плагин, где я хочу получить значения указателей (а не адрес, на который они указывают, но значение по этому адресу). Это работает до сих пор для простых указателей. Теперь я хоч

1зной

1ответ

Значение Frama-C Builtins

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

5зной

1ответ

Frama-c Magnesium: невозможно выполнить WP плагин на Windows

Я установил версию Magna-c Magnesium, используя предоставленную команду here. Во время установки и выполнения команды frama-c -version я не получил никаких ошибок при печати в печатной версии Frama-c

1зной

2ответ

Плагин Frama-C: Разрешить значения массива

Я работаю над фрейм-c-плагином, который должен разрешать значения всех видов varibles. Мне удалось вызвать указатели разметки, структуры и typedefs и напечатать соответствующие значения. Теперь я борю

-1зной

1ответ

Тайм-аут при проверке добавления двух массивов

Я пытаюсь проверить добавление двух массивов 2d, но я постоянно принимаю ошибку тайм-аута, независимо от решателя, который я использую. код, который я пытаюсь проверить, является следующее: typedef st