From 21cd29667da111c47ac41a53094211ac41bb3d5a Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Mon, 26 Feb 2018 22:47:34 +0100
Subject: [PATCH] inlining
---
klee/src/ll.rs | 3 +++
1 file changed, 3 insertions(+)
diff --git a/klee/src/ll.rs b/klee/src/ll.rs
index d814410..01d25d5 100644
--- a/klee/src/ll.rs
+++ b/klee/src/ll.rs
@@ -8,12 +8,15 @@ extern "C" {
}
#[cfg(not(feature = "klee_mode"))]
+#[inline(always)]
pub unsafe fn abort() -> ! {
loop {}
}
#[cfg(not(feature = "klee_mode"))]
+#[inline(always)]
pub unsafe fn klee_assume(_cond: bool) {}
#[cfg(not(feature = "klee_mode"))]
+#[inline(always)]
pub unsafe fn klee_make_symbolic(_ptr: *mut c_void, _size: usize, _name: *const c_char) {}
--
GitLab