about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.rules4
-rw-r--r--include/klee/ExecutionState.h107
-rw-r--r--include/klee/Internal/Module/KInstruction.h2
-rw-r--r--include/klee/Internal/Module/KModule.h2
-rw-r--r--include/klee/klee.h77
-rw-r--r--lib/Core/ExecutionState.cpp33
-rw-r--r--lib/Core/Memory.cpp4
-rw-r--r--lib/Module/RaiseAsm.cpp10
-rw-r--r--lib/Solver/STPBuilder.cpp26
-rw-r--r--runtime/Intrinsic/klee_int.c2
-rw-r--r--runtime/klee-libc/__cxa_atexit.c4
-rw-r--r--runtime/klee-libc/abort.c4
-rw-r--r--runtime/klee-libc/klee-choose.c6
-rw-r--r--runtime/klee-libc/memset.c4
-rw-r--r--test/Feature/arithmetic-right-overshift-sym-conc.c25
-rw-r--r--test/Programs/pcregrep.c4
-rw-r--r--test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c4
-rw-r--r--tools/klee/main.cpp2
18 files changed, 188 insertions, 132 deletions
diff --git a/Makefile.rules b/Makefile.rules
index 5e954adf..20e19e26 100644
--- a/Makefile.rules
+++ b/Makefile.rules
@@ -486,9 +486,9 @@ endif
 ifeq ($(HOST_OS),Darwin)
   DARWIN_VERSION := `sw_vers -productVersion`
   # Strip a number like 10.4.7 to 10.4
-  DARWIN_VERSION := $(shell echo $(DARWIN_VERSION)| sed -E 's/(10.[0-9]).*/\1/')
+  DARWIN_VERSION := $(shell echo $(DARWIN_VERSION)| sed -E 's/(10.[0-9]+).*/\1/')
   # Get "4" out of 10.4 for later pieces in the makefile.
-  DARWIN_MAJVERS := $(shell echo $(DARWIN_VERSION)| sed -E 's/10.([0-9]).*/\1/')
+  DARWIN_MAJVERS := $(shell echo $(DARWIN_VERSION)| sed -E 's/10.([0-9]+).*/\1/')
 
   SharedLinkOptions=-Wl,-flat_namespace -Wl,-undefined,suppress \
                     -dynamiclib
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 97b700c1..067a80a2 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -23,14 +23,14 @@
 #include <vector>
 
 namespace klee {
-  class Array;
-  class CallPathNode;
-  struct Cell;
-  struct KFunction;
-  struct KInstruction;
-  class MemoryObject;
-  class PTreeNode;
-  struct InstructionInfo;
+class Array;
+class CallPathNode;
+struct Cell;
+struct KFunction;
+struct KInstruction;
+class MemoryObject;
+class PTreeNode;
+struct InstructionInfo;
 
 llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm);
 
