diff --git a/README.md b/README.md index 8c716c8b8ba0639f7317e3b9d6e72328e8483265..dc1a2d1392e5bacf15a3355297dccc6b40e98ca0 100644 --- a/README.md +++ b/README.md @@ -10,10 +10,17 @@ This example showcase the different path termintaiton conditions possible and th This example showcase contract based verification, and the possibilies to extract proofs. +## struct.rs + +This example show the case of partially symbolic structures. + ## vcell_test.rs -Simple test to showcase low-level access. +Simple test to showcase low-level `vcell` access. + +## register_test.rs +Simple test to showcase the use of the `volatile-register` abstraction. ## f401_minimal.rs