Minor fixes

Author: TGWDB

src/util/piped_process.cpp

@@ -35,8 +35,8 @@
 // access from the same session token/permissions. This SHOULD be sufficient
 // for what we need.
 //
-// Non-blocking pipes allow immediate reading of any data on the pipre which
-// matches the Linux/MasOC pipe behvariour and also allows reading of the
+// Non-blocking pipes allow immediate reading of any data on the pipe which
+// matches the Linux/MacOS pipe behaviour and also allows reading of the
 // string "The Jabberwocky" from the example above before waiting for the ping
 // command to terminate. This reading can be done with any of the usual pipe
 // read/peek functions, so we use those.
@@ -66,7 +66,7 @@
 //    finished, again undoing the interactive behaviour desired.
 // Since none of the above work effectivley, the chosen approach is to use a
 // non-blocking peek to see if there is anthing to read, and use a sleep and
-// poll behaviour that might be puch busier than we want. At the time of
+// poll behaviour that might be much busier than we want. At the time of
 // writing this has not been made smart, just a first choice option for how
 // frequently to poll.
 //
@@ -106,8 +106,8 @@ piped_processt::piped_processt(const std::vector<std::string> commandvec)
 #  ifdef _WIN32
   // Security attributes for pipe creation
   SECURITY_ATTRIBUTES sec_attr;
-  // Ensure pipes are inherited
   sec_attr.nLength = sizeof(SECURITY_ATTRIBUTES);
+  // Ensure pipes are inherited
   sec_attr.bInheritHandle = TRUE;
   // This sets the security to the default for the current session access token
   // See following link for details
@@ -118,9 +118,8 @@ piped_processt::piped_processt(const std::vector<std::string> commandvec)
   std::string base_name = "\\\\.\\pipe\\cbmc\\SMT2\\child\\";
   // Use process ID as a unique ID for this process at this time.
   base_name.append(std::to_string(GetCurrentProcessId()));
-  std::string tmp_name = base_name;
-  tmp_name.append("\\IN");
-  LPCSTR tmp_str = tmp_name.c_str();
+  const std::string in_name = base_name + "\\IN";
+  LPCSTR tmp_str = in_name.c_str();
   child_std_IN_Rd = CreateNamedPipe(
     tmp_str,
     PIPE_ACCESS_INBOUND,          // Reading for us
@@ -152,9 +151,8 @@ piped_processt::piped_processt(const std::vector<std::string> commandvec)
     throw std::runtime_error(
       "Input pipe creation failed on SetHandleInformation");
   }
-  tmp_name = base_name;
-  tmp_name.append("\\OUT");
-  tmp_str = tmp_name.c_str();
+  const std::string out_name = base_name + "\\OUT";
+  tmp_str = out_name.c_str();
   child_std_OUT_Rd = CreateNamedPipe(
     tmp_str,
     PIPE_ACCESS_INBOUND,          // Reading for us
@@ -189,7 +187,6 @@ piped_processt::piped_processt(const std::vector<std::string> commandvec)
   }
   // Create the child process
   STARTUPINFOW start_info;
-  BOOL success = FALSE;
   ZeroMemory(&proc_info, sizeof(PROCESS_INFORMATION));
   ZeroMemory(&start_info, sizeof(STARTUPINFOW));
   start_info.cb = sizeof(STARTUPINFOW);
@@ -206,7 +203,7 @@ piped_processt::piped_processt(const std::vector<std::string> commandvec)
   }
   // Note that we do NOT free this since it becomes part of the child
   // and causes heap corruption in Windows if we free!
-  success = CreateProcessW(
+  const BOOL success = CreateProcessW(
     NULL,                     // application name, we only use the command below
     _wcsdup(cmdline.c_str()), // command line
     NULL,                     // process security attributes
@@ -368,7 +365,9 @@ std::string piped_processt::receive()
     success = ReadFile(child_std_OUT_Rd, buff, BUFSIZE, &nbytes, NULL);
 #else
     nbytes = read(pipe_output[0], buff, BUFSIZE);
-    success = nbytes > 0; // 0 is error, -1 is nothing to read
+    if(nbytes == 0) // Update if the pipe is stopped
+      process_state = statet::STOPPED;
+    success = nbytes > 0;
 #endif
     INVARIANT(
       nbytes < BUFSIZE,