Skip to content

README.md

Latest commit

 

History

History
72 lines (64 loc) · 2.46 KB

README.md

File metadata and controls

72 lines (64 loc) · 2.46 KB
Raw

Numerical Precision Examples

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 basic directory contains basic, mainly floating-point programs. Before running, please set the KLEE_HOME variable in basic/Makefile to an appropriate value. There are four alternative ways to run KLEE for numerical precision analysis, as follows:

    1. To run KLEE for numerical precision using default options, execute the following in the basic directory:

      make <program_name>.klee

      where <program_name> is the name of a C program file basic/<program_name>.c.

    2. To run KLEE for numerical precision using default options but with displaying of debugging information, execute the following in the basic directory:

      make <program_name>.dklee

      where <program_name> is the name of a C program file basic/<program_name>.c.

    3. To run KLEE for numerical precision with loop breaking, execute the following in the basic directory:

      make <program_name>.loop

      where <program_name> is the name of a C program file basic/<program_name>.c.

    4. To run KLEE for numerical precision with loop breaking and with displaying of debugging information, execute the following in the basic directory:

      make <program_name>.dloop

      where <program_name> is the name of a C program file basic/<program_name>.c.

  • The package directory contains applications.

    • To build the bitcode files and run them using KLEE, first update the value of LLVM_COMPILER variable in package/Makefile to suit your system.
    • Change to the package directory. 
      cd package
    • To run the the program bitcode using KLEE, say: 
      make <program_name>.klee
      where <program_name> is either rawcaudio, rawdaudio, timing, memdjpeg, or memcjpeg.
    • To remove the KLEE output directories: 
      make clean
    • To remove the KLEE output directories and the built application package: 
      make realclean

  • The loops directory 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.