@@ -39,7 +39,7 @@ struct StackFrame {
   KFunction *kf;
   CallPathNode *callPathNode;
 
-  std::vector<const MemoryObject*> allocas;
+  std::vector<const MemoryObject *> allocas;
   Cell *locals;
 
   /// Minimum distance to an uncovered instruction once the function
@@ -61,56 +61,92 @@ struct StackFrame {
   ~StackFrame();
 };
 
+/// @brief ExecutionState representing a path under exploration
 class ExecutionState {
 public:
   typedef std::vector<StackFrame> stack_ty;
 
 private:
   // unsupported, use copy constructor
-  ExecutionState &operator=(const ExecutionState&); 
-  std::map< std::string, std::string > fnAliases;
+  ExecutionState &operator=(const ExecutionState &);
+
+  std::map<std::string, std::string> fnAliases;
 
 public:
-  bool fakeState;
-  unsigned depth;
-  
-  // pc - pointer to current instruction stream
-  KInstIterator pc, prevPC;
+  // Execution - Control Flow specific
+
+  /// @brief Pointer to instruction which is currently executed
+  KInstIterator prevPC;
+
+  /// @brief Pointer to instruction to be executed after the current
+  /// instruction
+  KInstIterator pc;
+
+  /// @brief Stack representing the current instruction stream
   stack_ty stack;
+
+  /// @brief Remember from which Basic Block control flow arrived
+  /// (i.e. to select the right phi values)
+  unsigned incomingBBIndex;
+
+  // Overall state of the state - Data specific
+
+  /// @brief Address space used by this state (e.g. Global and Heap)
+  AddressSpace addressSpace;
+
+  /// @brief Constraints collected so far
   ConstraintManager constraints;
+
+  /// Statistics and information
+
+  /// @brief Costs for all queries issued for this state, in seconds
   mutable double queryCost;
+
+  /// @brief Weight assigned for importance of this state.  Can be
+  /// used for searchers to decide what paths to explore
   double weight;
-  AddressSpace addressSpace;
-  TreeOStream pathOS, symPathOS;
+
+  /// @brief Exploration depth, i.e., number of times KLEE branched for this state
+  unsigned depth;
+
+  /// @brief History of complete path: Represents branches taken to
+  /// reach/create this state (both concrete and symbolic)
+  TreeOStream pathOS;
+
+  /// @brief History of symbolic path: Represents symbolic branches
+  /// taken to reach/create this state
+  TreeOStream symPathOS;
+
+  /// @brief Counts how many instructions were executed since the last new
+  /// instruction was covered.
   unsigned instsSinceCovNew;
+
+  /// @brief Whether a new instruction was covered in this state
   bool coveredNew;
 
-  /// Disables forking, set by user code.
+  /// @brief Disables forking for this state. Set by user code
   bool forkDisabled;
 
-  std::map<const std::string*, std::set<unsigned> > coveredLines;
+  /// @brief Set containing which lines in which files are covered by this state
+  std::map<const std::string *, std::set<unsigned> > coveredLines;
+
+  /// @brief Pointer to the process tree of the current state
   PTreeNode *ptreeNode;
 
-  /// ordered list of symbolics: used to generate test cases. 
+  /// @brief Ordered list of symbolics: used to generate test cases.
   //
   // FIXME: Move to a shared list structure (not critical).
-  std::vector< std::pair<const MemoryObject*, const Array*> > symbolics;
+  std::vector<std::pair<const MemoryObject *, const Array *> > symbolics;
 
-  /// Set of used array names.  Used to avoid collisions.
+  /// @brief Set of used array names for this state.  Used to avoid collisions.
   std::set<std::string> arrayNames;
 
-  // Used by the checkpoint/rollback methods for fake objects.
-  // FIXME: not freeing things on branch deletion.
-  MemoryMap shadowObjects;
-
-  unsigned incomingBBIndex;
-
   std::string getFnAlias(std::string fn);
   void addFnAlias(std::string old_fn, std::string new_fn);
   void removeFnAlias(std::string fn);
-  
+
 private:
-  ExecutionState() : fakeState(false), ptreeNode(0) {}
+  ExecutionState() : ptreeNode(0) {}
 
 public:
   ExecutionState(KFunction *kf);
@@ -119,24 +155,21 @@ public:
   // use on structure
   ExecutionState(const std::vector<ref<Expr> > &assumptions);
 
-  ExecutionState(const ExecutionState& state);
+  ExecutionState(const ExecutionState &state);
 
   ~ExecutionState();
-  
+
   ExecutionState *branch();
 
   void pushFrame(KInstIterator caller, KFunction *kf);
   void popFrame();
 
   void addSymbolic(const MemoryObject *mo, const Array *array);
-  void addConstraint(ref<Expr> e) { 
-    constraints.addConstraint(e); 
-  }
+  void addConstraint(ref<Expr> e) { constraints.addConstraint(e); }
 
   bool merge(const ExecutionState &b);
   void dumpStack(llvm::raw_ostream &out) const;
 };
-
 }
 
 #endif
diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h
index fc86070b..62f514ff 100644
--- a/include/klee/Internal/Module/KInstruction.h
+++ b/include/klee/Internal/Module/KInstruction.h
@@ -50,7 +50,7 @@ namespace klee {
     std::vector< std::pair<unsigned, uint64_t> > indices;
 
     /// offset - A constant offset to add to the pointer operand to execute the
-    /// insturction.
+    /// instruction.
     uint64_t offset;
   };
 }
