This repository contains examples from various sources as a benchmark suite for numerical precision. This suite is for use with KLEE for numerical precision in https://github.com/fp-analysis/klee.
-
The
basicdirectory contains basic, mainly floating-point programs. Before running, please set theKLEE_HOMEvariable inbasic/Makefileto an appropriate value. There are four alternative ways to run KLEE for numerical precision analysis, as follows:-
To run KLEE for numerical precision using default options, execute the following in the
basicdirectory:make <program_name>.kleewhere
<program_name>is the name of a C program filebasic/<program_name>.c. -
To run KLEE for numerical precision using default options but with displaying of debugging information, execute the following in the
basicdirectory:make <program_name>.dkleewhere
<program_name>is the name of a C program filebasic/<program_name>.c. -
To run KLEE for numerical precision with loop breaking, execute the following in the
basicdirectory:make <program_name>.loopwhere
<program_name>is the name of a C program filebasic/<program_name>.c. -
To run KLEE for numerical precision with loop breaking and with displaying of debugging information, execute the following in the
basicdirectory:make <program_name>.dloopwhere
<program_name>is the name of a C program filebasic/<program_name>.c.
-
-
The
packagedirectory contains applications.- To build the bitcode files and run them using KLEE, first update
the value of
LLVM_COMPILERvariable inpackage/Makefileto suit your system. - Change to the
packagedirectory.cd package - To run the the program bitcode using KLEE, say:
where
make <program_name>.klee<program_name>is eitherrawcaudio,rawdaudio,timing,memdjpeg, ormemcjpeg. - To remove the KLEE output directories:
make clean - To remove the KLEE output directories and the built application
package:
make realclean
- To build the bitcode files and run them using KLEE, first update
the value of
-
The
loopsdirectory contains looping examples from Malardalen WCET benchmark suite without floating points and for which KLEE with numerical precision is able to infer loop trip counts.