From 67e40a9377ab27907aab6941dc14001886c6325d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20Tj=C3=A4der?= <henrik@tjaders.com> Date: Mon, 5 Feb 2018 15:52:42 +0100 Subject: [PATCH] Separated tested functions into a separate crate with modules --- .gitignore | 4 ++- .gitlab-ci.yml | 51 ++++++++++++++++++++++++++++++++++ klee-examples/Cargo.toml | 3 +- klee-examples/examples/foos.rs | 25 +++++++++++++++++ testfunction/Cargo.toml | 6 ++++ testfunction/src/lib.rs | 7 +++++ testfunction/src/m1.rs | 3 ++ testfunction/src/m2.rs | 3 ++ 8 files changed, 100 insertions(+), 2 deletions(-) create mode 100644 .gitlab-ci.yml create mode 100644 klee-examples/examples/foos.rs create mode 100644 testfunction/Cargo.toml create mode 100644 testfunction/src/lib.rs create mode 100644 testfunction/src/m1.rs create mode 100644 testfunction/src/m2.rs diff --git a/.gitignore b/.gitignore index 28f4043..560bf16 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,5 @@ **/*.rs.bk .#* -target \ No newline at end of file +target +*.swp +tags diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml new file mode 100644 index 0000000..5995c86 --- /dev/null +++ b/.gitlab-ci.yml @@ -0,0 +1,51 @@ +#.cargo_test_template: &cargo_test + #stage: test + #script: + #- ./run-cargo.sh + #- ls -lR + #- ./klee.sh + +#nightly:cargo: + #image: afoht/llvm4-klee-rust + #<<: *cargo_test + +stages: + - deploy + #- test + +# Setup the rust environment +#before_script: + #- pacman -Sy tree + #- apt-get update -yqq + #- apt-get install -yqq --no-install-recommends build-essential + ## Must be outside the project folder + #- cd / + #- cargo install cargo + ## Return + #- cd - + ##- rustup toolchain remove nightly + ##- rustup toolchain install nightly + #- rustup default nightly + #- rustup target add arm-unknown-linux-gnueabihf + #- rustup target add arm-unknown-linux-gnueabi + #- rustup target add armv7-unknown-linux-gnueabihf + #- rustup component add rust-src + #- rustup update + + +# Generate documentation +pages: + image: rustdocker/rust:nightly + stage: deploy + only: + - master + script: + - rm -rf public + - mkdir public + - cd cargo-klee + - cargo doc --no-deps + # The content inside the target doc folder, but index even deeper down + - cp -R target/doc/* ../public + artifacts: + paths: + - public diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml index 7b3ded6..205a709 100644 --- a/klee-examples/Cargo.toml +++ b/klee-examples/Cargo.toml @@ -5,6 +5,7 @@ authors = ["Jorge Aparicio <jorge@japaric.io>"] [dependencies] klee = {path="../klee"} +testfunction = {path="../testfunction"} [profile.release] -debug = true \ No newline at end of file +debug = true diff --git a/klee-examples/examples/foos.rs b/klee-examples/examples/foos.rs new file mode 100644 index 0000000..d00d2ee --- /dev/null +++ b/klee-examples/examples/foos.rs @@ -0,0 +1,25 @@ +#![no_std] + +#[macro_use] +extern crate klee; + +extern crate testfunction; + +use core::ptr; +use testfunction::m1::*; +use testfunction::m2::*; + +fn main() { + let u = ksymbol!("u"); + + unsafe { + ptr::read_volatile(&f2(f1(u))); + } +} + +// add 1 wrapping +//mod m1; +//mod m2; + +//use m1::*; +//use m2::*; diff --git a/testfunction/Cargo.toml b/testfunction/Cargo.toml new file mode 100644 index 0000000..473a473 --- /dev/null +++ b/testfunction/Cargo.toml @@ -0,0 +1,6 @@ +[package] +name = "testfunction" +version = "0.1.0" +authors = ["Henrik Tjäder <henrik@tjaders.com>"] + +[dependencies] diff --git a/testfunction/src/lib.rs b/testfunction/src/lib.rs new file mode 100644 index 0000000..b3e545b --- /dev/null +++ b/testfunction/src/lib.rs @@ -0,0 +1,7 @@ +#![no_std] + +pub mod m1; +pub mod m2; + +use m1::*; +use m2::*; diff --git a/testfunction/src/m1.rs b/testfunction/src/m1.rs new file mode 100644 index 0000000..14e1fab --- /dev/null +++ b/testfunction/src/m1.rs @@ -0,0 +1,3 @@ +pub fn f1(u: u8) -> u8 { + u.wrapping_add(1) +} diff --git a/testfunction/src/m2.rs b/testfunction/src/m2.rs new file mode 100644 index 0000000..87e0c46 --- /dev/null +++ b/testfunction/src/m2.rs @@ -0,0 +1,3 @@ +pub fn f2(u: u8) -> u8 { + 100 / u +} -- GitLab