diff options
author | Nguyễn Gia Phong <cnx@loang.net> | 2023-07-31 16:46:13 +0900 |
---|---|---|
committer | Nguyễn Gia Phong <cnx@loang.net> | 2024-03-05 17:26:57 +0900 |
commit | bb2337248e770863b8e488c8f02adf90369a624f (patch) | |
tree | d83f663cd84d9845d673c1be39b060ff84c06cec | |
parent | d37a4bca5dd23feabf0e4554a997a4b505b47f05 (diff) | |
download | klee-bb2337248e770863b8e488c8f02adf90369a624f.tar.gz |
Fallback on UB
This is not benefitting off UBSan, but there are too many moving parts now that a common denominator is needed for me to mentally keep track of things. (Yes, it's embarrassing that I commit less often working on software engineering research software, now I'm paying the price.)-;
-rw-r--r-- | lib/Core/Executor.cpp | 4 | ||||
-rw-r--r-- | shell.nix | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 6be77eb1..e0ab9f84 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4135,6 +4135,10 @@ void Executor::terminateStateOnError(ExecutionState &state, interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix); } + metaEnvVars[state.patchNo] = state.metaEnvVar; + getConstraintLog(state, state.formula, Interpreter::SMTLIB2); + if (exitStates[state.patchNo].insert(&state).second) + searchDifferentiators(&state); terminateState(state, terminationType); if (shouldExitOn(terminationType)) diff --git a/shell.nix b/shell.nix index 570f39bd..8e14a489 100644 --- a/shell.nix +++ b/shell.nix @@ -1,10 +1,10 @@ with import <nixpkgs> {}; let symbdiff = callPackage ./tools/symbdiff { }; in mkShell { - packages = [ clang symbdiff ]; + packages = [ llvmPackages_12.clang symbdiff ]; shellHook = '' # clang -emit-llvm -c -DKLEE_RUNTIME metaprogram.c for bitcode # clang -o metaprogram{,.c} for binary - alias clang='clang -g -O0 -Xclang -disable-O0-optnone' + alias clang='clang -g -O0 -Xclang -disable-O0-optnone -fsanitize=undefined -fno-sanitize=local-bounds,function,vptr' ''; } |