Open
Description
Hello,
Is it possible to obtain the logic equations of a C code with CBMC? If so, how?
Here's an simple example:
#ifndef CBMC
#include <stdlib.h>
#include <assert.h>
#include <stdio.h>
#define nondet_int() 0
#else
//...
#endif
#define BOOL short
#define false 0
#define true 1
int main()
{
BOOL ok;
int a, b, c;
#ifdef CBMC
a = nondet_int();
b = nondet_int();
#else
//possible solution...
a = 3;
b = 7;
#endif
c = a + b;
ok = (c == 10);
assert(ok == false); //find a condition to prove that c==a+b (can be equal to...)
}
From what I've read, goto-instrument would be able to do this, but I haven't found any more information.
Thank you :)