42 lines
2.5 KiB
Shell
Executable file
42 lines
2.5 KiB
Shell
Executable file
#!/usr/bin/env bash
|
|
# flowrs-core's proofs: the widgets' index, range and geometry rules the interpreter and the
|
|
# generated code share (crates/flowrs-core/src/graph/value.rs, graph/widgets/{list,video,dsp,
|
|
# audio}.rs). Until Kani 0.68 `make verify` ran these as one `cargo kani -p flowrs-core`, with
|
|
# no memory budget; Kani 0.68 verifies harnesses in parallel by default, so each now has a cap
|
|
# and the run as a whole a total.
|
|
#
|
|
# tools/kani-core.sh # every harness
|
|
# tools/kani-core.sh PATTERN... # those whose name contains a pattern
|
|
#
|
|
# Budgets and results as tools/kani-env.sh describes: 16 GB per harness (KANI_MEM_GB), the
|
|
# run under memguard at KANI_TOTAL_GB, KANI_TIMEOUT (default 1800s) per harness, as many at
|
|
# once as fit; results in $KANI_OUT/core.json.
|
|
set -uo pipefail
|
|
cd "$(dirname "$0")/.."
|
|
. tools/kani-env.sh
|
|
kani_preflight || exit 1
|
|
KANI_TIMEOUT=${KANI_TIMEOUT:-1800s}
|
|
TABLE=(
|
|
graph::value::proofs::the_intersection_never_exceeds_the_union:16
|
|
graph::value::proofs::overlap_does_not_depend_on_which_box_is_asked:16
|
|
graph::value::proofs::px_is_in_bounds_for_every_coordinate_inside_the_image:16
|
|
graph::value::proofs::nearest_source_stays_inside_the_source_image:16
|
|
graph::value::proofs::nearest_source_never_runs_backwards:16
|
|
graph::value::proofs::crop_rect_answers_none_or_a_rectangle_that_fits:16
|
|
graph::widgets::list::proofs::resolve_index_never_points_outside_the_list:16
|
|
graph::widgets::list::proofs::slice_range_is_always_a_range_rust_accepts:16
|
|
graph::widgets::video::proofs::the_shared_nearest_source_stays_inside_the_source:16
|
|
graph::widgets::video::proofs::the_shared_nearest_source_never_runs_backwards:16
|
|
graph::widgets::video::proofs::the_shared_nearest_source_never_truncates_a_large_product:16
|
|
graph::widgets::video::proofs::resize_produces_exactly_the_frame_that_was_asked_for:16
|
|
graph::widgets::dsp::proofs::the_bit_reversal_is_a_permutation:16
|
|
graph::widgets::dsp::proofs::every_biquad_the_panel_can_build_is_stable:16
|
|
graph::widgets::dsp::proofs::rbj_terms_are_finite_for_every_cutoff_and_q:16
|
|
graph::widgets::audio::proofs::fft_window_is_always_a_power_of_two_that_fits:16
|
|
graph::widgets::audio::proofs::stft_never_reads_past_the_end_of_its_input:16
|
|
graph::widgets::audio::proofs::stft_refuses_a_frame_longer_than_its_input:16
|
|
graph::widgets::audio::proofs::resample_linear_cannot_panic_for_any_rate_the_panel_allows:16
|
|
graph::widgets::audio::proofs::an_empty_input_resamples_to_an_empty_output:16
|
|
)
|
|
kani_select "$@"
|
|
kani_go core ${SELECTED[@]+"${SELECTED[@]}"} -- cargo kani -p flowrs-core
|