Описание тега cbmc
CBMC - это средство проверки ограниченной модели для C и C++
1
ответ
Почему CBMC раскручивается больше раз?
Давайте рассмотрим код, приведенный ниже, могу ли я знать, почему CBMC разматывает больше, чем верхний предел, в то время как мы предположили, что начальное значение io больше 2. #include<assert.h> void main() { int i0; int o1; __CPROVER_assum…
23 апр '18 в 05:45
1
ответ
Обход переполнения без знака, обнаруженного CBMC
CBMC обнаруживает возможное переполнение без знака в следующих строках: l = (t + *b)&(0xffffffffL); c += (l < t); Я согласен, что существует вероятность переполнения в первой строке, но я забочусь о переносе в следующей строке, который CBMC н…
26 июн '15 в 04:54
0
ответов
Проверка переполнения буфера (привязка к массиву) в инструментах проверки ограниченной модели?
Как инструменты "проверки модели" справляются с переполнением буфера? Какие-либо конкретные методы, например, инструменты BMC применяются для проверки границ массивов с динамическим размером?
04 фев '19 в 20:50
1
ответ
Не удается проверить с помощью CBMC в программах на Ubuntu C++ - специализация шаблона компилятора type_traits.h с неверным количеством аргументов
Я пытаюсь использовать CBMC Bounded Model Checker в Ubuntu для программ на C и C++. Я скачал компиляторы gcc (4.9 v) и g++ (4.9 v) и установил CBMC через терминал. Я могу проверить программы на C, и никаких проблем не возникает, используя следующую …
24 мар '16 в 09:12
1
ответ
Лучший способ выразить "ровно один раз" в CBMC
Я очень стараюсь придумать лучшее решение для определения свойства "ровно один раз" в CBMC (средство проверки ограниченной модели C). Я имею в виду, что ровно одна позиция элемента в строке должна иметь значение 1 (или любое положительное число, кот…
09 мар '15 в 14:01
2
ответа
Казалось бы, неверный доступ к памяти не сообщен CMBC
У меня есть следующий фрагмент кода. #include<stdio.h> #include<stdlib.h> int main() { char *c = malloc(1); printf("%p\n", c); c = c + 20; printf("%p\n", c); printf("%d\n", *c); free(c - 20); return 0; } В этом коде я выделяю 1 байт памя…
31 мар '16 в 09:35
0
ответов
Невозможно интегрировать CBMC в системы сборки
Я пытаюсь использовать CBMC (C Bounded Model Checking: https://www.cprover.org/cbmc/) в проектах C с открытым исходным кодом из GitHub. Для целей этого вопроса давайте рассмотрим следующий проект: https://github.com/reubenhwk/radvd Проблема возникае…
21 апр '18 в 11:44
1
ответ
CBMC обнаружил ошибку подтверждения в моей программе Pthreads, это правильно?
Я использую CBMC для проверки моей программы Pthreads, она обнаружила некоторые ошибки подтверждения, которые, я думаю, не существовали. Ошибка возникает только тогда, когда я запускаю два потока одновременно. То есть, когда я помещаю один из операт…
29 авг '18 в 02:57
1
ответ
CBMC как самостоятельный?
Можно ли запустить CBMC как автономный без Visual Express? Нужно ли перекомпилировать его или есть еще один трюк? Мне нужно только использовать CBMC для регулярного перевода функции в CNF, поэтому я хочу вызвать ее с именем функции, записать файл cn…
15 ноя '14 в 15:24
1
ответ
Неявное замедление функции "setWeight"
Я пишу программу, но получаю это предупреждение!! Может ли кто-нибудь помочь мне в этом отношении. #include <stdio.h> #include <stdlib.h> typedef int bool; #define true 1 #define false 0 #define M 5 // Define total molecules #define MAX …
22 окт '15 в 06:40
2
ответа
CBMC звонить с Python?
Есть ли способ, которым я могу вызвать CBMC из Python или есть какая-нибудь обертка или API для него? Моя проблема заключается в следующем. Я хочу создать функцию C автоматически в Python (это работает довольно хорошо) и отправил их в CBMC из Python…
10 ноя '14 в 19:22
1
ответ
Почему итерация по общему количеству ребер не приводит к бесконечному или конечному числу раскручиваний петель?
#include<stdio.h> #define N 6 #define M 10 typedef int bool; #define true 1 #define false 0 unsigned int nondet_uint(); typedef unsigned __CPROVER_bitvector[M] bitvector; unsigned int zeroTon(unsigned int n) { unsigned int result = nondet_uint…
18 ноя '15 в 06:50
1
ответ
Проверка модели CBMC
Я пытаюсь ограничить стол b[4][4] такой, что только те места, которые имеют i>=j и удовлетворяя условию, что (stored[i] & stored[j]) == stored[i] будет 1, а остальные будут 0. Почему это не работает? void main(){ unsigned int i = 0 , j = 0; _…
05 мар '15 в 14:05
0
ответов
Как выполнить CBMC для нескольких проектов в одном решении в командной строке Visual Studio?
Я выполняю CBMC из командной строки MS Visual Studio. Я построил решение с использованием MSBuild и передал его через goto-cc для получения исполняемого файла. Этот исполняемый файл при передаче в cbmc дает результат только для основного проекта, ко…
23 ноя '18 в 09:50
1
ответ
Невозможно использовать команды JBMC (Bounded Model Checker) для Java
Я новичок в JBMC(ограниченная модель проверки). У нас есть требование выяснить возможности исключения RunTime, которое может возникнуть в Java-программе, без ее запуска. Мы искали некоторые абстрактные рамки интерпретации и обнаружили, что JBMC помо…
19 июн '19 в 16:15
1
ответ
Как cbmc работает с заголовком c?
Если у меня есть ac-файл, содержащий более одной функции, и я хочу запустить cbmc с z3 solver для предварительно обработанной версии программы (используя gcc), а в разделе заголовка есть несколько других файлов (c-файлов). Как cbmc увидит эти файлы?…
24 июн '19 в 18:53
1
ответ
Как получить все перестановки в CBMC?
Я пытаюсь получить все перестановки массива в CBMC. Для небольших случаев, например [1,2,3], я полагаю, что могу написать i1 = nondet() i2 = nondet() i3 = nondet() assume (i > 0 && i < 4); ... assume (i1 != i2 && i2 != i3 &…
15 апр '20 в 12:06
0
ответов
CBMC: throws: "атомные секции различаются в зависимости от ветки"
Я пытаюсь использовать CBMC в большом стеке встроенного программного обеспечения с одним основным прерыванием. Файлы .c обрабатываются нормально, но я застрял в моделировании поведения прерывания с помощью следующего кода: void main_interrupt(void);…
29 сен '21 в 18:24
1
ответ
Пример игрушки CBMC
Я новичок в CBMC и экспериментирую с ним. В этой связи здесь есть пример игрушки для проверки функции binsearch с СВМСОМ. Я решил запустить следующую команду, которую они предоставили, просто изменив количество раз, когда цикл разматывался: cbmc bin…
10 ноя '21 в 05:38
1
ответ
Аргументы __CPROVER_fence()
Я вижу код вроде __CPROVER_fence("RRfence", "RWfence");используются в таких проектах, как тестирование Linux RCU и оболочки pthread для анализа CBMC. Я просмотрел онлайн-документацию, но не нашел текста в строках, отправленных этой функции CBMC. Как…
03 дек '21 в 00:12