verus
forked from verus-lang/verus
Star 0
Fork 0
Watch
verus source rust_verify_test tests
3 folders · 147 files
cargo-tests
common
vc_shapes
adts_generics.rs
adts_opaque.rs
adts.rs
arrays.rs
assert_bitvector_by.rs
assert_by_compute.rs
assert_forall_by.rs
assoc_type_impls.rs
async_functions.rs
atomic_lib.rs
atomics.rs
basic.rs
bitvector.rs
boundary_suggestions.rs
broadcast_forall.rs
btree.rs
byte_char.rs
byte_string.rs
calc.rs
cargo.rs
cell_lib.rs
char.rs
choose.rs
closures.rs
compile.rs
consts.rs
contrib.rs
control_flow.rs
core_special_setup.rs
cow.rs
dafny_axioms.rs
default_trait.rs
eq_cmp.rs
erase.rs
examples.rs
exec_closures.rs
exec_spec_unverified.rs
exec_spec_verified.rs
exec_termination.rs
expand_errors.rs
expr_stmts.rs
ext_equal.rs
extern_functions.rs
external_fn_specification.rs
external_traits.rs
external_type_specification.rs
float.rs
fndef_types.rs
functions.rs
generics.rs
harness.rs
hash.rs
impl.rs
index.rs
inline.rs
integer_ring.rs
integers.rs
iterators.rs
layout.rs
let_else.rs
lifetime.rs
literals.rs
logatom.rs
loop_isolation_boundary.rs
loops_havoc.rs
loops_no_spinoff.rs
loops.rs
maps.rs
marker_traits.rs
match.rs
modes.rs
modules.rs
multiset.rs
mut_refs_closures.rs
mut_refs_libs.rs
mut_refs_loops.rs
mut_refs_modes.rs
mut_refs_old.rs
mut_refs_patterns.rs
mut_refs_slices_arrays.rs
mut_refs_temporaries.rs
mut_refs_time_travel.rs
mut_refs_unions.rs
mut_refs.rs
mutable_params.rs
nested_items.rs
never_type.rs
no_cheating.rs
nonlinear.rs
observer.rs
opaque_reveal.rs
opaque_types.rs
open_invariant.rs
operators.rs
option.rs
output_json.rs
overflow.rs
partial_eq.rs
pattern_arrays.rs
pattern_slices.rs
proof_closures.rs
proof_in_spec.rs
proph.rs
prophecy.rs
quantifiers.rs
raw_ptrs.rs
real.rs
recommends.rs
recursion.rs
recursive_types.rs
refs.rs
regression.rs
results.rs
return.rs
returns_postcondition.rs
safe_api.rs
scope.rs
seqs.rs
sets.rs
shadowed_names.rs
shr_ref_struct_wrap.rs
size_of.rs
slices.rs
spec_derive.rs
state_machines.rs
std.rs
strings.rs
struct_with_invariants.rs
structural.rs
summer_school.rs
syntax_attr.rs
traits_dyn.rs
traits_extend_ensures.rs
traits_modules_pub_crate.rs
traits_modules.rs
traits.rs
triggers.rs
ui.rs
unions.rs
unsafe.rs
unwind.rs
user_defined_type_invariants.rs
utf8.rs
vec.rs
verifier_assume_allow.rs
when_used_as_spec.rs
z3_restart.rs