diff options
Diffstat (limited to 'lib/Core/Differentiator.h')
-rw-r--r-- | lib/Core/Differentiator.h | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/lib/Core/Differentiator.h b/lib/Core/Differentiator.h new file mode 100644 index 00000000..54a12ac7 --- /dev/null +++ b/lib/Core/Differentiator.h @@ -0,0 +1,43 @@ +//===-- Differentiator.h ----------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +// +// Class to perform actual execution, hides implementation details from external +// interpreter. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_DIFFERENTIATOR_H +#define KLEE_DIFFERENTIATOR_H + +#include "llvm/Support/raw_ostream.h" + +#include <cstdint> +#include <map> +#include <string> + +namespace klee { + +/// Return if name matches arg\d\d +bool isSymArg(std::string); + +/// Return if name matches out!.*\d +bool isSymOut(std::string); + +struct Differentiator { + uint64_t revA, revB; + std::map<uint8_t, std::string> args; + std::map<std::string, std::pair<std::string, std::string>> outputs; + Differentiator(uint64_t a, uint64_t b) : revA{a}, revB{b} {} +}; + +/// Write convenient representation for debugging +llvm::raw_ostream &operator<<(llvm::raw_ostream&, const Differentiator&); +} // End klee namespace + +#endif /* KLEE_DIFFERENTIATOR_H */ |