From ef84a90c23fba5d24ed558dcf1abe51c80b04ade Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Jon=C3=A1=C5=A1?= Date: Thu, 14 Nov 2024 11:23:06 +0100 Subject: [PATCH 1/3] Mark vsnprintf as external --- include/klee/Statistics/Statistic.h | 1 + lib/Core/Executor.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/include/klee/Statistics/Statistic.h b/include/klee/Statistics/Statistic.h index bbb67116db..7407153305 100644 --- a/include/klee/Statistics/Statistic.h +++ b/include/klee/Statistics/Statistic.h @@ -11,6 +11,7 @@ #define KLEE_STATISTIC_H #include +#include namespace klee { class Statistic; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 65b4ad7c89..7756f7e156 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4282,6 +4282,7 @@ void Executor::terminateStateOnSolverError(ExecutionState &state, // XXX shoot me static const char *okExternalsList[] = { "printf", "fprintf", + "vsnprintf", "sscanf", "snprintf", "puts", From b896aefe6551bf1c3381e6199e6a813b327be773 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Paul=C3=ADna=20Ayaziov=C3=A1?= Date: Mon, 28 Oct 2024 19:20:01 +0100 Subject: [PATCH 2/3] Do not treat all values as unsigned in replay --- lib/Core/SpecialFunctionHandler.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 72ed553f56..571ea63e19 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -1106,7 +1106,7 @@ void SpecialFunctionHandler::handleVerifierNondetType(ExecutionState &state, // std::get<0>(nondet).c_str(), std::get<1>(nondet), // std::get<2>(nondet), val.getZExtValue()); - putConcreteValue(state, name, val.isSigned(), target, + putConcreteValue(state, name, isSigned, target, ConstantExpr::alloc(val.getZExtValue(), size)); ++position; // matched, move on From 110ba5d01f514b2f1e0f2638bc6454c8b9a07011 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Jon=C3=A1=C5=A1?= Date: Fri, 22 Nov 2024 08:57:13 +0100 Subject: [PATCH 3/3] Do not treat setlocale as pure function, fail instead. --- lib/Core/Executor.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 7756f7e156..37c5a2d8a6 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4404,7 +4404,7 @@ static std::set nokExternals({"fesetround", "fesetenv", "feclearexcept", "feraiseexcept", "gettext", "dcgettext" , "longjmp", "fgets", "getmntent", "__freading", "__fwriting", "fread", "fread_unlocked", - "strspn", "strtod"}); + "strspn", "strtod", "setlocale"}); void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,