Crate ktest_parser[][src]

ktest-parser is a utility to parse .ktest binaries which is the output of KLEE, into a Rust friendly struct instead.

KTest File Format Description

The KTest binary is structured as follows,

  1. A header
  2. KLEE arguments
  3. Symbolic arguments
  4. KTest objects.

The following sections describes the detailed structure. Each new section starts at byte 0 here, but since they follow each other the arguments start at byte 8 where the header left off. But it is easier to describe the structure this way.

The header describes the magic number which is either “KTEST” or “BOUT/n”. Then followed by a version of the file format.

BYTENAMEDESCRIPTIONLENGTH
0..5HDRFile format (default: KTEST)4 bytes
5..8VERSIONFile format version4 bytes

Arguments

The arguments section describes the number of arguments and then a repeated section of arguments where each argument is first described by a size and then its content of size length.

Information

BYTENAMEDESCRIPTIONLENGTH
0..4NUMARGSNumber of arguments4 bytes

Argument

This is repeated for (NUMARGS) times.

BYTENAMEDESCRIPTIONLENGTH
0..4SIZESize of argument4 bytes
4..(SIZE)ARGAn argument(SIZE) bytes

Symbolic arguments

Describes symbolic arguments.

BYTENAMEDESCRIPTIONLENGTH
0..4ARGVSnone4 bytes
4..8ARGVLENnone4 bytes

Objects

Like the arguments section, the first item is the number of objects. Then followed by a repeated section of objects where each object is described by a size and then its content of size length.

Information

BYTENAMEDESCRIPTIONLENGTH
0..4NUMOBJECTSNumber of objects4 bytes

Object

This is repeated for (NUMOBJECTS) times.

BYTENAMEDESCRIPTIONLENGTH
0..4SIZESize of object4 bytes
4..(SIZE)OBJECTAn object(SIZE) bytes

Structs

KTest

A representation of the KTest file format.

KTestObject

Contains information about the generated test vector on a symbolic object.

Functions

parse_ktest

Parses a .ktest file and returns a KTest. Will return an error if any parts of the binary is illegal.