output redirection

[c11tester.git] / main.cc

diff --git a/main.cc b/main.cc
index 10e2d3b93eae2e3c80e4569464e44a9ebb63d17a..f79366fb2d8450bcbbe69373ac45db600aec8caa 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -7,6 +7,7 @@
 #include <threads.h>
 #include "common.h"
 #include "threads-model.h"
+#include "output.h"
 
 #include "datarace.h"
 
@@ -130,6 +131,8 @@ static void model_main() {
                model->finish_execution();
        } while (model->next_execution());
 
+       model->print_stats();
+
        delete model;
 
        DEBUG("Exiting\n");
@@ -143,6 +146,9 @@ int main(int argc, char ** argv) {
        main_argc = argc;
        main_argv = argv;
 
+       /* Configure output redirection for the model-checker */
+       redirect_output();
+
        /* Let's jump in quickly and start running stuff */
        initSnapshotLibrary(10000, 1024, 1024, 4000, &model_main);
 }