diff --git a/include/klee/Internal/Module/KModule.h b/include/klee/Internal/Module/KModule.h
index 80672b5e..76db4694 100644
--- a/include/klee/Internal/Module/KModule.h
+++ b/include/klee/Internal/Module/KModule.h
@@ -92,7 +92,7 @@ namespace klee {
 #endif
     
     // Some useful functions to know the address of
-    llvm::Function *dbgStopPointFn, *kleeMergeFn;
+    llvm::Function *kleeMergeFn;
 
     // Our shadow versions of LLVM structures.
     std::vector<KFunction*> functions;
diff --git a/include/klee/klee.h b/include/klee/klee.h
index ce92ba37..032e5243 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -1,11 +1,11 @@
-//===-- klee.h --------------------------------------------------*- C++ -*-===//
+/*===-- klee.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 __KLEE_H__
 #define __KLEE_H__
@@ -18,51 +18,57 @@ extern "C" {
 #endif
   
   /* Add an accesible memory object at a user specified location. It
-     is the users responsibility to make sure that these memory
-     objects do not overlap. These memory objects will also
-     (obviously) not correctly interact with external function
-     calls. */
+   * is the users responsibility to make sure that these memory
+   * objects do not overlap. These memory objects will also
+   * (obviously) not correctly interact with external function
+   * calls.
+   */
   void klee_define_fixed_object(void *addr, size_t nbytes);
 
-  /// klee_make_symbolic - Make the contents of the object pointer to by \arg
-  /// addr symbolic. 
-  ///
-  /// \arg addr - The start of the object.
-  /// \arg nbytes - The number of bytes to make symbolic; currently this *must*
-  /// be the entire contents of the object.
-  /// \arg name - An optional name, used for identifying the object in messages,
-  /// output files, etc.
+  /* klee_make_symbolic - Make the contents of the object pointer to by \arg
+   * addr symbolic.
+   *
+   * \arg addr - The start of the object.
+   * \arg nbytes - The number of bytes to make symbolic; currently this *must*
+   * be the entire contents of the object.
+   * \arg name - An optional name, used for identifying the object in messages,
+   * output files, etc.
+   */
   void klee_make_symbolic(void *addr, size_t nbytes, const char *name);
 
-  /// klee_range - Construct a symbolic value in the signed interval
-  /// [begin,end).
-  ///
-  /// \arg name - An optional name, used for identifying the object in messages,
-  /// output files, etc.
+  /* klee_range - Construct a symbolic value in the signed interval
+   * [begin,end).
+   *
+   * \arg name - An optional name, used for identifying the object in messages,
+   * output files, etc.
+   */
   int klee_range(int begin, int end, const char *name);
 
-  /// klee_int - Construct an unconstrained symbolic integer.
-  ///
-  /// \arg name - An optional name, used for identifying the object in messages,
-  /// output files, etc.
+  /*  klee_int - Construct an unconstrained symbolic integer.
+   *
+   * \arg name - An optional name, used for identifying the object in messages,
+   * output files, etc.
+   */
   int klee_int(const char *name);
 
-  /// klee_silent_exit - Terminate the current KLEE process without generating a
-  /// test file.
+  /* klee_silent_exit - Terminate the current KLEE process without generating a
+   * test file.
+   */
   __attribute__((noreturn))
   void klee_silent_exit(int status);
 
-  /// klee_abort - Abort the current KLEE process.
+  /* klee_abort - Abort the current KLEE process. */
   __attribute__((noreturn))
   void klee_abort(void);  
 
-  /// klee_report_error - Report a user defined error and terminate the current
-  /// KLEE process.
-  ///
-  /// \arg file - The filename to report in the error message.
-  /// \arg line - The line number to report in the error message.
-  /// \arg message - A string to include in the error message.
-  /// \arg suffix - The suffix to use for error files.
+  /* klee_report_error - Report a user defined error and terminate the current
+   * KLEE process.
+   *
+   * \arg file - The filename to report in the error message.
+   * \arg line - The line number to report in the error message.
+   * \arg message - A string to include in the error message.
+   * \arg suffix - The suffix to use for error files.
+   */
   __attribute__((noreturn))
   void klee_report_error(const char *file, 
 			 int line, 
@@ -142,6 +148,11 @@ extern "C" {
   /* Print stack trace. */
   void klee_stack_trace(void);
 
+  /* Print range for given argument and tagged with name */
+  void klee_print_range(const char * name, int arg );
+
+  /* Merge current states together if possible */
+  void klee_merge();
 #ifdef __cplusplus
 }
 #endif
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 5d32c936..6aeaa833 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -66,13 +66,14 @@ StackFrame::~StackFrame() {
 
 /***/
 
-ExecutionState::ExecutionState(KFunction *kf) 
-  : fakeState(false),
-    depth(0),
+ExecutionState::ExecutionState(KFunction *kf) :
     pc(kf->instructions),
     prevPC(pc),
+
     queryCost(0.), 
     weight(1),
+    depth(0),
+
     instsSinceCovNew(0),
     coveredNew(false),
     forkDisabled(false),
@@ -80,12 +81,8 @@ ExecutionState::ExecutionState(KFunction *kf)
   pushFrame(0, kf);
 }
 
-ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions) 
-  : fakeState(true),
-    constraints(assumptions),
-    queryCost(0.),
-    ptreeNode(0) {
-}
+ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions)
+    : constraints(assumptions), queryCost(0.), ptreeNode(0) {}
 
 ExecutionState::~ExecutionState() {
   for (unsigned int i=0; i<symbolics.size(); i++)
@@ -100,28 +97,30 @@ ExecutionState::~ExecutionState() {
   while (!stack.empty()) popFrame();
 }
 
-ExecutionState::ExecutionState(const ExecutionState& state)
-  : fnAliases(state.fnAliases),
-    fakeState(state.fakeState),
-    depth(state.depth),
+ExecutionState::ExecutionState(const ExecutionState& state):
+    fnAliases(state.fnAliases),
     pc(state.pc),
     prevPC(state.prevPC),
     stack(state.stack),
+    incomingBBIndex(state.incomingBBIndex),
+
+    addressSpace(state.addressSpace),
     constraints(state.constraints),
+
     queryCost(state.queryCost),
     weight(state.weight),
-    addressSpace(state.addressSpace),
+    depth(state.depth),
+
     pathOS(state.pathOS),
     symPathOS(state.symPathOS),
+
     instsSinceCovNew(state.instsSinceCovNew),
     coveredNew(state.coveredNew),
     forkDisabled(state.forkDisabled),
     coveredLines(state.coveredLines),
     ptreeNode(state.ptreeNode),
     symbolics(state.symbolics),
-    arrayNames(state.arrayNames),
-    shadowObjects(state.shadowObjects),
-    incomingBBIndex(state.incomingBBIndex)
+    arrayNames(state.arrayNames)
 {
   for (unsigned int i=0; i<symbolics.size(); i++)
     symbolics[i].first->refCount++;
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 1dd1e1fd..07c292a0 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -468,7 +468,7 @@ ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const {
 
   // Otherwise, follow the slow general case.
   unsigned NumBytes = width / 8;
-  assert(width == NumBytes * 8 && "Invalid write size!");
+  assert(width == NumBytes * 8 && "Invalid read size!");
   ref<Expr> Res(0);
   for (unsigned i = 0; i != NumBytes; ++i) {
     unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
@@ -488,7 +488,7 @@ ref<Expr> ObjectState::read(unsigned offset, Expr::Width width) const {
 
   // Otherwise, follow the slow general case.
   unsigned NumBytes = width / 8;
-  assert(width == NumBytes * 8 && "Invalid write size!");
+  assert(width == NumBytes * 8 && "Invalid width for read size!");
   ref<Expr> Res(0);
   for (unsigned i = 0; i != NumBytes; ++i) {
     unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp
index d9145a1e..12e5479b 100644
--- a/lib/Module/RaiseAsm.cpp
+++ b/lib/Module/RaiseAsm.cpp
@@ -66,17 +66,18 @@ bool RaiseAsmPass::runOnModule(Module &M) {
   std::string HostTriple = llvm::sys::getHostTriple();
 #endif
   const Target *NativeTarget = TargetRegistry::lookupTarget(HostTriple, Err);
+  TargetMachine * TM = 0;
   if (NativeTarget == 0) {
     llvm::errs() << "Warning: unable to select native target: " << Err << "\n";
     TLI = 0;
   } else {
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
-    TargetMachine *TM = NativeTarget->createTargetMachine(HostTriple, "", "",
+    TM = NativeTarget->createTargetMachine(HostTriple, "", "",
                                                           TargetOptions());
 #elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 0)
-    TargetMachine *TM = NativeTarget->createTargetMachine(HostTriple, "", "");
+    TM = NativeTarget->createTargetMachine(HostTriple, "", "");
 #else
-    TargetMachine *TM = NativeTarget->createTargetMachine(HostTriple, "");
+    TM = NativeTarget->createTargetMachine(HostTriple, "");
 #endif
     TLI = TM->getTargetLowering();
   }
@@ -91,5 +92,8 @@ bool RaiseAsmPass::runOnModule(Module &M) {
     }
   }
 
+  if (TM)
+    delete TM;
+
   return changed;
 }
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 6d7dd8b7..a5e4c5ad 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -51,11 +51,6 @@ namespace {
 
 
 STPArrayExprHash::~STPArrayExprHash() {
-  
-  // Design decision: STPArrayExprHash is destroyed from the destructor of STPBuilder at the end of the KLEE run;
-  // Therefore, freeing memory allocated for STP::VCExpr's is currently disabled.
-  
-   /*
   for (ArrayHashIter it = _array_hash.begin(); it != _array_hash.end(); ++it) {
     ::VCExpr array_expr = it->second;
     if (array_expr) {
@@ -63,16 +58,16 @@ STPArrayExprHash::~STPArrayExprHash() {
       array_expr = 0;
     }
   }
-  
-  
-  for (UpdateNodeHashConstIter it = _update_node_hash.begin(); it != _update_node_hash.end(); ++it) {
+
+
+  for (UpdateNodeHashConstIter it = _update_node_hash.begin();
+      it != _update_node_hash.end(); ++it) {
     ::VCExpr un_expr = it->second;
     if (un_expr) {
       ::vc_DeleteExpr(un_expr);
       un_expr = 0;
     }
   }
-  */
 }
 
 /***/
@@ -218,10 +213,9 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) {
   }
 
   // If overshifting, shift to zero
-  res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
-                   res,
-                   bvZero(width));
+  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
+
+  res = vc_iteExpr(vc, ex, res, bvZero(width));
   return res;
 }
 
@@ -239,8 +233,9 @@ ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) {
   }
 
   // If overshifting, shift to zero
+  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   ex,
                    res,
                    bvZero(width));
   return res;
@@ -269,8 +264,9 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) {
   }
 
   // If overshifting, shift to zero
+  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   ex,
                    res,
                    bvZero(width));
   return res;
