From 2fdd5aa8fc01e3d5c1ff66adf03b6dbb8e427ecd Mon Sep 17 00:00:00 2001 From: Andrea Mattavelli Date: Thu, 4 Aug 2016 17:00:01 +0100 Subject: Modified logging information to steer the usage of klee_message, klee_warning, and klee_error --- lib/Basic/ConstructSolverChain.cpp | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'lib/Basic') diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp index 2df87d51..debb1e9e 100644 --- a/lib/Basic/ConstructSolverChain.cpp +++ b/lib/Basic/ConstructSolverChain.cpp @@ -12,6 +12,7 @@ */ #include "klee/Common.h" #include "klee/CommandLine.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "llvm/Support/raw_ostream.h" namespace klee { @@ -24,15 +25,15 @@ Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath, if (optionIsSet(queryLoggingOptions, SOLVER_PC)) { solver = createPCLoggingSolver(solver, baseSolverQueryPCLogPath, MinQueryTimeToLog); - llvm::errs() << "Logging queries that reach solver in .pc format to " - << baseSolverQueryPCLogPath.c_str() << "\n"; + klee_message("Logging queries that reach solver in .pc format to %s\n", + baseSolverQueryPCLogPath.c_str()); } if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB)) { solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, MinQueryTimeToLog); - llvm::errs() << "Logging queries that reach solver in .smt2 format to " - << baseSolverQuerySMT2LogPath.c_str() << "\n"; + klee_message("Logging queries that reach solver in .smt2 format to %s\n", + baseSolverQuerySMT2LogPath.c_str()); } if (UseFastCexSolver) @@ -52,15 +53,15 @@ Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath, if (optionIsSet(queryLoggingOptions, ALL_PC)) { solver = createPCLoggingSolver(solver, queryPCLogPath, MinQueryTimeToLog); - llvm::errs() << "Logging all queries in .pc format to " - << queryPCLogPath.c_str() << "\n"; + klee_message("Logging all queries in .pc format to %s\n", + queryPCLogPath.c_str()); } if (optionIsSet(queryLoggingOptions, ALL_SMTLIB)) { solver = createSMTLIBLoggingSolver(solver, querySMT2LogPath, MinQueryTimeToLog); - llvm::errs() << "Logging all queries in .smt2 format to " - << querySMT2LogPath.c_str() << "\n"; + klee_message("Logging all queries in .smt2 format to %s\n", + querySMT2LogPath.c_str()); } if (DebugCrossCheckCoreSolverWith != NO_SOLVER) { Solver *oracleSolver = createCoreSolver(DebugCrossCheckCoreSolverWith); -- cgit 1.4.1