|
CBMC
|
Output file container that handles stdout ("-") and regular files. More...
#include "output_file.h"#include "exception_utils.h"#include "unicode.h"#include <fstream>#include <iostream>
Include dependency graph for output_file.cpp:Go to the source code of this file.
Output file container that handles stdout ("-") and regular files.
Definition in file output_file.cpp.