GitHub - yangke/KATCH: This is a copied and to be developed version of KATCH(see ESEC/FSE ’13, paper of Paul Dan Marinescu and Cristian Cadar)

yangke / KATCH Public

Notifications You must be signed in to change notification settings
Fork 0
Star 7

This is a copied and to be developed version of KATCH(see ESEC/FSE ’13, paper of Paul Dan Marinescu and Cristian Cadar)

Unknown, Unknown licenses found

Licenses found

7 stars 0 forks Branches Tags Activity

Star

Notifications

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 1 Commit
autoconf		autoconf
docs		docs
examples		examples
include		include
lib		lib
runtime		runtime
scripts		scripts
test		test
tools		tools
unittests		unittests
utils		utils
www		www
LICENSE-KATCH.TXT		LICENSE-KATCH.TXT
LICENSE.TXT		LICENSE.TXT
Makefile		Makefile
Makefile.common		Makefile.common
Makefile.config.in		Makefile.config.in
Makefile.rules		Makefile.rules
README.txt		README.txt
TODO.txt		TODO.txt
configure		configure

Repository files navigation

//===----------------------------------------------------------------------===//
// KATCH
//===----------------------------------------------------------------------===//

KATCH is a tool for automatic and comprehensive testing of code patches.
It combines symbolic execution with several novel heuristics based on
static and dynamic program analysis, and leverages existing test suites
to quickly reach the new code.

KATCH is based on the klee symbolic virtual machine.

For details, see http://srg.doc.ic.ac.uk/projects/katch/

//===----------------------------------------------------------------------===//
// Klee Symbolic Virtual Machine
//===----------------------------------------------------------------------===//

klee is a symbolic virtual machine built on top of the LLVM compiler
infrastructure. Currently, there are two primary components:

  1. The core symbolic virtual machine engine; this is responsible for
     executing LLVM bitcode modules with support for symbolic
     values. This is comprised of the code in lib/.

  2. A POSIX/Linux emulation layer oriented towards supporting uClibc,
     with additional support for making parts of the operating system
     environment symbolic.

Additionally, there is a simple library for replaying computed inputs
on native code (for closed programs). There is also a more complicated
infrastructure for replaying the inputs generated for the POSIX/Linux
emulation layer, which handles running native programs in an
environment that matches a computed test input, including setting up
files, pipes, environment variables, and passing command line
arguments.

For further information, see the webpage or docs in www/.