Skip to content
Snippets Groups Projects
Commit 519a1dc7 authored by Nils Fitinghoff's avatar Nils Fitinghoff
Browse files

improve abort identification in KLEE output

KLEE reports the line that called `ll::abort()`. The previous
solution called a safe `abort()` which in turn called `ll::abort`. This
meant that every abort was reported as originating in this library.

This replaces the safe `abort()` function with a macro `kabort!()`. The
behavior differs in that `kabort!()` expands to nothing when not in KLEE
mode, while `abort()` expanded to a panic.

The macro causes the call to `ll::abort()` to happen directly from user
code from KLEE's point of view.
parent d6ddde24
No related branches found
No related tags found
No related merge requests found
...@@ -22,6 +22,6 @@ fn main() { ...@@ -22,6 +22,6 @@ fn main() {
} }
if rw.read() == 0 { if rw.read() == 0 {
klee::abort(); // we directly call the intrinsic abort klee::kabort!(); // we directly call the intrinsic abort
} }
} }
...@@ -18,7 +18,7 @@ fn main() { ...@@ -18,7 +18,7 @@ fn main() {
} }
if dwt.ctrl.read() == 0 { if dwt.ctrl.read() == 0 {
if dwt.ctrl.read() == 0 { if dwt.ctrl.read() == 0 {
klee::abort(); klee::kabort!();
}; };
}; };
} }
...@@ -51,7 +51,7 @@ fn main() { ...@@ -51,7 +51,7 @@ fn main() {
if rw.read() == 0 { if rw.read() == 0 {
if rw.read() == 0 { if rw.read() == 0 {
klee::abort(); klee::kabort!();
} }
} }
} }
...@@ -16,15 +16,13 @@ use core::ffi::c_void; ...@@ -16,15 +16,13 @@ use core::ffi::c_void;
#[doc(hidden)] #[doc(hidden)]
pub use cstr_core::CStr; pub use cstr_core::CStr;
/// Aborts the path in KLEE mode, does nothing otherwise
#[macro_export]
macro_rules! kabort {
() => {
#[cfg(feature = "klee-analysis")] #[cfg(feature = "klee-analysis")]
#[inline(always)] unsafe { $crate::ll::abort() };
pub fn abort() -> ! { };
unsafe { ll::abort() }
}
#[cfg(not(feature = "klee-analysis"))]
pub fn abort() -> ! {
panic!(); // leads to the defined panic handler
} }
#[cfg(feature = "klee-analysis")] #[cfg(feature = "klee-analysis")]
...@@ -60,18 +58,16 @@ macro_rules! ksymbol { ...@@ -60,18 +58,16 @@ macro_rules! ksymbol {
}; };
} }
#[cfg(feature = "klee-analysis")] /// If in KLEE mode, the assertion is made.
/// Otherwise, this is does nothing.
#[macro_export] #[macro_export]
macro_rules! kassert { macro_rules! kassert {
($e:expr) => { ($e:expr) => {
#[cfg(feature = "klee-analysis")]
{
if !$e { if !$e {
$crate::abort(); $crate::kabort!();
} }
};
} }
};
#[cfg(not(feature = "klee-analysis"))]
#[macro_export]
macro_rules! kassert {
($e:expr) => {};
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment