From 27797ebfbf8f374670eede7d3c256ce6d3c3e946 Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Thu, 1 Mar 2018 17:59:26 +0100
Subject: [PATCH] simply chaos
---
klee/src/lib.rs | 39 +++++++++++----------------------------
1 file changed, 11 insertions(+), 28 deletions(-)
diff --git a/klee/src/lib.rs b/klee/src/lib.rs
index 5204421..31b22b5 100644
--- a/klee/src/lib.rs
+++ b/klee/src/lib.rs
@@ -7,7 +7,7 @@ extern crate cstr_core;
extern crate cty;
// mod lang_items;
-pub mod ll;
+mod ll;
use core::mem;
@@ -42,7 +42,7 @@ pub fn k_mk_symbol<T>(t: &mut T, name: &CStr) {
}
}
-#[inline(always)]
+#[inline(never)]
pub fn k_abort() -> ! {
unsafe {
ll::abort();
@@ -50,7 +50,7 @@ pub fn k_abort() -> ! {
}
/// assume a condition involving symbolic variables
-#[inline(always)]
+#[inline(never)]
pub fn k_assume(cond: bool) {
unsafe {
ll::klee_assume(cond);
@@ -58,12 +58,10 @@ pub fn k_assume(cond: bool) {
}
/// assert a condition involving symbolic variables
-#[inline(always)]
+#[inline(never)]
pub fn k_assert(e: bool) {
if !e {
- unsafe {
- ll::abort();
- }
+ k_abort();
}
}
@@ -72,27 +70,12 @@ pub fn k_assert(e: bool) {
macro_rules! k_symbol {
($id:expr, $name:expr) => {
{
- #[allow(unsafe_code)]
- #[allow(warnings)]
- $crate::k_mk_symbol(
- unsafe { $id },
- unsafe { $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes()) }
- )
- }
- }
-}
-
-/// assertion
-#[macro_export]
-macro_rules! k_assert {
- ($e: expr) => {
- {
- use klee::ll;
- if !$e {
- unsafe {
- ll::abort();
- }
- }
+ #[allow(unsafe_code)]
+ #[allow(warnings)]
+ $crate::k_mk_symbol(
+ unsafe { $id },
+ unsafe { $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes()) }
+ )
}
}
}
--
GitLab