Описание тега value-analysis
1
ответ
Scanf не работает должным образом в Frama-C
В программе ниже функция dec использования scanf прочитать произвольный ввод от пользователя. dec вызывается из main и в зависимости от входа он возвращает 1 или 0 и, соответственно, будет выполнена операция. Тем не менее, анализ стоимости показывае…
28 фев '17 в 12:23
1
ответ
Анализ значений для верхних границ петли
Я анализирую управляющую программу со следующей структурой: unsigned int cnt=0; unsigned int inc=3; ... void main(){ int i; int lim; for(i=0;i<100000;i++) { f1(); .... lim = f2(); if(cnt < lim) cnt += inc; .... } } Моя цель - проанализировать …
17 мар '16 в 14:02
2
ответа
Разработка плагина Frama-C: получение результата анализа стоимости
Я работаю над плагином для Frama-C, используя Value-analysis. Я просто хочу напечатать состояние переменных (значений) после каждого оператора (я думаю, что решение довольно легко, но я не мог понять это). Я получил текущее состояние с Db.Value.get_…
21 мар '16 в 13:48
1
ответ
Каково значение и назначение столбца "после" в EVA-плагине Frama-C
В уроке по EVA я нашел этот скриншот: с объяснением:"Точное значение, которое вызвало это, показано в столбце c5: -1. Стандарт C рассматривает сдвиг влево отрицательного числа как неопределенное поведение. Поскольку -1 - единственно возможное значен…
23 июл '18 в 15:14
2
ответа
Почему код недоступен в Frama-C Value Analysis?
При запуске анализа значений Frama-C с некоторыми тестами, например susan в http://www.eecs.umich.edu/mibench/automotive.tar.gzМы заметили, что многие блоки считаются мертвым кодом или недоступны. Однако на практике этот код выполняется, когда мы ра…
24 ноя '13 в 04:42
1
ответ
Используйте Frama-c для анализа проекта с помощью инфраструктуры сборки CMake.
Мне нужно использовать плагин для анализа значений frama-c для анализа некоторых проектов. Эти проекты используют инфраструктуру сборки CMake в качестве системы сборки. Я использовал frama-c для анализа каждого файла отдельно. Таким образом, информа…
16 фев '16 в 22:25
1
ответ
Измените шаблон Entity Framework, чтобы включить атрибуты анализа значений ReSharper в свойствах объекта
Моя модель данных сущностей содержит информацию о том, какие поля могут быть обнуляемыми и не обнуляемыми. Однако сгенерированные шаблоны не включают эту информацию. В другом месте в моем коде я использую JetBrains.Annotations чтобы показать, где пу…
02 авг '13 в 15:14
2
ответа
Рассчитать диапазон входных данных, который приводит к удовлетворению предиката
Допустим, у нас есть следующий C-код: int my_main(int x){ if (x > 5){ x++; if (x > 8){ x++; if (x < 15){ //@(x >= 9 && x <= 14); } } } return 0; } Я хотел бы вычислить с помощью статического анализа границы переменной x при ин…
09 фев '16 в 10:04
1
ответ
Frama-C Plugin-Development: получение значений анализа стоимости различных вызовов
Я разрабатываю плагин Frama-C, который должен печатать значения переменных после каждого оператора. В Frama-C-Gui на вкладке Значения я вижу значения анализа по всей программе и после различных вызовов функций (с параметрами функции). Теперь я хочу …
22 мар '16 в 13:36