From 281c5117edaf04c89f831822f74ad568b4233dad Mon Sep 17 00:00:00 2001 From: Joe Ranweiler Date: Mon, 19 Feb 2018 11:46:38 -0800 Subject: [PATCH] Add example for `DeepState_TakeOver()` --- examples/CMakeLists.txt | 3 +++ examples/TakeOver.cpp | 45 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 48 insertions(+) create mode 100644 examples/TakeOver.cpp diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 746b4ce..8db60a0 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -43,3 +43,6 @@ target_link_libraries(StreamingAndFormatting deepstate) add_executable(Squares Squares.c) target_link_libraries(Squares deepstate) set_target_properties(Squares PROPERTIES COMPILE_DEFINITIONS "DEEPSTATE_TEST") + +add_executable(TakeOver TakeOver.cpp) +target_link_libraries(TakeOver deepstate) diff --git a/examples/TakeOver.cpp b/examples/TakeOver.cpp new file mode 100644 index 0000000..d31db80 --- /dev/null +++ b/examples/TakeOver.cpp @@ -0,0 +1,45 @@ +/* + * Copyright (c) 2018 Trail of Bits, Inc. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + + +#include + +using namespace deepstate; + +DEEPSTATE_NOINLINE void func(uint32_t x) { + CHECK_LT(x, 0x1234) + << "Found x=" << x << " was not greater than 0x1234."; + + if (x < 0x1234) { + printf("hi\n"); + } else { + printf("bye\n"); + } +} + +int main(int argc, char *argv[]) { + DeepState_InitOptions(argc, argv); + + uint32_t x = 123; + func(x); // Unexplored + + DeepState_TakeOver(); + + Symbolic y; + Symbolic z; + func(y); // Explored + func(z); // Explored +}