From bfda421e45898de79c47f5de705c46eee4258486 Mon Sep 17 00:00:00 2001
From: Jorge Aparicio <jorge@japaric.io>
Date: Sun, 28 Jan 2018 14:18:01 +0100
Subject: [PATCH] add termination lang item
---
klee-examples/examples/foo.rs | 2 +-
klee/src/lang_items.rs | 16 +++++++++++++++-
2 files changed, 16 insertions(+), 2 deletions(-)
diff --git a/klee-examples/examples/foo.rs b/klee-examples/examples/foo.rs
index 83851e4..af64ea3 100644
--- a/klee-examples/examples/foo.rs
+++ b/klee-examples/examples/foo.rs
@@ -6,7 +6,7 @@ extern crate klee;
use core::ptr;
fn main() {
- let u = symbol!("u");
+ let u = ksymbol!("u");
unsafe {
ptr::read_volatile(&f2(f1(u)));
diff --git a/klee/src/lang_items.rs b/klee/src/lang_items.rs
index bf97b30..f81e9e0 100644
--- a/klee/src/lang_items.rs
+++ b/klee/src/lang_items.rs
@@ -4,8 +4,22 @@ unsafe extern "C" fn panic_fmt(_: ::core::fmt::Arguments, _: &'static str, _: u3
}
#[lang = "start"]
-extern "C" fn start(main: fn(), _argc: isize, _argv: *const *const u8) -> isize {
+extern "C" fn start<T>(main: fn() -> T, _argc: isize, _argv: *const *const u8) -> isize
+ where
+ T: Termination,
+{
main();
0
}
+
+#[lang = "termination"]
+pub trait Termination {
+ fn report(self) -> i32;
+}
+
+impl Termination for () {
+ fn report(self) -> i32 {
+ 0
+ }
+}
--
GitLab