User Tools

Site Tools


faq

FAQ

This contains a list of facts and faq concerning CPROVER.

What is the difference between the goto program compiled by''goto-cc'' and ''cbmc''?

There is a difference between goto-cc and cbmc regarding the __CPROVER__ macro. We show it through the following example program, namely main.c.

int main()
{
  #ifdef __CPROVER__
  assert(0);
  #endif
 
  return 1;
}

The verification by cbmc main.c will return a failure because of the statement assert(0); an equivalent run is that

goto-cc main.c -D__CPROVER__ -o main.goto && cbmc main.goto

However, if we do not explicitly specify -D__CPROVER__, that is, we use the following call

goto-cc main.c -o main.goto && cbmc main.goto

then, the assert(0) will not be detected.

This inconsistency is the intended behaviour, i.e., goto-cc behaves like GCC by default.

What is the difference between ''assert'' and ''__CPROVER_assert''?

To have a look at the difference of the two, let us consider the following C program, namely main.c.

#include <assert.h>
 
int main()
{
  int x=0, y=1;
 
  assert(x>y);
 
  __CPROVER_assert(x>y, "cprover assert");
 
  return 1;
}

At first, we compile main.c into goto program: goto-cc main.c -o main.goto.

Then, we output the goto functions: goto-instrument main.goto –show-goto-functions.

The goto representation of assert and __CPROVER_assert, shown in below, clearly demonstrates their difference.

            ...  
     // 4 file main.c line 7 function main
     ASSERT !((signed long int)!(x > y) != 0l) // assertion x>y
     // 5 file main.c line 7 function main
     IF (signed long int)!(x > y) != 0l THEN GOTO 1
     // 6 file main.c line 7 function main
     (void)0;
     // 7 no location
  1: SKIP
     // 8 file main.c line 9 function main
     ASSERT x > y // cprover assert
            ...  

When compiled into goto program, as we can see, an if-statement is inserted after the line of assert, though it does nothing. In fact, such a difference sometimes can totally change the analysis result. For example, when generating test cases using the –cover option of cbmc, the test case coverage relies on the conditions in if-statements; in other words, the conditions specified within assert can be detected, but this is not true for __CPROVER_assert.

Note that if we do not include the header file assert.h in main.c, it turns out that the goto representation of assert and __CPROVER_assert is the same (except for the comment part).

How does CPROVER keep track of threads that have exited?

CPROVER maintains a global variable __CPROVER_threads_exited in the file ansi-c/library/pthread_lib.c. This variable essentially tracks whether a certain thread has exited or not. CPROVER can only know that a thread has exited when the function used for thread creation ends, unless the user has explicitly provided pthread_exit. Notice that in the thread spawn function in pthread_lib.c, the statements are sequentialized and__CPROVER_threads_exited is updated only after the thread created (via start_routine) has completed its execution.

void __actual_thread_spawn(
  void * (*start_routine)(void *),
  void *arg,
  unsigned long id)
{
  __CPROVER_HIDE:;
  __CPROVER_ASYNC_1: __CPROVER_thread_id=id,
                       start_routine(arg),
                       __CPROVER_threads_exited[id]=1;
}

Since r2704, __CPROVER_threads_exited is an unbounded array. Thus there is no limit on the number of threads that can be tracked. Before that change, CBMC could only track 64 threads, because the bits of an unsigned long long were used.

If I compile successfully my C or C++ programs by using Microsoft Visual Studio, can I verify them using cbmc?

[Response to someone on the mailing list]

Maybe. CBMC has (I believe) complete support for C99, support for the commonly used parts of C11 and a variety of compiler specific extensions, including some from GCC. Microsoft Visual Studio does not fully support C99 and has some extensions. Thus there are some valid C99 programs that you can verify with CBMC but not compile with Visual Studio and some programs in Microsoft's extension of C that you can compile with Visual Studio but will not parse in CBMC. If you stick to C99 (gcc has the flag -std=c99 which can check this) then it is likely that you can compile things in Visual Studio and verify them using CBMC.

The picture for C++ is a little more complicated. C++ is a very large and complex language with a lot of obscure and little used features. Writing a complete C++ front-end is a very time consuming process (note that most compilers do not implement the full language). Thus the C++ front-end for CBMC includes the parts of C++ that are commonly used in embedded applications plus a number of other features that particular customers have needed for their project. We support much of the core of C++98 and C++03 although our support for template meta-programming could be improved. We don't support many of the new features added in C++11 as some of them are a lot of work and we have yet to find a pressing need for them. Thus for C++ there will be more programs that compile in Visual Studio (some of which will not be standards compliant C++) that will not parse in CBMC.

If you are starting a new project from scratch and want to use CBMC I would suggest using C99. If you have a program that does not parse and you would like it to, please send us a minimal test case and we'll add it to the todo list. If you need more prompt support for a particular feature, contact us directly and we can probably work something out.

If I've used goto-cc to compile part of a program to object files, how do I analyse it?

[Michael says…]

The issue simply is that CBMC won't do the finalisation step by itself when reading a goto binary. That is, cbmc –function f00 file.c would work on your example, but cbmc –function f00 file.o does not. But here's how to make it work:

goto-cc -c file.c # file.o not usable by CBMC at this stage

goto-cc file.o –function f00 -o file # –function is a non-gcc option

cbmc file # this works

faq.txt · Last modified: 2016/08/07 21:45 by syc