summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
28067ad)
A C library FILE does buffering (and possibly other opaque operations)
that can conflict with the model-checker's methods of snapshotting
memory. Particularly, it seems like we could corrupt and drop data that
was written to model_out, if the data was large enough and buffered in
just the right way.
Really, with the presence of dprintf(), there is no reason to print to a
FILE stream; we can just use the file descriptor (either STDOUT_FILENO
or the descriptor received from dup2()).
This fixes bugs seen in verbose mode, with a lot of extra debug
printing. Some of the output was being dropped.
#define MAX_TRACE_LEN 100
#define MAX_TRACE_LEN 100
-/** @brief Model-checker output stream; default to stdout until redirected */
-FILE *model_out = stdout;
+/** @brief Model-checker output file descriptor; default to stdout until redirected */
+int model_out = STDOUT_FILENO;
#define CONFIG_STACKTRACE
/** Print a backtrace of the current program state. */
void print_trace(void)
{
#ifdef CONFIG_STACKTRACE
#define CONFIG_STACKTRACE
/** Print a backtrace of the current program state. */
void print_trace(void)
{
#ifdef CONFIG_STACKTRACE
- print_stacktrace(model_out);
+ FILE *file = fdopen(model_out, "w");
+ print_stacktrace(file);
+ fclose(file);
#else
void *array[MAX_TRACE_LEN];
char **strings;
#else
void *array[MAX_TRACE_LEN];
char **strings;
*
* Redirects user program's stdout to a pipe so that we can dump it
* selectively, when displaying bugs, etc.
*
* Redirects user program's stdout to a pipe so that we can dump it
* selectively, when displaying bugs, etc.
- * Also connects a special file 'model_out' directly to stdout, for printing
+ * Also connects a file descriptor 'model_out' directly to stdout, for printing
* data when needed.
*
* The model-checker can selectively choose to print/hide the user program
* data when needed.
*
* The model-checker can selectively choose to print/hide the user program
int fd;
/* Save stdout for later use */
int fd;
/* Save stdout for later use */
- fd = dup(fileno(stdout));
- model_out = fdopen(fd, "w");
+ model_out = dup(fileno(stdout));
/* Redirect program output to a pipe */
int pipefd[2];
/* Redirect program output to a pipe */
int pipefd[2];
fflush(stdout);
/* Read program output pipe and write to (real) stdout */
fflush(stdout);
/* Read program output pipe and write to (real) stdout */
while (1) {
ret = read_to_buf(fd_user_out, buf, sizeof(buf));
if (!ret)
break;
while (ret > 0) {
while (1) {
ret = read_to_buf(fd_user_out, buf, sizeof(buf));
if (!ret)
break;
while (ret > 0) {
- int res = fwrite(buf, 1, ret, model_out);
+ ssize_t res = write(model_out, buf, ret);
- errno = ferror(model_out);
- perror("fwrite");
exit(EXIT_FAILURE);
}
ret -= res;
exit(EXIT_FAILURE);
}
ret -= res;
#include <stdio.h>
#include "config.h"
#include <stdio.h>
#include "config.h"
-#define model_print(fmt, ...) do { fprintf(model_out, fmt, ##__VA_ARGS__); } while (0)
+#define model_print(fmt, ...) do { dprintf(model_out, fmt, ##__VA_ARGS__); } while (0)
#ifdef CONFIG_DEBUG
#define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ##__VA_ARGS__); } while (0)
#ifdef CONFIG_DEBUG
#define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ##__VA_ARGS__); } while (0)
DEBUG("+++ Resetting to initial state +++\n");
node_stack->reset_execution();
DEBUG("+++ Resetting to initial state +++\n");
node_stack->reset_execution();
- /* Print all model-checker output before rollback */
- fflush(model_out);
-
/**
* FIXME: if we utilize partial rollback, we will need to free only
* those pending actions which were NOT pending before the rollback
/**
* FIXME: if we utilize partial rollback, we will need to free only
* those pending actions which were NOT pending before the rollback