klee-analysis (no-rt)

Cargo.toml

@@ -8,12 +8,14 @@ version = "0.3.0"
 
 
 [patch.crates-io]
-cortex-m = { path = "../cortex-m" }
-volatile-register = { path = "../volatile-register" }
+volatile-register = { git = "https://gitlab.henriktjader.com/pln/volatile-register.git", branch = "klee-analysis" }
+#volatile-register = { path = "../../klee/volatile-register/" }
+cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" }
+#cortex-m = { path = "../../cortex-m" }
 
 [dependencies]
 bare-metal = "0.2.4"
-vcell = "0.1.0"
+vcell = "0.2.0"
 
 [dependencies.cortex-m]
 version = "0.6.0"
@@ -22,11 +24,11 @@ version = "0.6.0"
 optional = true
 version = "0.6.5"
 
-[dependencies.klee]
-optional = true
-path = "../."
-#version = "0.6.5"
+#[dependencies.klee]
+#optional = true
+#path = "../."
+##version = "0.6.5"
 
 [features]
 rt = ["cortex-m-rt/device"]
-klee-analysis = ["klee", "cortex-m/klee-analysis"]
+klee-analysis = ["cortex-m/klee-analysis", "vcell/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();