KLEE

Cargo.toml

@@ -7,14 +7,26 @@ name = "stm32f413"
 version = "0.3.0"
 
 
+[patch.crates-io]
+cortex-m = { path = "../cortex-m" }
+volatile-register = { path = "../volatile-register" }
+
 [dependencies]
-cortex-m = "0.5.8"
 bare-metal = "0.2.4"
 vcell = "0.1.0"
 
+[dependencies.cortex-m]
+version = "0.6.0"
+
 [dependencies.cortex-m-rt]
 optional = true
 version = "0.6.5"
 
+[dependencies.klee]
+optional = true
+path = "../."
+#version = "0.6.5"
+
 [features]
-rt = ["cortex-m-rt/device"]
\ No newline at end of file
+rt = ["cortex-m-rt/device"]
+klee-analysis = ["klee", "cortex-m/klee-analysis"]
\ No newline at end of file

src/klee_statics/mod.rs

+use core::mem::MaybeUninit;
+pub static mut ADC1: MaybeUninit<::adc1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut CRC: MaybeUninit<::crc::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut DBG: MaybeUninit<::dbg::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut EXTI: MaybeUninit<::exti::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut FLASH: MaybeUninit<::flash::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut IWDG: MaybeUninit<::iwdg::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut PWR: MaybeUninit<::pwr::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut RCC: MaybeUninit<::rcc::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut RTC: MaybeUninit<::rtc::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut SDIO: MaybeUninit<::sdio::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut SYSCFG: MaybeUninit<::syscfg::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM1: MaybeUninit<::tim1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM8: MaybeUninit<::tim1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM10: MaybeUninit<::tim10::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM11: MaybeUninit<::tim11::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM2: MaybeUninit<::tim2::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM3: MaybeUninit<::tim3::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM4: MaybeUninit<::tim3::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM5: MaybeUninit<::tim5::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM9: MaybeUninit<::tim9::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut USART1: MaybeUninit<::usart1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut USART2: MaybeUninit<::usart1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut USART6: MaybeUninit<::usart1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut USART3: MaybeUninit<::usart1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut UART4: MaybeUninit<::usart1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut UART5: MaybeUninit<::usart1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut UART7: MaybeUninit<::usart1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut UART8: MaybeUninit<::usart1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut UART9: MaybeUninit<::usart1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut UART10: MaybeUninit<::usart1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut WWDG: MaybeUninit<::wwdg::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut DMA2: MaybeUninit<::dma2::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut DMA1: MaybeUninit<::dma2::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut GPIOH: MaybeUninit<::gpioh::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut GPIOE: MaybeUninit<::gpioh::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut GPIOD: MaybeUninit<::gpioh::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut GPIOC: MaybeUninit<::gpioh::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut GPIOF: MaybeUninit<::gpioh::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut GPIOG: MaybeUninit<::gpioh::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut GPIOB: MaybeUninit<::gpiob::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut GPIOA: MaybeUninit<::gpioa::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut I2C3: MaybeUninit<::i2c3::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut I2C2: MaybeUninit<::i2c3::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut I2C1: MaybeUninit<::i2c3::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut I2S2EXT: MaybeUninit<::i2s2ext::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut I2S3EXT: MaybeUninit<::i2s2ext::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut SPI1: MaybeUninit<::i2s2ext::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut SPI2: MaybeUninit<::i2s2ext::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut SPI3: MaybeUninit<::i2s2ext::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut SPI4: MaybeUninit<::i2s2ext::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut SPI5: MaybeUninit<::i2s2ext::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut SPI6: MaybeUninit<::i2s2ext::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut DFSDM1: MaybeUninit<::dfsdm1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut DFSDM2: MaybeUninit<::dfsdm1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM6: MaybeUninit<::tim6::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM7: MaybeUninit<::tim6::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM12: MaybeUninit<::tim12::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM13: MaybeUninit<::tim13::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut TIM14: MaybeUninit<::tim13::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut RNG: MaybeUninit<::rng::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut CAN1: MaybeUninit<::can1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut CAN2: MaybeUninit<::can1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut CAN3: MaybeUninit<::can1::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut FMPI2C: MaybeUninit<::fmpi2c::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut FSMC: MaybeUninit<::fsmc::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut OTG_FS_GLOBAL: MaybeUninit<::otg_fs_global::RegisterBlock> =
+    MaybeUninit::uninitialized();
+pub static mut OTG_FS_HOST: MaybeUninit<::otg_fs_host::RegisterBlock> =
+    MaybeUninit::uninitialized();
+pub static mut OTG_FS_DEVICE: MaybeUninit<::otg_fs_device::RegisterBlock> =
+    MaybeUninit::uninitialized();
+pub static mut OTG_FS_PWRCLK: MaybeUninit<::otg_fs_pwrclk::RegisterBlock> =
+    MaybeUninit::uninitialized();
+pub static mut QUADSPI: MaybeUninit<::quadspi::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut LPTIM: MaybeUninit<::lptim::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut DAC: MaybeUninit<::dac::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut SAI: MaybeUninit<::sai::RegisterBlock> = MaybeUninit::uninitialized();
+pub static mut AES: MaybeUninit<::aes::RegisterBlock> = MaybeUninit::uninitialized();