From 179a8930253e7e81dda77fda1db11a6d11b22f14 Mon Sep 17 00:00:00 2001
From: Peter Collingbourne <peter@pcc.me.uk>
Date: Fri, 29 Jul 2011 17:49:56 +0000
Subject: Sign extend, rather than zero extend, narrow gep indices

For example, clang creates these for ++ and -- operations on pointers
on 64-bit platforms.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136474 91177308-0d34-0410-b5e6-96231b3b80d8
---
 include/klee/Expr.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'include')

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index ccbd9163..3e296934 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -230,7 +230,8 @@ public:
   /* Kind utilities */
 
   /* Utility creation functions */
-  static ref<Expr> createCoerceToPointerType(ref<Expr> e);
+  static ref<Expr> createSExtToPointerWidth(ref<Expr> e);
+  static ref<Expr> createZExtToPointerWidth(ref<Expr> e);
   static ref<Expr> createImplies(ref<Expr> hyp, ref<Expr> conc);
   static ref<Expr> createIsZero(ref<Expr> e);
 
-- 
cgit 1.4.1