diff options
| author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2016-04-17 14:25:30 +0100 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2016-04-17 14:25:30 +0100 |
| commit | c2d9fc9accea01a2f65d81bb0998fa0b3a60adaa (patch) | |
| tree | a994dc70f2b99804062b7a2a0d5eb761b3250868 /test | |
| parent | cc267845c8a4f954cdf9402ade03196be16148ea (diff) | |
| parent | 8dd640c8a0fd19047f7a30d3952e12dbac0311f7 (diff) | |
| download | klee-c2d9fc9accea01a2f65d81bb0998fa0b3a60adaa.tar.gz | |
Merge pull request #359 from delcypher/fix_indep_solver_bug
Bug fix in IndependentSolver
Diffstat (limited to 'test')
| -rw-r--r-- | test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery | 15 | ||||
| -rw-r--r-- | test/regression/lit.local.cfg | 2 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery b/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery new file mode 100644 index 00000000..9116ea47 --- /dev/null +++ b/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery @@ -0,0 +1,15 @@ +# RUN: %kleaver %s 2>&1 | FileCheck %s +array n_args[4] : w32 -> w8 = symbolic +array n_args_1[4] : w32 -> w8 = symbolic +array A-data-stat[144] : w32 -> w8 = symbolic +array stdin-stat[144] : w32 -> w8 = symbolic +(query [(Ult N0:(ReadLSB w32 0 n_args) 2) +(Slt 0 N0) +(Ult N1:(ReadLSB w32 0 n_args_1) 3) +(Slt 0 N1) +(Slt 1 N1) +(Eq false (Eq 0 (And w64 (ReadLSB w64 8 A-data-stat) 2147483647))) +(Ult (ReadLSB w64 56 A-data-stat) 65536) +(Eq false (Eq 0 (And w64 (ReadLSB w64 8 stdin-stat) 2147483647)))] +(Eq false (Ult (ReadLSB w64 56 stdin-stat) 65536)) [] [n_args]) +# CHECK: INVALID diff --git a/test/regression/lit.local.cfg b/test/regression/lit.local.cfg new file mode 100644 index 00000000..d64daf29 --- /dev/null +++ b/test/regression/lit.local.cfg @@ -0,0 +1,2 @@ +# Look for .kquery files too +config.suffixes.add('.kquery') |