From 03eca4ba3255665bd4b2e246b92f63cc2b06a1bf Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Tue, 16 Jun 2009 02:26:40 +0000
Subject: Start SimplifyingExprBuilder  - Normalize Ne, Ugt, Uge, Slt, Sge

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73458 91177308-0d34-0410-b5e6-96231b3b80d8
---
 test/Expr/Parser/Simplify.pc | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 test/Expr/Parser/Simplify.pc

(limited to 'test/Expr/Parser')

diff --git a/test/Expr/Parser/Simplify.pc b/test/Expr/Parser/Simplify.pc
new file mode 100644
index 00000000..cf6d90ab
--- /dev/null
+++ b/test/Expr/Parser/Simplify.pc
@@ -0,0 +1,28 @@
+# RUN: %kleaver --builder=simplify -print-ast %s > %t
+
+array a[64] : w32 -> w8 = symbolic
+
+# Check -- X u> Y ==> Y u< X
+# RUN: grep -A 2 \"# Query 1\" %t > %t2
+# RUN: grep \"(query .. false .(Ult (Read w8 1 a) (Read w8 0 a)).)\" %t2
+(query [] false [(Ugt (Read w8 0 a) (Read w8 1 a))])
+
+# Check -- X u>= Y ==> Y u<= X
+# RUN: grep -A 2 \"# Query 2\" %t > %t2
+# RUN: grep \"(query .. false .(Ule (Read w8 1 a) (Read w8 0 a)).)\" %t2
+(query [] false [(Uge (Read w8 0 a) (Read w8 1 a))])
+
+# Check -- X u> Y ==> Y u< X
+# RUN: grep -A 2 \"# Query 3\" %t > %t2
+# RUN: grep \"(query .. false .(Slt (Read w8 1 a) (Read w8 0 a)).)\" %t2
+(query [] false [(Sgt (Read w8 0 a) (Read w8 1 a))])
+
+# Check -- X u>= Y ==> Y u<= X
+# RUN: grep -A 2 \"# Query 4\" %t > %t2
+# RUN: grep \"(query .. false .(Sle (Read w8 1 a) (Read w8 0 a)).)\" %t2
+(query [] false [(Sge (Read w8 0 a) (Read w8 1 a))])
+
+# Check -- X != Y ==> !(X == Y)
+# RUN: grep -A 2 \"# Query 5\" %t > %t2
+# RUN: grep \"(query .. false .(Not (Eq (Read w8 0 a) (Read w8 1 a))).)\" %t2
+(query [] false [(Ne (Read w8 0 a) (Read w8 1 a))])
-- 
cgit 1.4.1