Описание тега frama-c
Frama-C - это набор инструментов с открытым исходным кодом, предназначенный для анализа исходного кода C.
1
ответ
Компиляция Frama-c под Mac OS X 10,9
Я пытаюсь установить последнюю версию frama-c(Fluorine 3) в Mac OS X 10.9. Используя brew, я смог заполнить предпосылки frama-c(Gtk, GtkSourceView, GnomeCanvas и Lablgtk2) Результат из файла конфигурации следующий: $ ./configure configure: *********…
11 ноя '13 в 23:54
1
ответ
Frama-c, недетерминированные значения с плавающей точкой
В качестве примера я использую следующую функцию: float nondet_float(){ float x; return x; } int main(){ float x = nondet_float(); if(isnan(x)){ some_error(); } } Интересно, как мне использовать frama-c для симуляции недетерминированных операций с п…
17 сен '17 в 15:56
1
ответ
Использование Frama-C на Windows 7
Я установил версию Windows для Boron с сайта frame-c http://frama-c.com/download.html когда я пытаюсь запустить плагин val, я получаю сообщение об ошибке, что препроцессорная переменная CPP не установлена, как показано ниже: C:\Frama-C\bin>frama-…
12 мар '14 в 21:18
2
ответа
Получу ли я 3-х адресный код в Frama-c
Я только начал разрабатывать плагин frama-c, который выполняет некоторый анализ псевдонимов. Я использую анализ Dataflow.Backwards, и теперь мне нужно пройти через различные операторы присваивания и собрать кое-что о lvalues. Предоставляет ли frama-…
21 мар '13 в 20:30
1
ответ
Проблема проверки с использованием плагина Jessie и Frama-C
Я новичок в Frama-C и хочу правильно изучить синтаксис ACSL. У меня есть этот фиктивный пример, и плагин Jessie не может проверить строки № 9 и 12. Я что-то упустил? Проверяемая (равная) функция проверит, имеют ли два массива (a и b) одинаковые знач…
18 апр '13 в 13:59
1
ответ
Заставить Frama-c показывать зависимости даже от "мертвых веток"
Я использую версию frama-c Aluminium-20160502 и хочу выяснить зависимости в большой программе. При использовании опции -deps в командной строке я обнаружил, что некоторые зависимости отсутствуют. В частности, когда несколько условий объединяются в о…
18 ноя '16 в 11:17
1
ответ
Введение спецификаций математических функций с ACSL/Frama-C
Можно ли реализовать спецификации в ACSL для функций, обычно вызываемых при компиляции с -lm, как sqrt? Я использую его для плагина Frama-C WP. Вот небольшой пример, чтобы проиллюстрировать, что я хотел бы сделать. /*@ requires sqrt_spec: \forall fl…
24 июн '14 в 15:29
2
ответа
Плагин WP: ошибка синтаксиса Alt-Ergo
Для функции C ниже я получаю синтаксические ошибки от Alt-Ergo для последней версии Frama-c. frama-c -wp -wp-rte -lib-entry RoundNearestFive.c -wp-out temp -wp-model="nat, real" Я не уверен, что не так в этой сгенерированной строке: ... let r_0 = da…
08 янв '14 в 18:45
1
ответ
Scanf не работает должным образом в Frama-C
В программе ниже функция dec использования scanf прочитать произвольный ввод от пользователя. dec вызывается из main и в зависимости от входа он возвращает 1 или 0 и, соответственно, будет выполнена операция. Тем не менее, анализ стоимости показывае…
28 фев '17 в 12:23
1
ответ
Предварительная обработка исходного кода перед нарезкой с использованием Frama-c
Я пытаюсь сравнить исходный код с нарезанным кодом, но frama-c нормализует код во время синтаксического анализа, что делает операторы нарезанного кода не идентичными операторам исходного кода. Можно ли предварительно обработать код с использованием …
10 сен '14 в 20:41
1
ответ
Формула LTL с Aorai
Я пытаюсь найти пример об операторе LTL _ F_, что фатально означает для Aorai, но я не могу точно выяснить, для чего предназначен этот оператор, и нет примеров в "тестах" хранилища Aorai. Например, я написал эту формулу CALL(main) && _X_ (CA…
11 июн '15 в 08:43
1
ответ
Рассчитать достижимость функции, используя анализ значений frama-c
Вот мой пример: int in; int sum(int n){ int log_input = n; int log_global = in; return 0; } int main(){ int n = Frama_C_interval(-10, 10); in = n; if (n > 0){ sum(n + 4); } return 0; } Я хотел бы найти диапазон входной переменной n при инициализа…
03 фев '16 в 11:25
1
ответ
Сильные указатели на varinfo, которого нет в AST?
Мой плагин Frama-C создает несколько varinfos с makeGlobalVar ~logic:true name type, Эти varinfos не существуют в AST (они являются заполнителями для результатов вызовов для распределения функций в целевой программе, созданных "динамически" во время…
21 авг '13 в 20:49
0
ответов
Можно ли получить (оригинальные) SID нарезанного AST с использованием Frama-C?
В настоящее время я пытаюсь использовать возможности нарезки Frama-C для создания обратного среза определенного оператора в данном файле, и из этого конкретного среза я хотел бы получить исходные идентификаторы SID принадлежащих ему операторов. Жела…
03 авг '16 в 11:11
1
ответ
Frama-c: сохранить результаты анализа плагина в файле c
Я новичок в frama-c. Поэтому я заранее прошу прощения за мой вопрос. Я хотел бы создать плагин, который будет изменять исходный код, клонировать некоторые функции, вставлять вызовы некоторых функций, и я хотел бы, чтобы мой плагин генерировал второй…
05 янв '18 в 22:23
3
ответа
Frama-C Gui на Маверикс не работает
Кто-нибудь устанавливал Frama-C на Маверикс? Потому что я не могу установить его или не знаю, как его установить (Gui Version)! Я уже установил ocaml на свой компьютер, но для версии Gui мне нужно установить эти библиотеки: Gtk, GtkSourceView, Gnome…
28 апр '14 в 13:06
1
ответ
Как отследить различия между исходным кодом C и предварительно обработанным кодом Frama-C?
В frama-C, когда я загружаю исходный файл, он выполняет предварительную обработку и выполняет автоматическое исправление ошибок, например, "автоматическое приведение типов", как показано ниже (int является типизированным до float). Теперь, как я мог…
04 июн '15 в 08:44
1
ответ
Frama-C/WP не может доказать цикл, инвариантный с \at
У меня проблемы с проверкой двух инвариантов цикла: loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre); loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((cha…
23 мар '13 в 19:10
1
ответ
Frama-C делает ошибку
Моя настройка среды - Ubuntu 14.04 LTS x86_64: После того, как я "./configure", а затем "make", ошибки следующим образом: Ocamlc src/plugins/value/gui_eval.cmi Ocamlc src/plugins/value/gui_eval.cmo Ocamlc src/plugins/value/gui_callstacks_filters.cmi…
02 мар '16 в 08:51
1
ответ
Игнорировать ассемблерный код в анализе значений и резервный код
Я попытаюсь использовать анализ стоимости проекта в C, но этот проект содержит некоторые .c файл, где мы можем найти код ассемблера. Когда я пытаюсь запустить frama-C для этих файлов, я получаю сообщение об ошибке в коде сборки. Код ассемблера разра…
26 май '14 в 07:50