SMT2 and goto-cc

[Chester Wong]

Hi,

 

I am a new beginner to the CBMC. I got a few questions related to the use of cbmc and goto-cc.

 

I was trying to convert my program into SMT-LIB, so I tried to use the "--smt2" flag.

I tried to check the c file:

```

int put(char c) {return c - c;}

int s2() {return 0;}

 

int main() {

    int a = puts('a');

    assert(a != s2());

}

```

1. It does output "assertion a != s2(): FAILURE" if I use the "--smt2" flag, however, when I output the file with "--outfile smt", and parse it to z3 solver, it said there is a satisfy model. I notice that there is no any assertion between the variable a and s2 return value in the output file. May I know am I using the outfile option correctly?

 

2. Is there a way to translate the function into SMT-LIB without giving any assertion?

3. Can I disable the simplification of the VCC, and generate the SMT-LIB straightly?

 

4. May I know what is the standard way to test a function in a library?

I tried the following approach:

```

In the library   (contains in library.a): int func_in_lib(int a, int b) { ... }

In the test file                (file.c):

    int totest(int a, int b) {

        int result func_in_lib(a, b);

        //some assertions

    }

```

Firstly run "goto-cc file.c -o test -l library -I include -L lib"

Then run "cbmc test --function totest"

 

Is this a normal way to test the function?

 

Thank you very much.

Chester

[Martin Nyx Brain]

On Tue, 2021-07-20 at 09:23 -0700, Chester Wong wrote:
>
> Hi,
>
>
>
> I am a new beginner to the CBMC. I got a few questions related to the
> use
> of cbmc and goto-cc.
>
>
>
> I was trying to convert my program into SMT-LIB, so I tried to use
> the "--smt2" flag.

( At the risk of being patronising : you do know that this will only
work for some kind of programs because you have to unroll the loops. )

> I tried to check the c file:
>
> ```
>
> int put(char c) {return c - c;}
>
> int s2() {return 0;}
>
>
>
> int main() {
>
> int a = puts('a');
>
> assert(a != s2());
>
> }
>
> ```
>
> 1. It does output "assertion a != s2(): FAILURE" if I use the "
> --smt2"
> flag, however, when I output the file with "--outfile smt", and parse
> it to
> z3 solver, it said there is a satisfy model.

Yes; we are using the solver to search for a counter-example so SAT ~~>
verification failure.

> I notice that there is no any
> assertion between the variable a and s2 return value in the output
> file.

a may be resolved by constant propagation during symbolic execution.

> May I know am I using the outfile option correctly?

--smt2 --outfile whatever.smt2
is the correct usage, so, yes, sounds like it.

> 2. Is there a way to translate the function into SMT-LIB without
> giving any
> assertion?

I believe this is what --program-only is supposed to do but I don't
know how well tested it is, so bit-rot is possible.

> 3. Can I disable the simplification of the VCC, and generate the SMT-
> LIB
> straightly?

--no-simplify should do the trick but be warned that simplification is
needed for things like detecting finite loop unrollings so you may need
--unwind or --depth to make sure it terminates.

> 4. May I know what is the standard way to test a function in a
> library?
>
> I tried the following approach:
>
> ```
>
> In the library (contains in library.a): int func_in_lib(int a, int
> b) {
> ... }
>
> In the test file (file.c):
>
> int totest(int a, int b) {
>
> int result func_in_lib(a, b);
>
> //some assertions
>
> }
>
> ```
>
> Firstly run "goto-cc file.c -o test -l library -I include -L lib"
>
> Then run "cbmc test --function totest"
>
>
>
> Is this a normal way to test the function?

That should work. You might want to create a calling context for the
function(s) so you can control what the inputs are a bit better.

HTH

Cheers,
- Martin