@@ -42,6 +42,11 @@ See section `Cargo.toml` for detaled information on features introduced.
...
@@ -42,6 +42,11 @@ See section `Cargo.toml` for detaled information on features introduced.
Simple test to showcase the use of the `volatile-register` abstraction. `volitile-register` builds on `vcell` and is used by both hand written and machine generated hardware accesses in the Rust embedded ecosystem.
Simple test to showcase the use of the `volatile-register` abstraction. `volitile-register` builds on `vcell` and is used by both hand written and machine generated hardware accesses in the Rust embedded ecosystem.
This example also showcase the `gdb` replay functionality.
TODO:perhaps better to put the `gdb` replay in the Basic test examples,
as replay is not tied to `volatile-register`.
-`cortex-m-test1.rs`
-`cortex-m-test1.rs`
Simple test to showcase the [cortex-m](https://github.com/perlindgren/vcell) abstraction of ARM-core peripherals ARM thumb assembly instructions and ARM thumb CPU registers. `cortex-m` uses the `volatile-register` abstraction for ARM-core peripherals. The `klee-analysis` feature replaces read operations on CPU registers by symbolic data and suppresses write operations as for analysis we are not interested in the side effects.
Simple test to showcase the [cortex-m](https://github.com/perlindgren/vcell) abstraction of ARM-core peripherals ARM thumb assembly instructions and ARM thumb CPU registers. `cortex-m` uses the `volatile-register` abstraction for ARM-core peripherals. The `klee-analysis` feature replaces read operations on CPU registers by symbolic data and suppresses write operations as for analysis we are not interested in the side effects.
