Skip to content
Snippets Groups Projects
Commit be22f4a1 authored by Per Lindgren's avatar Per Lindgren
Browse files

examples

parent 82e9a08f
Branches
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Cargo.lock deleted 100644 → 0
+ 0
− 326
View file @ 82e9a08f
# This file is automatically @generated by Cargo.
# It is not intended for manual editing.
[[package]]
name = "aligned"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "as-slice"
version = "0.1.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"generic-array 0.12.3 (registry+https://github.com/rust-lang/crates.io-index)",
"generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)",
"stable_deref_trait 1.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "autocfg"
version = "0.1.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "bare-metal"
version = "0.2.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"rustc_version 0.2.3 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "byteorder"
version = "1.3.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "cortex-m"
version = "0.6.1"
dependencies = [
"aligned 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
"bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
"klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
"volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cortex-m-rt"
version = "0.6.11"
dependencies = [
"cortex-m 0.6.1",
"cortex-m-rt-macros 0.1.7",
"klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
"r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cortex-m-rt-macros"
version = "0.1.7"
dependencies = [
"proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
"quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
"syn 1.0.12 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cortex-m-rtfm"
version = "0.5.1"
dependencies = [
"cortex-m 0.6.1",
"cortex-m-rt 0.6.11",
"cortex-m-rtfm-macros 0.5.0",
"heapless 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)",
"rtfm-core 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cortex-m-rtfm-macros"
version = "0.5.0"
dependencies = [
"proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
"quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
"rtfm-syntax 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
"syn 1.0.12 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cortex-m-semihosting"
version = "0.3.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"cortex-m 0.6.1",
]
[[package]]
name = "cstr_core"
version = "0.1.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)",
"memchr 2.2.1 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cty"
version = "0.1.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "generic-array"
version = "0.12.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "generic-array"
version = "0.13.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "hash32"
version = "0.1.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"byteorder 1.3.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "heapless"
version = "0.5.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
"generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)",
"hash32 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "indexmap"
version = "1.3.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"autocfg 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "klee-examples"
version = "0.1.0"
dependencies = [
"cortex-m 0.6.1",
"cortex-m-rt 0.6.11",
"cortex-m-rtfm 0.5.1",
"cortex-m-semihosting 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)",
"klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
"lm3s6965 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)",
"panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
"panic-klee 0.1.0 (git+https://gitlab.henriktjader.com/pln/panic-klee.git)",
"vcell 0.1.2",
"volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "klee-sys"
version = "0.1.0"
source = "git+https://gitlab.henriktjader.com/pln/klee-sys.git#c8275a34cffb895984d6bdea80e9c6ff9079f769"
dependencies = [
"cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "lm3s6965"
version = "0.1.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
"cortex-m-rt 0.6.11",
]
[[package]]
name = "memchr"
version = "2.2.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "panic-halt"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "panic-klee"
version = "0.1.0"
source = "git+https://gitlab.henriktjader.com/pln/panic-klee.git#3b0c897f49d7fff017424364e280bcb9dbaffa5d"
[[package]]
name = "proc-macro2"
version = "1.0.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "quote"
version = "1.0.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "r0"
version = "0.2.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "rtfm-core"
version = "0.3.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "rtfm-syntax"
version = "0.4.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"indexmap 1.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
"proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
"syn 1.0.12 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "rustc_version"
version = "0.2.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "semver"
version = "0.9.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "semver-parser"
version = "0.7.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "stable_deref_trait"
version = "1.1.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "syn"
version = "1.0.12"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)",
"quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
"unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "typenum"
version = "1.11.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "unicode-xid"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "vcell"
version = "0.1.2"
dependencies = [
"klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
]
[[package]]
name = "volatile-register"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"vcell 0.1.2",
]
[metadata]
"checksum aligned 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "d39da9b88ae1a81c03c9c082b8db83f1d0e93914126041962af61034ab44c4a5"
"checksum as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "be6b7e95ac49d753f19cab5a825dea99a1149a04e4e3230b33ae16e120954c04"
"checksum autocfg 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)" = "1d49d90015b3c36167a20fe2810c5cd875ad504b39cff3d4eae7977e6b7c1cb2"
"checksum bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)" = "5deb64efa5bd81e31fcd1938615a6d98c82eafcbcd787162b6f63b91d6bac5b3"
"checksum byteorder 1.3.2 (registry+https://github.com/rust-lang/crates.io-index)" = "a7c3dd8985a7111efc5c80b44e23ecdd8c007de8ade3b96595387e812b957cf5"
"checksum cortex-m-semihosting 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)" = "113ef0ecffee2b62b58f9380f4469099b30e9f9cbee2804771b4203ba1762cfa"
"checksum cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6ebe7158ee57e848621d24d0ed87910edb97639cb94ad9977edf440e31226035"
"checksum cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "c4e1d41c471573612df00397113557693b5bf5909666a8acb253930612b93312"
"checksum generic-array 0.12.3 (registry+https://github.com/rust-lang/crates.io-index)" = "c68f0274ae0e023facc3c97b2e00f076be70e254bc851d972503b328db79b2ec"
"checksum generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)" = "0ed1e761351b56f54eb9dcd0cfaca9fd0daecf93918e1cfc01c8a3d26ee7adcd"
"checksum hash32 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "d4041af86e63ac4298ce40e5cca669066e75b6f1aa3390fe2561ffa5e1d9f4cc"
"checksum heapless 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)" = "f339aa7d51777fc0af6aa7cbeb277dfc6e6c029cbdeda48d0fbb92c2337f0e69"
"checksum indexmap 1.3.0 (registry+https://github.com/rust-lang/crates.io-index)" = "712d7b3ea5827fcb9d4fda14bf4da5f136f0db2ae9c8f4bd4e2d1c6fde4e6db2"
"checksum klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)" = "<none>"
"checksum lm3s6965 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)" = "8698042a7495160eac9f7298a32cd1ddbb6ad2780f766f5a99b4f0a6b915e0ad"
"checksum memchr 2.2.1 (registry+https://github.com/rust-lang/crates.io-index)" = "88579771288728879b57485cc7d6b07d648c9f0141eb955f8ab7f9d45394468e"
"checksum panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "de96540e0ebde571dc55c73d60ef407c653844e6f9a1e2fdbd40c07b9252d812"
"checksum panic-klee 0.1.0 (git+https://gitlab.henriktjader.com/pln/panic-klee.git)" = "<none>"
"checksum proc-macro2 1.0.7 (registry+https://github.com/rust-lang/crates.io-index)" = "0319972dcae462681daf4da1adeeaa066e3ebd29c69be96c6abb1259d2ee2bcc"
"checksum quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)" = "053a8c8bcc71fcce321828dc897a98ab9760bef03a4fc36693c231e5b3216cfe"
"checksum r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)" = "e2a38df5b15c8d5c7e8654189744d8e396bddc18ad48041a500ce52d6948941f"
"checksum rtfm-core 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)" = "9ec893edb2aa5b70320b94896ffea22a7ebb1cf3f942bb67cd5b60a865a63493"
"checksum rtfm-syntax 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)" = "4455e23c34df3d66454e7e218a4d76a7f83321d04a806be614463341cec4116e"
"checksum rustc_version 0.2.3 (registry+https://github.com/rust-lang/crates.io-index)" = "138e3e0acb6c9fb258b19b67cb8abd63c00679d2851805ea151465464fe9030a"
"checksum semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)" = "1d7eb9ef2c18661902cc47e535f9bc51b78acd254da71d375c2f6720d9a40403"
"checksum semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)" = "388a1df253eca08550bef6c72392cfe7c30914bf41df5269b68cbd6ff8f570a3"
"checksum stable_deref_trait 1.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "dba1a27d3efae4351c8051072d619e3ade2820635c3958d826bfea39d59b54c8"
"checksum syn 1.0.12 (registry+https://github.com/rust-lang/crates.io-index)" = "ddc157159e2a7df58cd67b1cace10b8ed256a404fb0070593f137d8ba6bef4de"
"checksum typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6d2783fe2d6b8c1101136184eb41be8b1ad379e4657050b8aaff0c79ee7575f9"
"checksum unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "826e7639553986605ec5979c7dd957c7895e93eabed50ab2ffa7f6128a75097c"
"checksum volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "0d67cb4616d99b940db1d6bd28844ff97108b498a6ca850e5b6191a532063286"
Cargo.toml
+ 4
− 4
View file @ be22f4a1
...@@ -37,14 +37,14 @@ optional = true ...@@ -37,14 +37,14 @@ optional = true
# #features = ["inline-asm", "klee-analysis"] # #features = ["inline-asm", "klee-analysis"]
[patch.crates-io] [patch.crates-io]
#vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" } vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" }
vcell = { path = "../vcell" } #vcell = { path = "../vcell" }
#volatile-register = { git = "https://github.com/perlindgren/volatile-register.git", branch = "trustit" } #volatile-register = { git = "https://github.com/perlindgren/volatile-register.git", branch = "trustit" }
#volatile-register = { path = "../volatile-register" } #volatile-register = { path = "../volatile-register" }
#cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" } cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" }
cortex-m = { path = "../cortex-m" } #cortex-m = { path = "../cortex-m" }
#cortex-m-rt = { git = "https://github.com/perlindgren/cortex-m-rt.git", branch = "trustit" } #cortex-m-rt = { git = "https://github.com/perlindgren/cortex-m-rt.git", branch = "trustit" }
cortex-m-rt = { path = "../cortex-m-rt" } cortex-m-rt = { path = "../cortex-m-rt" }
......
examples/expand.rs deleted 100644 → 0
+ 0
− 51
View file @ 82e9a08f
#![feature(prelude_import)]
#![no_std]
#![no_main]
#[prelude_import]
use core::prelude::v1::*;
#[macro_use]
extern crate core;
#[macro_use]
extern crate compiler_builtins;
use cortex_m_rt::{entry, exception, pre_init};
use panic_klee as _;
use klee_sys::{klee_abort, klee_make_symbolic};
use cortex_m::peripheral::Peripherals;
static mut S: u32 = 100;
#[doc(hidden)]
#[export_name = "main_klee"]
pub unsafe extern "C" fn __cortex_m_rt_main_trampoline() {
__cortex_m_rt_main()
}
unsafe fn __cortex_m_rt_main() -> ! {
let peripherals = Peripherals::take().unwrap();
let mut dwt = peripherals.DWT;
let a = dwt.cyccnt.read();
if a == unsafe { S } {
::core::panicking::panic("explicit panic", ::core::intrinsics::caller_location());
}
unsafe { ::klee_sys::ll::abort() };
}
#[export_name = "__pre_init"]
pub unsafe fn pre_init() {
let mut a = 0;
::klee_sys::klee_make_symbolic(unsafe { &mut a }, unsafe {
::klee_sys::CStr::from_bytes_with_nul_unchecked("a\u{0}".as_bytes())
});
if a == 100 {
unsafe { ::klee_sys::ll::abort() };
}
}
#[doc(hidden)]
#[export_name = "DefaultHandler"]
fn __cortex_m_rt_DefaultHandler(_irqn: i16) -> ! {
if _irqn > 255 {
unsafe { ::klee_sys::ll::abort() };
}
unsafe { ::klee_sys::ll::abort() };
}
examples/klee_cortex_m_rt_test3.rs
+ 77
− 20
View file @ be22f4a1
#![no_std] #![no_std]
#![no_main] #![no_main]
use cortex_m_rt::{entry, exception, pre_init}; use cortex_m_rt::{entry, exception, pre_init, ExceptionFrame};
use panic_klee as _; use panic_klee as _;
use klee_sys::{klee_abort, klee_make_symbolic}; use klee_sys::{klee_abort, klee_make_symbolic};
...@@ -12,33 +12,90 @@ static mut S: u32 = 100; ...@@ -12,33 +12,90 @@ static mut S: u32 = 100;
#[entry] #[entry]
unsafe fn main() -> ! { unsafe fn main() -> ! {
let peripherals = Peripherals::take().unwrap(); // let peripherals = Peripherals::take().unwrap();
let mut dwt = peripherals.DWT; // let mut dwt = peripherals.DWT;
let a = dwt.cyccnt.read(); // let a = dwt.cyccnt.read();
if a == unsafe { S } { // if a == unsafe { S } {
panic!(); // panic!();
} // }
klee_abort!(); klee_abort!();
} }
#[pre_init] #[pre_init]
unsafe fn pre_init() { unsafe fn pre_init() {
let mut a = 0; // let mut a = 0;
klee_make_symbolic!(&mut a, "a"); // klee_make_symbolic!(&mut a, "a");
if a == 100 { // if a == 100 {
klee_abort!(); // klee_abort!();
} // }
} }
#[exception] #[exception]
fn DefaultHandler(irqn: i16) -> ! { fn DefaultHandler(irqn: i16) -> ! {
static mut X: i16 = 0; // static mut X: i16 = 0;
if irqn > 255 { // if irqn > 255 {
unsafe { core::ptr::write_volatile(&mut X, irqn) }; // unsafe { core::ptr::write_volatile(&mut X, irqn) };
klee_abort!(); // klee_abort!();
} else { // } else {
unsafe { core::ptr::write_volatile(&mut X, 0) }; // unsafe { core::ptr::write_volatile(&mut X, 0) };
klee_abort!(); // klee_abort!();
} // }
klee_abort!();
}
#[exception]
fn NonMaskableInt() -> ! {
klee_abort!();
}
#[exception]
fn HardFault(eh: &ExceptionFrame) -> ! {
// match eh.xpsr {
// 0 => klee_abort!(),
// 1 => klee_abort!(),
// 2 => klee_abort!(),
// _ => (),
// }
klee_abort!();
}
#[exception]
fn MemoryManagement() {
// klee_abort!();
}
#[exception]
fn BusFault() {
//klee_abort!();
}
#[exception]
fn UsageFault() {
//klee_abort!();
}
#[exception]
fn SecureFault() {
//klee_abort!();
}
#[exception]
fn SVCall() {
//klee_abort!();
}
#[exception]
fn DebugMonitor() {
//klee_abort!();
}
#[exception]
fn PendSV() {
//klee_abort!();
}
#[exception]
fn SysTick() {
//klee_abort!();
} }
examples/klee_only_test.rs → examples/paths.rs
+ 0
− 0
View file @ be22f4a1
File moved
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment