How cbmc works with c header?

Question

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 files? because I tried to run it and he gives some errors about some variables as not declared where it's, in fact, they are declared in one of the header files.

could anyone explain how this works?

UPDATE:

int test(int x) {
for (int i = 2; i < sqrt(x); i++) {
    if (x%i == 0)
        return 0;
}

First of all, I preprocess the program using gcc

Then parse the program by pycparser

then instrument (add print statement after 4 to see the value of x)

Then I ran the cbmc on the instrumented version of file and I got this error: function `sqrt' is not declared

Welcome to SO! Please provide a [minimal, reproducible example](https://stackoverflow.com/help/minimal-reproducible-example) of the problem you're trying to solve, as well as the error output you're receiving in your console. Seeing this will help people answer your question. — jhelphenstine, Jun 24 '19 at 22:59

score 0 · Answer 1 · answered Jun 25 '19 at 09:00

You should include in the project all the files referenced by the header files. It is not enough to include only the right header(s), if the associated .c file(s) is not available.

Your sample code MUST have these lines also:

    else
    {
        return 1;
    }
}

How cbmc works with c header?

1 Answers1