We will explain the basics of using FunFrog in the following simple example (all the files can be downloaded here). The example constitutes a function that gets two integers and if they are within a predefined limit, it randomly (using a getchar() function) chooses one of them and returns it. The code looks as follows:
choice.c
choice.c
Now suppose that we would like to use FunFrog to verify that the implementation really does what we expect it to do. For this reason, we will create a sequence of verification scenarios and use FunFrog to analyze them. In addition to being the usual scenario of using model checking tools, this also allows FunFrog to create function summaries after every successful verification run and reuse them in the later runs.
Let us start with the following verification scenario:
test1.c:
The scenario test1 draws two random chars and checks that the result of the choice() function is equal to one of them, as expected. Note the special verification only implementation of the getchar() function. Special nondet_int() function is used to draw random values of a specific type. The naming convention nondet_TYPE assures that the analysis engine does not complain about missing function body and generates the corresponding random values. The construct __CPROVER_assume is used to limit the values of the nondeterministically chosen variables to the range we are interested in.
To use FunFrog in this example, we first need to "compile" the source codes to a goto-binary, which concisely represents the program in a form amenable to automated analysis known as goto-program. For this purpose, a special purpose compiler called goto-cc has to be used. The goto-cc compiler is part of the CProver framework and available at www.cprover.org/goto-cc/. However, due to possible version incompatibilities, we advise the FunFrog users to use the goto-cc binary that is part of the FunFrog binary package. In the following, we expect that the binaries that are part of the FunFrog package are on the path. This can be achieved by typing:
> export PATH=${PATH}:`pwd`/funfrog-0.5/
after unpacking the FunFrog package). Going back to the compilation of the goto-binary, all that needs to be done is to invoke goto-cc and pass it the source files to be analyzed.
> goto-cc test1.c choice.c
For projects using Makefiles, replacing gcc with goto-cc should do the job as the goto-cc compiler accepts the options of gcc and it also works both in the compiler and linker mode. Unless specified otherwise, the resulting goto-binary is stored in the a.out file in the current directory.
Now, we can run FunFrog to analyze the resulting goto-binary.
> funfrog a.out
Note that the verification was successful, i.e., the assertion on line 23 of test1 was not violated. This result takes into account any possible valuation of the random values returned by nondet_int(). Another important information is that function summaries for functions choice() and getchar() were generated and stored. By default, the generated function summaries are stored in the __summaries file and loaded from the same file. This behavior can be changed by using the --save-summaries FILE and --load-summaries FILE command line arguments.
If interested in the number and size of the stored summaries, you can use the sumo utility that is part of the FunFrog package.
> sumo --list __summaries
So there is one summary for both functions choice() and getchar().
Now, let us continue with another verification scenario.
test2.c:
In this scenario, we make sure, that when the choice is given only a single value within the limits, it returns the same value.
Again, we compile the new verification scenario:
> goto-cc test2.c choice.c
And analyze using FunFrog. By default, FunFrog will look for the already discovered function summaries in the __summaries file.
> funfrog a.out
Again, FunFrog proves that the assertion cannot be violated. Moreover, the summaries were used to substitute the functions choice() and getchar() and the substitution was strong enough to prove the property without a need of refinement.
Last, consider the following verification case.
test3.c:
The scenario focuses on a situation where the limits are exceeded by providing an EOF == -1 value.
Let us recompile and run FunFrog using the collected summaries:
> goto-cc test3.c choice.c
> funfrog a.out
FunFrog again proved that the assertion is not violated. However, this time the function summary of the choice() function was not strong enough to prove it. Therefore, a single refinement iteration took place. Finally, an additional function summary was generated that covers the out of limits case.
> sumo --list __summaries
The last thing to try is to rerun FunFrog on the second verification scenario but without the use of the stored summaries.
> rm __sumamries
> goto-cc test3.c choice.c
> funfrog a.out
Note that although both the running times are very small. The running time with function summaries is more than 10 times faster when compared to the fresh run without any summaries.
