Stack Overflow
Stack Overflow

Questions tagged [cbmc]

CBMC is a bounded model checker for C and C++

CBMC is a bounded model checker for C and C++. It can verify array bounds, pointer safety, exception catchment and user-specified assertions. It is primarily aimed at embedded software but supports dynamic memory allocation. It is available for Linux, Solaris, Mac OS X and Windows.

19 questions
5
votes
1 answer

Bypassing an unsigned addition overflow detected by CBMC

CBMC detects a possible unsigned addition overflow in the following lines: l = (t + *b)&(0xffffffffL); c += (l < t); I agree that there is a possibility of an overflow in the first line, but I am taking care of the carry in the next line which CBMC…
AcidBurn
  • 199
  • 1
  • 11
3
votes
1 answer

`__CPROVER_fence()` arguments

I see code like __CPROVER_fence("RRfence", "RWfence"); being using in projects like the Linux RCU testing and pthread wrappers for CBMC analysis. I looked at the online documentation, but found no text on the strings sent to this CBMC…
artless noise
  • 21,212
  • 6
  • 68
  • 105
3
votes
1 answer

CBMC detected an assert error in my Pthreads program, is it correct?

I use CBMC to verify my Pthreads program, it detected some assert errors which I don't think would exist. The error only occur when I run the two threads at the same time. That is to say, when I put one of the statement which calls the thread…
Bailin Lu
  • 73
  • 7
3
votes
0 answers

Unable to integrate CBMC into build systems

I'm trying to use CBMC (C Bounded Model Checking: https://www.cprover.org/cbmc/) on open-source C projects from GitHub. For the purpose of this question, let's consider the following project: https://github.com/reubenhwk/radvd The problem arises…
s.dallapalma
  • 1,225
  • 1
  • 12
  • 35
3
votes
1 answer

Can't verify with CBMC in Ubuntu c++ programs - compiler type_traits.h template specialization with wrong number of arguments

I am trying to use the CBMC Bounded Model Checker in Ubuntu for both C and C++ programs. I have downloaded gcc (4.9 v) and g++ (4.9 v) compilers and I installed the CBMC through terminal. I am able to verify C programs and no problems arise using…
Marialena
  • 817
  • 8
  • 31
3
votes
1 answer

Better way to express “exactly once” in CBMC

I'm trying really hard to come up with a better solution to state an “exactly once” property in CBMC (C bounded model checker). I mean exactly one element position in a row should have the value 1 (or any positive number that can be checked as the…
user2754673
  • 439
  • 3
  • 13
3
votes
1 answer

CBMC Model Checking

I'm trying to constraint the table b[4][4] such that only those places which have i>=j and satisfying the condition that (stored[i] & stored[j]) == stored[i] be 1, and the rest be 0. Why this is not working? void main(){ unsigned int i = 0 , j =…
user2754673
  • 439
  • 3
  • 13
1
vote
1 answer

Why iterating over total no of edges causing infinite or finitely many loop unwindings?

#include #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 =…
user2754673
  • 439
  • 3
  • 13
1
vote
1 answer

CBMC as standalone?

is it possible to run CBMC as stand alone witout Visual Express ? Do I need to recompile it or is there another trick maybe ? I only need to use CBMC to translate a function to CNF regularly, so I want to call it with the function name, write the…
Adrian Monk
  • 73
  • 2
  • 11
1
vote
2 answers

CBMC call from Python?

Is there a way that I can call CBMC from Python or is there any wrapper or API for it available? My Problem is the following. I want to create a C function automatically in Python (this works quite well) and sent them to CBMC from Python for…
Adrian Monk
  • 73
  • 2
  • 11
0
votes
0 answers

realpath failed: Invalid argument when using goto-gcc

I am new to goto-gcc. I try to use it to Compile the source files into a GOTO binary. I have file1.c: #include int multiply(int a, int b) { return a * b; } file2.c: #include extern int multiply(int a, int b); void…
Jackson
  • 23
  • 2
0
votes
1 answer

CBMC Toy Example

I'm new to CBMC and experimenting with it. In this link here, there is a toy example for checking the function binsearch with CBMC. I decided to run the following command that they provided, just changing up the number of times the loop was…
UnevenMango
  • 140
  • 8
0
votes
1 answer

How to get all permutations in CBMC?

I am trying to get all permutations of an array in CBMC. For small cases, e.g., [1,2,3], I suppose I can write i1 = nondet() i2 = nondet() i3 = nondet() assume (i > 0 && i < 4); ... assume (i1 != i2 && i2 != i3 && i1 != i3); // do stuffs with…
user2579326
  • 95
  • 4
0
votes
1 answer

How cbmc works with c header?

If I have a c file that contains more than one function, and I want to run the cbmc with z3 solver on the preprocessed version of the program (using gcc) and there are some other files(c files) in the header section. How will the cbmc see those…
eng2019
  • 53
  • 6
0
votes
1 answer

Unable to use JBMC (Bounded Model Checker) Commands for Java

Am new to the JBMC(Bounded Model Checker). We have a requirement to find out the possibilities of RunTime Exception which may occur in java program without running it. We searched some abstract interpretation framework and found JBMC would help in…
Natesan sathish
  • 5
  • 2
1
2