User Tools

Site Tools


faq

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
faq [2016/08/07 20:58]
syc
faq [2016/08/07 21:45] (current)
syc
Line 2: Line 2:
  
 This contains a list of facts and faq concerning CPROVER. ​ 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''​.
 +
 +<code C>
 +int main()
 +{
 +  #ifdef __CPROVER__
 +  assert(0);
 +  #endif
 +  ​
 +  return 1;
 +}
 +</​code>​
 +
 +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''?​ ===== ===== What is the difference between ''​assert''​ and ''​__CPROVER_assert''?​ =====
faq.txt ยท Last modified: 2016/08/07 21:45 by syc