diff --git a/runtime/Intrinsic/klee_int.c b/runtime/Intrinsic/klee_int.c
index 56f0f9dc..6ea1e02e 100644
--- a/runtime/Intrinsic/klee_int.c
+++ b/runtime/Intrinsic/klee_int.c
@@ -8,7 +8,7 @@
 //===----------------------------------------------------------------------===//
 
 #include <assert.h>
-#include <klee/klee.h>
+#include "klee/klee.h"
 
 int klee_int(const char *name) {
   int x;
diff --git a/runtime/klee-libc/__cxa_atexit.c b/runtime/klee-libc/__cxa_atexit.c
index e7982848..990b645d 100644
--- a/runtime/klee-libc/__cxa_atexit.c
+++ b/runtime/klee-libc/__cxa_atexit.c
@@ -1,11 +1,11 @@
-//===-- __cxa_atexit.c ----------------------------------------------------===//
+/*===-- __cxa_atexit.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/klee.h"
 
diff --git a/runtime/klee-libc/abort.c b/runtime/klee-libc/abort.c
index 0332d095..741bcf82 100644
--- a/runtime/klee-libc/abort.c
+++ b/runtime/klee-libc/abort.c
@@ -1,11 +1,11 @@
-//===-- abort.c -----------------------------------------------------------===//
+/*===-- abort.c -----------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <stdlib.h>
 
diff --git a/runtime/klee-libc/klee-choose.c b/runtime/klee-libc/klee-choose.c
index 181aedaa..44e5cea2 100644
--- a/runtime/klee-libc/klee-choose.c
+++ b/runtime/klee-libc/klee-choose.c
@@ -1,11 +1,11 @@
-//===-- klee-choose.c -----------------------------------------------------===//
+/*===-- klee-choose.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/klee.h"
 
@@ -13,7 +13,7 @@ uintptr_t klee_choose(uintptr_t n) {
   uintptr_t x;
   klee_make_symbolic(&x, sizeof x, "klee_choose");
 
-  // NB: this will *not* work if they don't compare to n values.
+  /* NB: this will *not* work if they don't compare to n values. */
   if(x >= n)
     klee_silent_exit(0);
   return x;
diff --git a/runtime/klee-libc/memset.c b/runtime/klee-libc/memset.c
index ee9ecb87..81025d32 100644
--- a/runtime/klee-libc/memset.c
+++ b/runtime/klee-libc/memset.c
@@ -1,11 +1,11 @@
-//===-- memset.c ----------------------------------------------------------===//
+/*===-- memset.c ----------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
-//===----------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===*/
 
 #include <stdlib.h>
 
diff --git a/test/Feature/arithmetic-right-overshift-sym-conc.c b/test/Feature/arithmetic-right-overshift-sym-conc.c
index a771bc75..7af6f9d7 100644
--- a/test/Feature/arithmetic-right-overshift-sym-conc.c
+++ b/test/Feature/arithmetic-right-overshift-sym-conc.c
@@ -15,11 +15,13 @@ typedef enum
 
 // We're using signed ints so should be doing
 // arithmetic right shift.
-int overshift(volatile unsigned int y, const char * type)
+// lhs should be a constant
+int overshift(signed int lhs, volatile unsigned int y, const char * type)
 {
     overshift_t ret;
-    volatile signed int x=15;
+    volatile signed int x = lhs;
     unsigned int limit = sizeof(x)*8;
+    assert(!klee_is_symbolic(x));
 
     volatile signed int result;
     result = x >> y; // Potential overshift
@@ -45,10 +47,13 @@ int overshift(volatile unsigned int y, const char * type)
 
 int main(int argc, char** argv)
 {
-    // Concrete overshift
     volatile unsigned int y = sizeof(unsigned int)*8;
-    overshift_t conc = overshift(y, "Concrete");
-    assert( conc == TO_ZERO);
+    // Try with +ve lhs
+    overshift_t conc = overshift(15, y, "Concrete");
+    assert(conc == TO_ZERO);
+    // Try with -ve lhs
+    conc = overshift(-1, y, "Concrete");
+    assert(conc == TO_ZERO);
 
     // Symbolic overshift
     volatile unsigned int y2;
@@ -56,11 +61,15 @@ int main(int argc, char** argv)
     // Add constraints so only one value possible
     klee_assume(y2 > (y-1));
     klee_assume(y2 < (y+1));
-    overshift_t sym = overshift(y2, "Symbolic");
-    assert( sym == TO_ZERO);
+    // Try with +ve lhs
+    overshift_t sym = overshift(15, y2, "Symbolic");
+    assert(sym == TO_ZERO);
+    // Try with -ve lhs
+    sym = overshift(-1, y2, "Symbolic");
+    assert(sym == TO_ZERO);
 
     // Concrete and symbolic behaviour should be the same
-    assert( conc == sym);
+    assert(conc == sym);
 
     return 0;
 }
diff --git a/test/Programs/pcregrep.c b/test/Programs/pcregrep.c
index fb99ef87..5ed8f4fa 100644
--- a/test/Programs/pcregrep.c
+++ b/test/Programs/pcregrep.c
@@ -211,7 +211,7 @@ struct l_struct_2E_pcre {
 /* Function Declarations */
 double fmod(double, double);
 float fmodf(float, float);
-unsigned int main(unsigned int llvm_cbe_argc, unsigned char **llvm_cbe_argv);
+int main(int llvm_cbe_argc, char **llvm_cbe_argv);
 unsigned int fprintf(struct l_struct_2E__IO_FILE *, unsigned char *, ...);
 unsigned int __strtol_internal(unsigned char *, unsigned char **, unsigned int , unsigned int );
 unsigned int printf(unsigned char *, ...);
@@ -319,7 +319,7 @@ static inline int llvm_fcmp_ogt(double X, double Y) { return X >  Y ; }
 static inline int llvm_fcmp_ole(double X, double Y) { return X <= Y ; }
 static inline int llvm_fcmp_oge(double X, double Y) { return X >= Y ; }
 
-unsigned int main(unsigned int llvm_cbe_argc, unsigned char **llvm_cbe_argv) {
+int main(int llvm_cbe_argc, char **llvm_cbe_argv) {
   unsigned int llvm_cbe_length_i_i;    /* Address-exposed local */
   unsigned int llvm_cbe_firstbyte_i_i;    /* Address-exposed local */
   unsigned int llvm_cbe_reqbyte_i_i;    /* Address-exposed local */
diff --git a/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c b/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c
index 71f6d07a..d82f0eb9 100644
--- a/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c
+++ b/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c
@@ -5,10 +5,12 @@
 #include <string.h>
 #include <assert.h>
 
+#include "klee/klee.h"
+
 int main() {
   int a;
 
-  klee_make_symbolic(&a, sizeof a);
+  klee_make_symbolic(&a, sizeof a, "a");
 
   memset(&a, 0, sizeof a);
 
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 8a246685..08eacac1 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -1092,6 +1092,8 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
   replaceOrRenameFunction(mainModule, "__libc_open", "open");
   replaceOrRenameFunction(mainModule, "__libc_fcntl", "fcntl");
 
+  // Take care of fortified functions
+  replaceOrRenameFunction(mainModule, "__fprintf_chk", "fprintf");
 
   // XXX we need to rearchitect so this can also be used with
   // programs externally linked with uclibc.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-10-05 17:19:50 +0000