fprintf: convert to klee_warning

In some Solver sources, some error outputs were missing \n. Instead of
adding a new line to all of them, convert the fprintf's to
klee_warning which adds \n automatically.

ErrorHandling.h had to be included in MetaSMTSolver.cpp to have
klee_warning declared there.

Signed-off-by: Jiri Slaby <jslaby@suse.cz>

2 files changed, 11 insertions, 10 deletions

diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index 56964b5d..411c07b1 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -11,6 +11,7 @@
 
 #include "MetaSMTBuilder.h"
 #include "klee/Constraints.h"
+#include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
 #include "klee/util/Assignment.h"
@@ -281,7 +282,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
   fflush(stderr);
   int pid = fork();
   if (pid == -1) {
-    fprintf(stderr, "error: fork failed (for metaSMT)");
+    klee_warning("fork failed (for metaSMT)");
     return (SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED);
   }
 
@@ -388,7 +389,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
     } while (res < 0 && errno == EINTR);
 
     if (res < 0) {
-      fprintf(stderr, "error: waitpid() for metaSMT failed");
+      klee_warning("waitpid() for metaSMT failed");
       return (SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED);
     }
 
@@ -408,10 +409,10 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
     } else if (exitcode == 1) {
       hasSolution = false;
     } else if (exitcode == 52) {
-      fprintf(stderr, "error: metaSMT timed out");
+      klee_warning("metaSMT timed out");
       return (SolverImpl::SOLVER_RUN_STATUS_TIMEOUT);
     } else {
-      fprintf(stderr, "error: metaSMT did not return a recognized code");
+      klee_warning("metaSMT did not return a recognized code");
       return (SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE);
     }
 
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index f2500572..e1d41eba 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -231,7 +231,7 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q,
   fflush(stderr);
   int pid = fork();
   if (pid == -1) {
-    fprintf(stderr, "ERROR: fork failed (for STP)");
+    klee_warning("fork failed (for STP)");
     if (!IgnoreSolverFailures)
       exit(1);
     return SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED;
@@ -266,7 +266,7 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q,
     } while (res < 0 && errno == EINTR);
 
     if (res < 0) {
-      fprintf(stderr, "ERROR: waitpid() for STP failed");
+      klee_warning("waitpid() for STP failed");
       if (!IgnoreSolverFailures)
         exit(1);
       return SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED;
@@ -276,8 +276,8 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q,
     // "occasion" return a status when the process was terminated by a
     // signal, so test signal first.
     if (WIFSIGNALED(status) || !WIFEXITED(status)) {
-      fprintf(stderr, "ERROR: STP did not return successfully.  Most likely "
-                      "you forgot to run 'ulimit -s unlimited'\n");
+      klee_warning("STP did not return successfully.  Most likely you forgot "
+                   "to run 'ulimit -s unlimited'");
       if (!IgnoreSolverFailures) {
         exit(1);
       }
@@ -290,11 +290,11 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q,
     } else if (exitcode == 1) {
       hasSolution = false;
     } else if (exitcode == 52) {
-      fprintf(stderr, "error: STP timed out");
+      klee_warning("STP timed out");
       // mark that a timeout occurred
       return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT;
     } else {
-      fprintf(stderr, "error: STP did not return a recognized code");
+      klee_warning("STP did not return a recognized code");
       if (!IgnoreSolverFailures)
         exit(1);
       return SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE;