From edfa29e836087cb61f33afcac40640be5f36341a Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Wed, 19 Apr 2023 19:20:55 +0100 Subject: Tests: replaced "-data" and "-stat" by "_data" and "_stat" for consistency with recent changes. --- test/Solver/2016-04-12-array-parsing-bug.kquery | 56 +++++++++++----------- test/Solver/FastCexSolver.kquery | 4 +- ...ce-solver-missing-objects-for-assignment.kquery | 12 ++--- 3 files changed, 36 insertions(+), 36 deletions(-) (limited to 'test') diff --git a/test/Solver/2016-04-12-array-parsing-bug.kquery b/test/Solver/2016-04-12-array-parsing-bug.kquery index d53fa35f..3df785b8 100644 --- a/test/Solver/2016-04-12-array-parsing-bug.kquery +++ b/test/Solver/2016-04-12-array-parsing-bug.kquery @@ -1,8 +1,8 @@ # RUN: %kleaver %s > %t # RUN: %kleaver --clear-array-decls-after-query %s > %t -array A-data[8] : w32 -> w8 = symbolic -array A-data-stat[144] : w32 -> w8 = symbolic +array A_data[8] : w32 -> w8 = symbolic +array A_data_stat[144] : w32 -> w8 = symbolic array arg0[3] : w32 -> w8 = symbolic array arg1[3] : w32 -> w8 = symbolic array const_arr1[768] : w32 -> w8 = [0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 3 32 2 32 2 32 2 32 2 32 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 1 96 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 4 192 4 192 4 192 4 192 4 192 4 192 4 192 8 213 8 213 8 213 8 213 8 213 8 213 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 4 192 4 192 4 192 4 192 4 192 4 192 8 214 8 214 8 214 8 214 8 214 8 214 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 4 192 4 192 4 192 4 192 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0] @@ -11,9 +11,9 @@ array model_version[4] : w32 -> w8 = symbolic array n_args[4] : w32 -> w8 = symbolic array n_args_1[4] : w32 -> w8 = symbolic array stdin[8] : w32 -> w8 = symbolic -array stdin-stat[144] : w32 -> w8 = symbolic +array stdin_stat[144] : w32 -> w8 = symbolic array stdout[1024] : w32 -> w8 = symbolic -array stdout-stat[144] : w32 -> w8 = symbolic +array stdout_stat[144] : w32 -> w8 = symbolic (query [(Ult N0:(ReadLSB w32 0 n_args) 2) (Eq false (Slt 0 N0)) @@ -23,21 +23,21 @@ array stdout-stat[144] : w32 -> w8 = symbolic (Slt 1 N1) (Eq false (Eq 0 - (And w64 (ReadLSB w64 8 A-data-stat) + (And w64 (ReadLSB w64 8 A_data_stat) 2147483647))) - (Ult (ReadLSB w64 56 A-data-stat) + (Ult (ReadLSB w64 56 A_data_stat) 65536) (Eq false (Eq 0 - (And w64 (ReadLSB w64 8 stdin-stat) + (And w64 (ReadLSB w64 8 stdin_stat) 2147483647))) - (Ult (ReadLSB w64 56 stdin-stat) + (Ult (ReadLSB w64 56 stdin_stat) 65536) (Eq false (Eq 0 - (And w64 (ReadLSB w64 8 stdout-stat) + (And w64 (ReadLSB w64 8 stdout_stat) 2147483647))) - (Ult (ReadLSB w64 56 stdout-stat) + (Ult (ReadLSB w64 56 stdout_stat) 65536) (Eq 1 (ReadLSB w32 0 model_version)) @@ -83,25 +83,25 @@ array stdout-stat[144] : w32 -> w8 = symbolic n_args_1 arg0 arg1 - A-data - A-data-stat + A_data + A_data_stat stdin - stdin-stat + stdin_stat stdout - stdout-stat + stdout_stat model_version]) -array A-data[8] : w32 -> w8 = symbolic -array A-data-stat[144] : w32 -> w8 = symbolic +array A_data[8] : w32 -> w8 = symbolic +array A_data_stat[144] : w32 -> w8 = symbolic array arg0[11] : w32 -> w8 = symbolic array arg1[3] : w32 -> w8 = symbolic array model_version[4] : w32 -> w8 = symbolic array n_args[4] : w32 -> w8 = symbolic array n_args_1[4] : w32 -> w8 = symbolic array stdin[8] : w32 -> w8 = symbolic -array stdin-stat[144] : w32 -> w8 = symbolic +array stdin_stat[144] : w32 -> w8 = symbolic array stdout[1024] : w32 -> w8 = symbolic -array stdout-stat[144] : w32 -> w8 = symbolic +array stdout_stat[144] : w32 -> w8 = symbolic (query [(Ult N0:(ReadLSB w32 0 n_args) 2) (Slt 0 N0) @@ -111,21 +111,21 @@ array stdout-stat[144] : w32 -> w8 = symbolic (Eq false (Slt 1 N1)) (Eq false (Eq 0 - (And w64 (ReadLSB w64 8 A-data-stat) + (And w64 (ReadLSB w64 8 A_data_stat) 2147483647))) - (Ult (ReadLSB w64 56 A-data-stat) + (Ult (ReadLSB w64 56 A_data_stat) 65536) (Eq false (Eq 0 - (And w64 (ReadLSB w64 8 stdin-stat) + (And w64 (ReadLSB w64 8 stdin_stat) 2147483647))) - (Ult (ReadLSB w64 56 stdin-stat) + (Ult (ReadLSB w64 56 stdin_stat) 65536) (Eq false (Eq 0 - (And w64 (ReadLSB w64 8 stdout-stat) + (And w64 (ReadLSB w64 8 stdout_stat) 2147483647))) - (Ult (ReadLSB w64 56 stdout-stat) + (Ult (ReadLSB w64 56 stdout_stat) 65536) (Eq 1 (ReadLSB w32 0 model_version)) @@ -218,10 +218,10 @@ array stdout-stat[144] : w32 -> w8 = symbolic arg0 n_args_1 arg1 - A-data - A-data-stat + A_data + A_data_stat stdin - stdin-stat + stdin_stat stdout - stdout-stat + stdout_stat model_version]) \ No newline at end of file diff --git a/test/Solver/FastCexSolver.kquery b/test/Solver/FastCexSolver.kquery index b3ec63e3..0fc1d704 100644 --- a/test/Solver/FastCexSolver.kquery +++ b/test/Solver/FastCexSolver.kquery @@ -4,7 +4,7 @@ array arr1[4] : w32 -> w8 = symbolic (query [] (Not (Eq 4096 (ReadLSB w32 0 arr1)))) -array A-data[2] : w32 -> w8 = symbolic -(query [(Ule (Add w8 208 N0:(Read w8 0 A-data)) +array A_data[2] : w32 -> w8 = symbolic +(query [(Ule (Add w8 208 N0:(Read w8 0 A_data)) 9)] (Eq 52 N0)) 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 index 9116ea47..d2deabbe 100644 --- 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 @@ -1,15 +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 +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]) +(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 -- cgit 1.4.1