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

fixed cstr_core dependency

parent 3d0ccd80
No related branches found
No related tags found
No related merge requests found
{
"cSpell.ignoreWords": [
"concat",
"core",
"cstr"
]
}
\ No newline at end of file
[package]
name = "klee-sys"
version = "0.1.0"
version = "0.2.0"
authors = ["pln <Per Lindgren>"]
edition = "2018"
[dependencies]
cstr_core = "0.1.2"
[dependencies.cstr_core]
version = "0.2.2"
default-features = false
[features]
inline-asm = []
......
......@@ -16,7 +16,7 @@ Variables (or rather `memory objects`) can be made symbolic, through the KLEE C
pub fn klee_make_symbolic(
ptr: *mut core::ffi::c_void, // pointer to the data
size: usize, // size (in bytes)
name: *const cstr_core::c_char, // pointer to zero-terminted C string
name: *const cstr_core::c_char, // pointer to zero-terminated C string
);
}
```
......@@ -24,13 +24,19 @@ pub fn klee_make_symbolic(
The internal Rust abstraction, calls into the FFI binding.
``` Rust
fn klee_make_symbolic<T>(
t: &mut T, // reference to generic type
name: &'static CStr // reference to static CStr
) {...}
#[inline(always)]
pub fn klee_make_symbolic<T>(t: &mut T, name: &'static CStr) {
unsafe {
crate::ll::klee_make_symbolic(
t as *mut T as *mut c_void,
core::mem::size_of::<T>(),
name.as_ptr() as *const c_char,
)
}
}
```
However dealing with CStr is cumbersome in Rust user code so we provide a macro, `klee_make_symbolic!(&mut T, &str)`, that zero-termintes the `&str` and cast it to the appropriate type.
However dealing with CStr is cumbersome in Rust user code so we provide a macro, `klee_make_symbolic!(&mut T, &str)`, that zero-terminates the `&str` and cast it to the appropriate type.
Example usage:
......
......@@ -14,7 +14,7 @@
//! TODO: better documentation (as always)
#![no_std]
#![cfg_attr(feature = "inline-asm", feature(asm))]
#![cfg_attr(feature = "inline-asm", feature(llvm_asm))]
// re-exports for klee-analysis
#[cfg(feature = "klee-analysis")]
......@@ -22,13 +22,13 @@ mod lib_klee_analysis;
#[cfg(feature = "klee-analysis")]
pub mod ll; // low level bindings
#[cfg(feature = "klee-analysis")]
pub use lib_klee_analysis::*; // functions and macros
pub use lib_klee_analysis::*; // re-export functions and macros
// re-exports for klee-replay
#[cfg(feature = "klee-replay")]
mod lib_klee_replay;
#[cfg(feature = "klee-replay")]
pub use lib_klee_replay::*; // functions and macros
pub use lib_klee_replay::*; // re-export functions and macros
#[cfg(all(not(feature = "klee-analysis"), not(feature = "klee-replay")))]
compile_error!("feature required, either `klee-analysis` or `klee-replay`");
use core::ffi::c_void;
use cstr_core::c_char;
#[doc(hidden)]
pub use cstr_core::CStr;
#[cfg(not(feature = "inline-asm"))]
compile_error!("klee-replay requires feature `inline-asm`");
#[inline(always)]
fn klee_abort() -> ! {
panic!();
}
/// suppress assumption
#[inline(always)]
pub fn klee_assume(_cond: bool) {}
......@@ -20,7 +9,7 @@ pub fn klee_assume(_cond: bool) {}
pub fn klee_make_symbolic<T>(t: &mut T) {
// force LLVM to consider data to be mutated
unsafe {
asm!("bkpt #0" : /* output */: /* input */ "r"(t): /* clobber */ : "volatile")
llvm_asm!("bkpt #0" : /* output */: /* input */ "r"(t): /* clobber */ : "volatile")
}
}
......
......@@ -5,6 +5,6 @@ extern "C" {
pub fn klee_make_symbolic(
ptr: *mut core::ffi::c_void, // pointer to the data
size: usize, // size (in bytes)
name: *const cstr_core::c_char, // pointer to zero-terminted C string
name: *const cstr_core::c_char, // pointer to zero-terminated C string
);
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment