diff --git a/klee/src/ll.rs b/klee/src/ll.rs index 7c60f6f969cdf3c8253e1881e4eef7eaf79412d1..d8144103613ebc629feecc868775251ad3488928 100644 --- a/klee/src/ll.rs +++ b/klee/src/ll.rs @@ -4,11 +4,7 @@ use cty::{c_char, c_void}; extern "C" { pub fn abort() -> !; pub fn klee_assume(cond: bool); - pub fn klee_make_symbolic( - ptr: *mut c_void, - size: usize, - name: *const c_char, - ); + pub fn klee_make_symbolic(ptr: *mut c_void, size: usize, name: *const c_char); } #[cfg(not(feature = "klee_mode"))] @@ -20,9 +16,4 @@ pub unsafe fn abort() -> ! { pub unsafe fn klee_assume(_cond: bool) {} #[cfg(not(feature = "klee_mode"))] -pub unsafe fn klee_make_symbolic( - _ptr: *mut c_void, - _size: usize, - _name: *const c_char, -) { -} +pub unsafe fn klee_make_symbolic(_ptr: *mut c_void, _size: usize, _name: *const c_char) {} diff --git a/klee/tasks.txt b/klee/tasks.txt index fb62ad331f6b05c445c05a4cdfee52e0cc01d985..b2f6e50527d23c27db6aa5633a36ddfcbb3ea947 100644 --- a/klee/tasks.txt +++ b/klee/tasks.txt @@ -1,2 +1,2 @@ -// autogenertated file - [] \ No newline at end of file +// autogenerated file +["EXTI3", "EXTI2", "EXTI1"] \ No newline at end of file diff --git a/macros/src/lib.rs b/macros/src/lib.rs index 27829e9876b3948de5bfcbf2c75f084b13ae2584..aad020f5ccd0f205617e9cfe73e2591d22fa0486 100644 --- a/macros/src/lib.rs +++ b/macros/src/lib.rs @@ -200,7 +200,7 @@ fn run(ts: TokenStream) -> Result<TokenStream> { let path = Path::new("klee/tasks.txt"); let mut file = File::create(path).unwrap(); - write!(file, "// autogenertated file \n {:?}", tasks).unwrap(); + write!(file, "// autogenerated file\n{:?}", tasks).unwrap(); } Ok(format!("{}", tokens) .parse() diff --git a/macros/src/trans.rs b/macros/src/trans.rs index 70b553d6fc594e10edb701180c016afb38a0662b..8d0e9e6a98e5ca2fc3d935fd167a3ef0d25e13d7 100644 --- a/macros/src/trans.rs +++ b/macros/src/trans.rs @@ -27,12 +27,7 @@ pub fn app(app: &App, ownerships: &Ownerships) -> Tokens { quote!(#(#root)*) } -fn idle( - app: &App, - ownerships: &Ownerships, - main: &mut Vec<Tokens>, - root: &mut Vec<Tokens>, -) { +fn idle(app: &App, ownerships: &Ownerships, main: &mut Vec<Tokens>, root: &mut Vec<Tokens>) { let krate = krate(); let mut mod_items = vec![]; @@ -519,10 +514,9 @@ fn tasks(app: &App, ownerships: &Ownerships, root: &mut Vec<Tokens>) { for rname in &task.resources { let ceiling = ownerships[rname].ceiling(); let _rname = Ident::new(format!("_{}", rname.as_ref())); - let resource = app.resources.get(rname).expect(&format!( - "BUG: resource {} has no definition", - rname - )); + let resource = app.resources + .get(rname) + .expect(&format!("BUG: resource {} has no definition", rname)); let ty = &resource.ty; let _static = if resource.expr.is_some() {