diff options
37 files changed, 496 insertions, 187 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 731aa446..9ad1b49a 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -324,163 +324,6 @@ inline std::stringstream &operator<<(std::stringstream &os, const Expr::Kind kin return os; } -// Terminal Exprs - -class ConstantExpr : public Expr { -public: - static const Kind kind = Constant; - static const unsigned numKids = 0; - -private: - llvm::APInt value; - - ConstantExpr(const llvm::APInt &v) : value(v) {} - -public: - ~ConstantExpr() {} - - Width getWidth() const { return value.getBitWidth(); } - Kind getKind() const { return Constant; } - - unsigned getNumKids() const { return 0; } - ref<Expr> getKid(unsigned i) const { return 0; } - - /// getAPValue - Return the arbitrary precision value directly. - /// - /// Clients should generally not use the APInt value directly and instead use - /// native ConstantExpr APIs. - const llvm::APInt &getAPValue() const { return value; } - - /// getZExtValue - Returns the constant value zero extended to the - /// return type of this method. - /// - ///\param bits - optional parameter that can be used to check that the - ///number of bits used by this constant is <= to the parameter - ///value. This is useful for checking that type casts won't truncate - ///useful bits. - /// - /// Example: unit8_t byte= (unit8_t) constant->getZExtValue(8); - uint64_t getZExtValue(unsigned bits = 64) const { - assert(getWidth() <= bits && "Value may be out of range!"); - return value.getZExtValue(); - } - - /// getLimitedValue - If this value is smaller than the specified limit, - /// return it, otherwise return the limit value. - uint64_t getLimitedValue(uint64_t Limit = ~0ULL) const { - return value.getLimitedValue(Limit); - } - - /// toString - Return the constant value as a string - /// \param Res specifies the string for the result to be placed in - /// \param radix specifies the base (e.g. 2,10,16). The default is base 10 - void toString(std::string &Res, unsigned radix=10) const; - - - - int compareContents(const Expr &b) const { - const ConstantExpr &cb = static_cast<const ConstantExpr&>(b); - if (getWidth() != cb.getWidth()) - return getWidth() < cb.getWidth() ? -1 : 1; - if (value == cb.value) - return 0; - return value.ult(cb.value) ? -1 : 1; - } - - virtual ref<Expr> rebuild(ref<Expr> kids[]) const { - assert(0 && "rebuild() on ConstantExpr"); - return const_cast<ConstantExpr*>(this); - } - - virtual unsigned computeHash(); - - static ref<Expr> fromMemory(void *address, Width w); - void toMemory(void *address); - - static ref<ConstantExpr> alloc(const llvm::APInt &v) { - ref<ConstantExpr> r(new ConstantExpr(v)); - r->computeHash(); - return r; - } - - static ref<ConstantExpr> alloc(const llvm::APFloat &f) { - return alloc(f.bitcastToAPInt()); - } - - static ref<ConstantExpr> alloc(uint64_t v, Width w) { - return alloc(llvm::APInt(w, v)); - } - - static ref<ConstantExpr> create(uint64_t v, Width w) { - assert(v == bits64::truncateToNBits(v, w) && - "invalid constant"); - return alloc(v, w); - } - - static bool classof(const Expr *E) { - return E->getKind() == Expr::Constant; - } - static bool classof(const ConstantExpr *) { return true; } - - /* Utility Functions */ - - /// isZero - Is this a constant zero. - bool isZero() const { return getAPValue().isMinValue(); } - - /// isOne - Is this a constant one. - bool isOne() const { return getLimitedValue() == 1; } - - /// isTrue - Is this the true expression. - bool isTrue() const { - return (getWidth() == Expr::Bool && value.getBoolValue()==true); - } - - /// isFalse - Is this the false expression. - bool isFalse() const { - return (getWidth() == Expr::Bool && value.getBoolValue()==false); - } - - /// isAllOnes - Is this constant all ones. - bool isAllOnes() const { return getAPValue().isAllOnesValue(); } - - /* Constant Operations */ - - ref<ConstantExpr> Concat(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Extract(unsigned offset, Width W); - ref<ConstantExpr> ZExt(Width W); - ref<ConstantExpr> SExt(Width W); - ref<ConstantExpr> Add(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Sub(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Mul(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> UDiv(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> SDiv(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> URem(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> SRem(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> And(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Or(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Xor(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Shl(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> LShr(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> AShr(const ref<ConstantExpr> &RHS); - - // Comparisons return a constant expression of width 1. - - ref<ConstantExpr> Eq(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Ne(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Ult(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Ule(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Ugt(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Uge(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Slt(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Sle(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Sgt(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Sge(const ref<ConstantExpr> &RHS); - - ref<ConstantExpr> Neg(); - ref<ConstantExpr> Not(); -}; - - // Utility classes class NonConstantExpr : public Expr { @@ -636,22 +479,9 @@ private: /// not parse correctly since two arrays with the same name cannot be /// distinguished once printed. Array(const std::string &_name, uint64_t _size, - const ref<ConstantExpr> *constantValuesBegin = 0, - const ref<ConstantExpr> *constantValuesEnd = 0, - Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8) - : name(_name), size(_size), domain(_domain), range(_range), - constantValues(constantValuesBegin, constantValuesEnd) { - - assert((isSymbolicArray() || constantValues.size() == size) && - "Invalid size for constant array!"); - computeHash(); -#ifndef NDEBUG - for (const ref<ConstantExpr> *it = constantValuesBegin; - it != constantValuesEnd; ++it) - assert((*it)->getWidth() == getRange() && - "Invalid initial constant value!"); -#endif //NDEBUG - } + const ref<ConstantExpr> *constantValuesBegin = 0, + const ref<ConstantExpr> *constantValuesEnd = 0, + Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8); public: bool isSymbolicArray() const { return constantValues.empty(); } @@ -1102,6 +932,157 @@ COMPARISON_EXPR_CLASS(Sle) COMPARISON_EXPR_CLASS(Sgt) COMPARISON_EXPR_CLASS(Sge) +// Terminal Exprs + +class ConstantExpr : public Expr { +public: + static const Kind kind = Constant; + static const unsigned numKids = 0; + +private: + llvm::APInt value; + + ConstantExpr(const llvm::APInt &v) : value(v) {} + +public: + ~ConstantExpr() {} + + Width getWidth() const { return value.getBitWidth(); } + Kind getKind() const { return Constant; } + + unsigned getNumKids() const { return 0; } + ref<Expr> getKid(unsigned i) const { return 0; } + + /// getAPValue - Return the arbitrary precision value directly. + /// + /// Clients should generally not use the APInt value directly and instead use + /// native ConstantExpr APIs. + const llvm::APInt &getAPValue() const { return value; } + + /// getZExtValue - Returns the constant value zero extended to the + /// return type of this method. + /// + ///\param bits - optional parameter that can be used to check that the + /// number of bits used by this constant is <= to the parameter + /// value. This is useful for checking that type casts won't truncate + /// useful bits. + /// + /// Example: unit8_t byte= (unit8_t) constant->getZExtValue(8); + uint64_t getZExtValue(unsigned bits = 64) const { + assert(getWidth() <= bits && "Value may be out of range!"); + return value.getZExtValue(); + } + + /// getLimitedValue - If this value is smaller than the specified limit, + /// return it, otherwise return the limit value. + uint64_t getLimitedValue(uint64_t Limit = ~0ULL) const { + return value.getLimitedValue(Limit); + } + + /// toString - Return the constant value as a string + /// \param Res specifies the string for the result to be placed in + /// \param radix specifies the base (e.g. 2,10,16). The default is base 10 + void toString(std::string &Res, unsigned radix = 10) const; + + int compareContents(const Expr &b) const { + const ConstantExpr &cb = static_cast<const ConstantExpr &>(b); + if (getWidth() != cb.getWidth()) + return getWidth() < cb.getWidth() ? -1 : 1; + if (value == cb.value) + return 0; + return value.ult(cb.value) ? -1 : 1; + } + + virtual ref<Expr> rebuild(ref<Expr> kids[]) const { + assert(0 && "rebuild() on ConstantExpr"); + return const_cast<ConstantExpr *>(this); + } + + virtual unsigned computeHash(); + + static ref<Expr> fromMemory(void *address, Width w); + void toMemory(void *address); + + static ref<ConstantExpr> alloc(const llvm::APInt &v) { + ref<ConstantExpr> r(new ConstantExpr(v)); + r->computeHash(); + return r; + } + + static ref<ConstantExpr> alloc(const llvm::APFloat &f) { + return alloc(f.bitcastToAPInt()); + } + + static ref<ConstantExpr> alloc(uint64_t v, Width w) { + return alloc(llvm::APInt(w, v)); + } + + static ref<ConstantExpr> create(uint64_t v, Width w) { + assert(v == bits64::truncateToNBits(v, w) && "invalid constant"); + return alloc(v, w); + } + + static bool classof(const Expr *E) { return E->getKind() == Expr::Constant; } + static bool classof(const ConstantExpr *) { return true; } + + /* Utility Functions */ + + /// isZero - Is this a constant zero. + bool isZero() const { return getAPValue().isMinValue(); } + + /// isOne - Is this a constant one. + bool isOne() const { return getLimitedValue() == 1; } + + /// isTrue - Is this the true expression. + bool isTrue() const { + return (getWidth() == Expr::Bool && value.getBoolValue() == true); + } + + /// isFalse - Is this the false expression. + bool isFalse() const { + return (getWidth() == Expr::Bool && value.getBoolValue() == false); + } + + /// isAllOnes - Is this constant all ones. + bool isAllOnes() const { return getAPValue().isAllOnesValue(); } + + /* Constant Operations */ + + ref<ConstantExpr> Concat(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Extract(unsigned offset, Width W); + ref<ConstantExpr> ZExt(Width W); + ref<ConstantExpr> SExt(Width W); + ref<ConstantExpr> Add(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Sub(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Mul(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> UDiv(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> SDiv(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> URem(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> SRem(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> And(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Or(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Xor(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Shl(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> LShr(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> AShr(const ref<ConstantExpr> &RHS); + + // Comparisons return a constant expression of width 1. + + ref<ConstantExpr> Eq(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Ne(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Ult(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Ule(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Ugt(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Uge(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Slt(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Sle(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Sgt(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Sge(const ref<ConstantExpr> &RHS); + + ref<ConstantExpr> Neg(); + ref<ConstantExpr> Not(); +}; + // Implementations inline bool Expr::isZero() const { diff --git a/include/klee/Internal/ADT/DiscretePDF.inc b/include/klee/Internal/ADT/DiscretePDF.inc index 1eb23629..5aee2de5 100644 --- a/include/klee/Internal/ADT/DiscretePDF.inc +++ b/include/klee/Internal/ADT/DiscretePDF.inc @@ -1,6 +1,11 @@ -//===- DiscretePDF.inc - --*- C++ -*-===// - +//===- DiscretePDF.inc - --*- C++ -*---------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. // +//===----------------------------------------------------------------------===// namespace klee { diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h index e7478d33..5d8aa1ab 100644 --- a/include/klee/util/Assignment.h +++ b/include/klee/util/Assignment.h @@ -49,15 +49,7 @@ namespace klee { template<typename InputIterator> bool satisfies(InputIterator begin, InputIterator end); - - void dump() { - for (bindings_ty::iterator i = bindings.begin(), e = bindings.end(); i != e; ++i) { - llvm::errs() << (*i).first->name << "\n["; - for (int j = 0, k =(*i).second.size(); j<k; ++j ) - llvm::errs() << (int)(*i).second[j] << ","; - llvm::errs() << "]\n"; - } - } + void dump(); }; class AssignmentEvaluator : public ExprEvaluator { diff --git a/include/klee/util/PrintContext.h b/include/klee/util/PrintContext.h index 6b1ef77a..a72af033 100644 --- a/include/klee/util/PrintContext.h +++ b/include/klee/util/PrintContext.h @@ -1,3 +1,12 @@ +//===-- PrintContext.h ------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #ifndef PRINTCONTEXT_H_ #define PRINTCONTEXT_H_ diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index 70ee736e..dcc1b238 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -1,3 +1,12 @@ +//===-- CmdLineOptions.cpp --------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + /* * This file groups command line options definitions and associated * data that are common to both KLEE and Kleaver. diff --git a/lib/Expr/Assigment.cpp b/lib/Expr/Assigment.cpp new file mode 100644 index 00000000..635362d4 --- /dev/null +++ b/lib/Expr/Assigment.cpp @@ -0,0 +1,25 @@ +//===-- Assignment.cpp ----------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +#include "klee/util/Assignment.h" +namespace klee { + +void Assignment::dump() { + if (bindings.size() == 0) { + llvm::errs() << "No bindings\n"; + return; + } + for (bindings_ty::iterator i = bindings.begin(), e = bindings.end(); i != e; + ++i) { + llvm::errs() << (*i).first->name << "\n["; + for (int j = 0, k = (*i).second.size(); j < k; ++j) + llvm::errs() << (int)(*i).second[j] << ","; + llvm::errs() << "]\n"; + } +} +} diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 2c64aff4..182093b9 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -481,7 +481,23 @@ ref<Expr> NotOptimizedExpr::create(ref<Expr> src) { /***/ -extern "C" void vc_DeleteExpr(void*); +Array::Array(const std::string &_name, uint64_t _size, + const ref<ConstantExpr> *constantValuesBegin, + const ref<ConstantExpr> *constantValuesEnd, Expr::Width _domain, + Expr::Width _range) + : name(_name), size(_size), domain(_domain), range(_range), + constantValues(constantValuesBegin, constantValuesEnd) { + + assert((isSymbolicArray() || constantValues.size() == size) && + "Invalid size for constant array!"); + computeHash(); +#ifndef NDEBUG + for (const ref<ConstantExpr> *it = constantValuesBegin; + it != constantValuesEnd; ++it) + assert((*it)->getWidth() == getRange() && + "Invalid initial constant value!"); +#endif // NDEBUG +} Array::~Array() { } diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index ffd3cfe9..9e1f9a62 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -1,4 +1,14 @@ - /* +//===-- MetaSMTBuilder.h ----------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + + +/* * MetaSMTBuilder.h * * Created on: 8 Aug 2012 diff --git a/scripts/IStatsMerge.py b/scripts/IStatsMerge.py index 1bd61c3e..ae87033f 100755 --- a/scripts/IStatsMerge.py +++ b/scripts/IStatsMerge.py @@ -1,5 +1,14 @@ #!/usr/bin/python +# ===-- IStatsMerge.py ----------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + from __future__ import division import sys, os diff --git a/scripts/IStatsSum.py b/scripts/IStatsSum.py index ce680c7b..0546e895 100755 --- a/scripts/IStatsSum.py +++ b/scripts/IStatsSum.py @@ -1,5 +1,14 @@ #!/usr/bin/python +# ===-- IStatsSum.py ------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + from __future__ import division import sys, os diff --git a/scripts/coverageServer.py b/scripts/coverageServer.py index db708545..841b8e5e 100644 --- a/scripts/coverageServer.py +++ b/scripts/coverageServer.py @@ -1,4 +1,14 @@ #!/usr/bin/python + +# ===-- coverageServer.py -------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + from flask import * from functools import wraps from subprocess import call diff --git a/scripts/genTempFiles.sh b/scripts/genTempFiles.sh index f77cbcea..fa6e435f 100755 --- a/scripts/genTempFiles.sh +++ b/scripts/genTempFiles.sh @@ -1,5 +1,14 @@ #!/bin/bash +# ===-- genTempFiles.sh ---------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + if [ -z "$1" ] ; then echo "No directory given" exit 1 diff --git a/scripts/klee-chroot-env b/scripts/klee-chroot-env index 3b524d8e..079714dd 100755 --- a/scripts/klee-chroot-env +++ b/scripts/klee-chroot-env @@ -1,6 +1,15 @@ #!/usr/bin/env python2 #-*- coding: utf-8 -*- # +# ===-- klee-chroot-env ---------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## +# # Buiding chroot environment for the program under test. # # This script uses `ldd' to get the shared libraries required by a program, diff --git a/scripts/klee-clang b/scripts/klee-clang index 212bc8ed..7b98a97d 100755 --- a/scripts/klee-clang +++ b/scripts/klee-clang @@ -1,5 +1,14 @@ #!/usr/bin/env python +# ===-- klee-clang --------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + import os, sys import subprocess import re diff --git a/scripts/klee-control b/scripts/klee-control index 50c1f82d..2f111524 100755 --- a/scripts/klee-control +++ b/scripts/klee-control @@ -1,5 +1,14 @@ #!/usr/bin/python +# ===-- klee-control ------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + import os, signal, popen2 def getPID(dir): diff --git a/scripts/klee-gcc b/scripts/klee-gcc index 3ed4c23a..2add2248 100755 --- a/scripts/klee-gcc +++ b/scripts/klee-gcc @@ -1,5 +1,14 @@ #!/usr/bin/env python +# ===-- klee-gcc ----- ----------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + import os, sys def isLinkCommand(): diff --git a/scripts/objdump b/scripts/objdump index ff055697..3090d383 100755 --- a/scripts/objdump +++ b/scripts/objdump @@ -1,5 +1,14 @@ #!/usr/bin/python +# ===-- objdump -----------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + """ An objdump wrapper for use with klee & kcachegrind. diff --git a/tools/gen-random-bout/gen-random-bout.cpp b/tools/gen-random-bout/gen-random-bout.cpp index 46f662dd..fca24008 100644 --- a/tools/gen-random-bout/gen-random-bout.cpp +++ b/tools/gen-random-bout/gen-random-bout.cpp @@ -1,3 +1,12 @@ +//===-- gen-random-bout.cpp -------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #include <assert.h> #include <stdio.h> #include <stdlib.h> diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index edc5f4c9..9c374eb8 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -1,3 +1,12 @@ +//===-- main.cpp ------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #include "expr/Lexer.h" #include "expr/Parser.h" diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats index 6ed772cd..93ae33d5 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -1,5 +1,15 @@ #!/usr/bin/env python # -*- encoding: utf-8 -*- + +# ===-- klee-stats --------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + """Output statistics logged by Klee.""" # use '/' to mean true division and '//' to mean floor division diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 0dfa4399..568c70bb 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -1,5 +1,14 @@ /* -*- mode: c++; c-basic-offset: 2; -*- */ +//===-- main.cpp ------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #include "klee/ExecutionState.h" #include "klee/Expr.h" #include "klee/Interpreter.h" diff --git a/tools/ktest-tool/ktest-tool b/tools/ktest-tool/ktest-tool index b7504be8..b73c6375 100755 --- a/tools/ktest-tool/ktest-tool +++ b/tools/ktest-tool/ktest-tool @@ -1,5 +1,14 @@ #!/usr/bin/env python +# ===-- ktest-tool --------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + import os import struct import sys diff --git a/unittests/Makefile b/unittests/Makefile index 175ccdd5..b7e51371 100644 --- a/unittests/Makefile +++ b/unittests/Makefile @@ -1,4 +1,11 @@ ##===- unittests/Makefile ----------------------------------*- Makefile -*-===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## LEVEL = .. diff --git a/unittests/Ref/RefTest.cpp b/unittests/Ref/RefTest.cpp index 229fd9a8..48a15885 100644 --- a/unittests/Ref/RefTest.cpp +++ b/unittests/Ref/RefTest.cpp @@ -1,3 +1,12 @@ +//===-- RefTest.cpp ---------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + /* Regression test for a bug caused by assigning a ref to itself. More details at http://keeda.stanford.edu/pipermail/klee-commits/2012-February/000904.html */ diff --git a/utils/emacs/klee-pc-mode.el b/utils/emacs/klee-pc-mode.el index 3d68b1cf..d036dddb 100644 --- a/utils/emacs/klee-pc-mode.el +++ b/utils/emacs/klee-pc-mode.el @@ -1,3 +1,12 @@ +;;===-- klee-pc-mode.el ---------------------------------------------------===;; +;; +;; The KLEE Symbolic Virtual Machine +;; +;; This file is distributed under the University of Illinois Open Source +;; License. See LICENSE.TXT for details. +;; +;;===----------------------------------------------------------------------===;; + (provide 'klee-pc-mode) (require 'font-lock) diff --git a/utils/hacks/TreeGraphs/Animate.py b/utils/hacks/TreeGraphs/Animate.py index 07f43756..03be6643 100755 --- a/utils/hacks/TreeGraphs/Animate.py +++ b/utils/hacks/TreeGraphs/Animate.py @@ -1,5 +1,14 @@ #!/usr/bin/python +# ===-- Animate.py --------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + import os import TreeGraph import Image diff --git a/utils/hacks/TreeGraphs/DumpTreeStream.py b/utils/hacks/TreeGraphs/DumpTreeStream.py index b3614c7c..0b3f0ee1 100644 --- a/utils/hacks/TreeGraphs/DumpTreeStream.py +++ b/utils/hacks/TreeGraphs/DumpTreeStream.py @@ -1,5 +1,14 @@ #!/usr/bin/python +# ===-- DumpTreeStream.py -------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + from __future__ import division import sys, os, struct diff --git a/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py b/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py index 048540ab..664ac668 100644 --- a/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py +++ b/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py @@ -1,3 +1,13 @@ +# ===-- __init__.py -------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + + from __future__ import division ### diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py b/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py index d310c20a..9e97a943 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py @@ -1,3 +1,12 @@ +# ===-- Intersect2D.py ----------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + import vec2, math def intersectLineCircle((p, no), (C, r)): diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py b/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py index 5a09be62..fc101475 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py @@ -1,3 +1,12 @@ +# ===-- mat2.py -----------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + import vec2 def det(m): diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py b/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py index c25d7e50..d2c23b1b 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py @@ -1,3 +1,12 @@ +# ===-- mat3.py -----------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + import vec3,mat2 def identity(): diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py b/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py index e927c936..3d161fe4 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py @@ -1,3 +1,12 @@ +# ===-- mat4.py -----------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + import vec4,mat3 def identity(): @@ -150,4 +159,4 @@ def inv(m): def toGL(m): m0,m1,m2,m3= m - return m0+m1+m2+m3 \ No newline at end of file + return m0+m1+m2+m3 diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py b/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py index 663d3d8c..c564a9f3 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py @@ -1,3 +1,12 @@ +# ===-- quat.py -----------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + from __future__ import division import math diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py b/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py index 73bc5717..fa4c722c 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py @@ -1,3 +1,12 @@ +# ===-- vec2.py -----------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + from __future__ import division from math import ceil,floor,sqrt,atan2,pi,cos,sin import random diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py b/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py index 48ebf129..5235f844 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py @@ -1,3 +1,12 @@ +# ===-- vec3.py -----------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + from __future__ import division from math import ceil,floor,sqrt from random import random as _random diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py b/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py index c0741bb3..398c5c51 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py @@ -1,3 +1,12 @@ +# ===-- vec4.py -----------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + from __future__ import division from math import ceil,floor,sqrt import vec3 diff --git a/utils/hacks/TreeGraphs/TreeGraph.py b/utils/hacks/TreeGraphs/TreeGraph.py index 28bd9fd6..3b4d3e96 100755 --- a/utils/hacks/TreeGraphs/TreeGraph.py +++ b/utils/hacks/TreeGraphs/TreeGraph.py @@ -1,5 +1,14 @@ #!/usr/bin/python +# ===-- TreeGraph.py ------------------------------------------------------===## +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +# ===----------------------------------------------------------------------===## + from __future__ import division import sys from types import GeneratorType |