From 74207d25c0a7a15641f26f81ebe5546195f7d82c Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Tue, 19 Nov 2024 15:33:44 +0100 Subject: [PATCH] test: Update --- .../CoverageBranches/btor2c-lazyMod.h_b04.c | 133 ------------------ .../CoverageErrorCall/01_fuzzle_30x30.c | 1 - .../12_fuzzle_50x50_CVE-2016-4492.c | 4 +- .../CoverageErrorCall/btor2c-lazyMod.mul6.c | 4 +- .../egcd3-ll_unwindbound10.c | 4 +- .../if_etherip-unreach-call.c | 4 +- test/Industry/CoverageErrorCall/od-4.c | 4 +- 7 files changed, 15 insertions(+), 139 deletions(-) delete mode 100644 test/Industry/CoverageBranches/btor2c-lazyMod.h_b04.c diff --git a/test/Industry/CoverageBranches/btor2c-lazyMod.h_b04.c b/test/Industry/CoverageBranches/btor2c-lazyMod.h_b04.c deleted file mode 100644 index bc6506c601..0000000000 --- a/test/Industry/CoverageBranches/btor2c-lazyMod.h_b04.c +++ /dev/null @@ -1,133 +0,0 @@ -// This file is part of the SV-Benchmarks collection of verification tasks: -// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks -// -// SPDX-FileCopyrightText: 2020 Aman Goel -// SPDX-FileCopyrightText: 2022 The SV-Benchmarks Community -// -// SPDX-License-Identifier: GPL-3.0-or-later - -// This C program is converted from Btor2 by Btor2C version sha1:a0fa249 -// with arguments: { architecture=64, lazy_modulo=true, use_memmove=false, unroll_inner_loops=false, shortest_type=true, diff_type=true, decimal_constant=true, zero_init=false, sra_extend_sign=true } -// Comments from the original Btor2 file: -// ; source: https://github.com/aman-goel/avr/tree/92362931700b66684418a991d018c9fbdbebc06f/tests -// ; BTOR description generated by Yosys 0.9+431 (git sha1 4a3b5437, clang 4.0.1-6 -fPIC -Os) for module main. -extern unsigned char __VERIFIER_nondet_uchar(); -extern unsigned short __VERIFIER_nondet_ushort(); -extern unsigned int __VERIFIER_nondet_uint(); -extern unsigned long __VERIFIER_nondet_ulong(); -extern void abort(void); -extern void __assert_fail(const char *, const char *, unsigned int, const char *); -void reach_error() { __assert_fail("0", "h_b04.c", 0, "reach_error"); } -void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: { reach_error(); abort(); } } } -void assume_abort_if_not(int cond) { if (!cond) { abort(); } } -int main() { - // Defining sorts ... - typedef unsigned char SORT_1; // BV with 1 bits - const SORT_1 mask_SORT_1 = (SORT_1)-1 >> (sizeof(SORT_1) * 8 - 1); - const SORT_1 msb_SORT_1 = (SORT_1)1 << (1 - 1); - typedef unsigned char SORT_4; // BV with 8 bits - const SORT_4 mask_SORT_4 = (SORT_4)-1 >> (sizeof(SORT_4) * 8 - 8); - const SORT_4 msb_SORT_4 = (SORT_4)1 << (8 - 1); - typedef unsigned int SORT_12; // BV with 32 bits - const SORT_12 mask_SORT_12 = (SORT_12)-1 >> (sizeof(SORT_12) * 8 - 32); - const SORT_12 msb_SORT_12 = (SORT_12)1 << (32 - 1); - // Initializing constants ... - const SORT_4 var_8 = 0; - const SORT_12 var_14 = 1; - const SORT_1 var_25 = 1; - const SORT_1 var_42 = 0; - // Collecting input declarations ... - SORT_1 input_2; - SORT_1 input_3; - SORT_4 input_5; - SORT_1 input_6; - SORT_1 input_7; - SORT_4 input_29; - SORT_4 input_31; - SORT_4 input_33; - SORT_4 input_35; - SORT_4 input_37; - SORT_4 input_39; - // Collecting state declarations ... - SORT_4 state_9 = __VERIFIER_nondet_uchar() & mask_SORT_4; - SORT_4 state_17 = __VERIFIER_nondet_uchar() & mask_SORT_4; - SORT_1 state_43 = __VERIFIER_nondet_uchar() & mask_SORT_1; - // Initializing states ... - SORT_4 init_10_arg_1 = var_8; - state_9 = init_10_arg_1; - SORT_4 init_18_arg_1 = var_8; - state_17 = init_18_arg_1; - SORT_1 init_44_arg_1 = var_42; - state_43 = init_44_arg_1; - for (;;) { - // Getting external input values ... - input_2 = __VERIFIER_nondet_uchar(); - input_3 = __VERIFIER_nondet_uchar(); - input_5 = __VERIFIER_nondet_uchar(); - input_6 = __VERIFIER_nondet_uchar(); - input_7 = __VERIFIER_nondet_uchar(); - input_29 = __VERIFIER_nondet_uchar(); - input_31 = __VERIFIER_nondet_uchar(); - input_33 = __VERIFIER_nondet_uchar(); - input_35 = __VERIFIER_nondet_uchar(); - input_37 = __VERIFIER_nondet_uchar(); - input_39 = __VERIFIER_nondet_uchar(); - // Assuming invariants ... - // Asserting properties ... - SORT_4 var_11_arg_0 = state_9; - SORT_1 var_11 = var_11_arg_0 >> 7; - SORT_1 var_13_arg_0 = var_11; - var_13_arg_0 = var_13_arg_0 & mask_SORT_1; - SORT_12 var_13 = var_13_arg_0; - SORT_12 var_15_arg_0 = var_13; - SORT_12 var_15_arg_1 = var_14; - SORT_1 var_15 = var_15_arg_0 == var_15_arg_1; - SORT_1 var_16_arg_0 = var_15; - SORT_1 var_16 = ~var_16_arg_0; - SORT_4 var_19_arg_0 = state_17; - SORT_1 var_19 = var_19_arg_0 >> 7; - SORT_1 var_20_arg_0 = var_19; - var_20_arg_0 = var_20_arg_0 & mask_SORT_1; - SORT_12 var_20 = var_20_arg_0; - SORT_12 var_21_arg_0 = var_20; - SORT_12 var_21_arg_1 = var_14; - SORT_1 var_21 = var_21_arg_0 == var_21_arg_1; - SORT_1 var_22_arg_0 = var_16; - SORT_1 var_22_arg_1 = var_21; - SORT_1 var_22 = var_22_arg_0 | var_22_arg_1; - SORT_1 var_26_arg_0 = var_22; - SORT_1 var_26 = ~var_26_arg_0; - SORT_1 var_27_arg_0 = var_25; - SORT_1 var_27_arg_1 = var_26; - SORT_1 var_27 = var_27_arg_0 & var_27_arg_1; - var_27 = var_27 & mask_SORT_1; - SORT_1 bad_28_arg_0 = var_27; - __VERIFIER_assert(!(bad_28_arg_0)); - // Computing next states ... - SORT_1 var_45_arg_0 = state_43; - SORT_4 var_45_arg_1 = input_5; - SORT_4 var_45_arg_2 = state_9; - SORT_4 var_45 = var_45_arg_0 ? var_45_arg_1 : var_45_arg_2; - SORT_4 next_46_arg_1 = var_45; - SORT_1 var_47_arg_0 = state_43; - SORT_4 var_47_arg_1 = input_5; - SORT_4 var_47_arg_2 = state_17; - SORT_4 var_47 = var_47_arg_0 ? var_47_arg_1 : var_47_arg_2; - SORT_4 next_48_arg_1 = var_47; - SORT_1 var_49_arg_0 = state_43; - SORT_1 var_49_arg_1 = var_42; - SORT_1 var_49_arg_2 = var_25; - SORT_1 var_49 = var_49_arg_0 ? var_49_arg_1 : var_49_arg_2; - var_49 = var_49 & mask_SORT_1; - SORT_1 next_50_arg_1 = var_49; - // Assigning next states ... - state_9 = next_46_arg_1; - state_17 = next_48_arg_1; - state_43 = next_50_arg_1; - } - return 0; -} - -// REQUIRES: bitwuzla -// REQUIRES: target-x86_64 -// RUN: %kleef --property-file=%S/coverage-branches.prp --max-memory=7000000000 --max-cputime-soft=300 --64 --debug %s 2>&1 | FileCheck %s diff --git a/test/Industry/CoverageErrorCall/01_fuzzle_30x30.c b/test/Industry/CoverageErrorCall/01_fuzzle_30x30.c index 69ea13472e..c1852a473e 100644 --- a/test/Industry/CoverageErrorCall/01_fuzzle_30x30.c +++ b/test/Industry/CoverageErrorCall/01_fuzzle_30x30.c @@ -1,6 +1,5 @@ // It requires bitwuzla because the script currently runs with bitwuzla solver backend // REQUIRES: bitwuzla -// REQUIRES: target-x86_64 // RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=900 --64 --debug %s 2>&1 | FileCheck %s // CHECK: KLEE: WARNING: 100.00% Reachable Reachable diff --git a/test/Industry/CoverageErrorCall/12_fuzzle_50x50_CVE-2016-4492.c b/test/Industry/CoverageErrorCall/12_fuzzle_50x50_CVE-2016-4492.c index c279f45ce0..57d5950229 100644 --- a/test/Industry/CoverageErrorCall/12_fuzzle_50x50_CVE-2016-4492.c +++ b/test/Industry/CoverageErrorCall/12_fuzzle_50x50_CVE-2016-4492.c @@ -1,6 +1,8 @@ // It requires bitwuzla because the script currently runs with bitwuzla solver backend // REQUIRES: bitwuzla -// REQUIRES: target-x86_64 +// REQUIRES: not-asan +// REQUIRES: not-msan +// REQUIRES: not-darwin // RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=900 --64 --debug %s 2>&1 | FileCheck %s // CHECK: KLEE: WARNING: 100.00% Reachable Reachable diff --git a/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c b/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c index 2b02777d57..22213de4e9 100644 --- a/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c +++ b/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c @@ -1,6 +1,8 @@ // It requires bitwuzla because the script currently runs with bitwuzla solver backend // REQUIRES: bitwuzla -// REQUIRES: target-x86_64 +// REQUIRES: not-asan +// REQUIRES: not-msan +// REQUIRES: not-darwin // RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=30 --64 --debug %s 2>&1 | FileCheck %s // CHECK: KLEE: WARNING: 100.00% Reachable Reachable diff --git a/test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c b/test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c index 27e10cadca..dfb550f73e 100644 --- a/test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c +++ b/test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c @@ -76,6 +76,8 @@ int main() { // It requires bitwuzla because the script currently runs with bitwuzla solver backend // REQUIRES: bitwuzla -// REQUIRES: target-x86_64 +// REQUIRES: not-asan +// REQUIRES: not-msan +// REQUIRES: not-darwin // RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=60 --32 --debug --write-ktests %s 2>&1 | FileCheck %s // CHECK: KLEE: WARNING: 100.00% Reachable Reachable diff --git a/test/Industry/CoverageErrorCall/if_etherip-unreach-call.c b/test/Industry/CoverageErrorCall/if_etherip-unreach-call.c index 776c2f9673..64dfb50646 100644 --- a/test/Industry/CoverageErrorCall/if_etherip-unreach-call.c +++ b/test/Industry/CoverageErrorCall/if_etherip-unreach-call.c @@ -1,6 +1,8 @@ // It requires bitwuzla because the script currently runs with bitwuzla solver backend // REQUIRES: bitwuzla -// REQUIRES: target-x86_64 +// REQUIRES: not-asan +// REQUIRES: not-msan +// REQUIRES: not-darwin // RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=30 --64 --debug %s 2>&1 | FileCheck %s // CHECK: KLEE: WARNING: 100.00% Reachable Reachable diff --git a/test/Industry/CoverageErrorCall/od-4.c b/test/Industry/CoverageErrorCall/od-4.c index 758fa8d026..d5571e2953 100644 --- a/test/Industry/CoverageErrorCall/od-4.c +++ b/test/Industry/CoverageErrorCall/od-4.c @@ -1,6 +1,8 @@ // It requires bitwuzla because the script currently runs with bitwuzla solver backend // REQUIRES: bitwuzla -// REQUIRES: target-x86_64 +// REQUIRES: not-asan +// REQUIRES: not-msan +// REQUIRES: not-darwin // RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=180 --64 --debug %s 2>&1 | FileCheck %s // CHECK: KLEE: WARNING: 100.00% Reachable Reachable