Skip to content

Latest commit

 

History

History

example

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
guide
guide
 
 
integer_ring
integer_ring
 
 
pcm
pcm
 
 
scache
scache
 
 
state_machines
state_machines
 
 
std_test
std_test
 
 
summer_school
summer_school
 
 
README.md
README.md
 
 
adts.rs
adts.rs
 
 
adts_eq.rs
adts_eq.rs
 
 
assert_by_compute.rs
assert_by_compute.rs
 
 
assertions.rs
assertions.rs
 
 
assorted_demo.rs
assorted_demo.rs
 
 
atomics.rs
atomics.rs
 
 
basic_failure.rs
basic_failure.rs
 
 
basic_lock1.rs
basic_lock1.rs
 
 
basic_lock2.rs
basic_lock2.rs
 
 
bitmap.rs
bitmap.rs
 
 
bitvector_basic.rs
bitvector_basic.rs
 
 
bitvector_equivalence.rs
bitvector_equivalence.rs
 
 
bitvector_garbage_collection.rs
bitvector_garbage_collection.rs
 
 
calc.rs
calc.rs
 
 
cells.rs
cells.rs
 
 
datatypes.rs
datatypes.rs
 
 
debug.rs
debug.rs
 
 
debug_expand.rs
debug_expand.rs
 
 
doubly_linked.rs
doubly_linked.rs
 
 
doubly_linked_xor.rs
doubly_linked_xor.rs
 
 
even_cell.rs
even_cell.rs
 
 
extensionality.rs
extensionality.rs
 
 
external.rs
external.rs
 
 
fun_ext.rs
fun_ext.rs
 
 
generics.rs
generics.rs
 
 
imo_1988_6.rs
imo_1988_6.rs
 
 
impl_basic.rs
impl_basic.rs
 
 
integers.rs
integers.rs
 
 
invariants.rs
invariants.rs
 
 
modules.rs
modules.rs
 
 
multiset.rs
multiset.rs
 
 
nevd_script.rs
nevd_script.rs
 
 
playground.rs
playground.rs
 
 
power_of_2.rs
power_of_2.rs
 
 
prelude.rs
prelude.rs
 
 
proposal-rw2022.rs
proposal-rw2022.rs
 
 
quantifiers.rs
quantifiers.rs
 
 
recommends.rs
recommends.rs
 
 
recursion.rs
recursion.rs
 
 
recursive_types.rs
recursive_types.rs
 
 
rfmig_script.rs
rfmig_script.rs
 
 
rw2022_script.rs
rw2022_script.rs
 
 
rwlock_vstd.rs
rwlock_vstd.rs
 
 
set_from_vec.rs
set_from_vec.rs
 
 
statements.rs
statements.rs
 
 
statics.rs
statics.rs
 
 
structural.rs
structural.rs
 
 
syntax.rs
syntax.rs
 
 
syntax_attr.rs
syntax_attr.rs
 
 
test.rs
test.rs
 
 
test_expand_errors.rs
test_expand_errors.rs
 
 
thread.rs
thread.rs
 
 
trait_for_fn.rs
trait_for_fn.rs
 
 
traits.rs
traits.rs
 
 
trigger_loops.rs
trigger_loops.rs
 
 
vectors.rs
vectors.rs
 
 
verified_vec.rs
verified_vec.rs
 
 

README.md

This directory contains various example files of programs to verify.

There is a test in rust_verify/tests/examples.rs that attempts to run the verify on all .rs files in example, unless tagged as "ignore". The test will check the verification outcome based on the mode specified in the tag. The tag is specified by adding the following as the first line:

// rust_verify/tests/example.rs <mode> [---] [optional comment]

where <mode> is one of:

  • expect-success (default) expects the verification to succeed, reporting zero verification failures,
  • expect-errors expects the compiler to fail, without reporting verification successes and failures,
  • expect-failures expects the compiler and verifier to run successfully, but reporting one or more verification failures,
  • ignore causes the test to skip this file.

These checks are implemented with a regular expression that matches the expected verifier output.

If no tag is specified on the first line, expect-success is assumed.

The "optional comment" field is required if ignore is used.

It is recommended to include the optional comment if expect-failures is used.