diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp index 03f6d5d58dd..c753a0b0c31 100644 --- a/src/ansi-c/c_preprocess.cpp +++ b/src/ansi-c/c_preprocess.cpp @@ -15,10 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include - -#ifdef _MSC_VER -# include -#endif +#include #include @@ -720,11 +717,7 @@ bool c_preprocess_none( std::ostream &outstream, message_handlert &message_handler) { - #ifdef _MSC_VER - std::ifstream infile(widen(file)); - #else - std::ifstream infile(file); - #endif + std::ifstream infile(widen_if_needed(file)); if(!infile) { diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 882dbf4c13e..e310b2a623e 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -16,17 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include -#include // exit() -#include // IWYU pragma: keep -#include -#include - -#ifdef _MSC_VER -# include -#endif - #include #include #include @@ -69,6 +61,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_test_input_generator.h" +#include // exit() +#include // IWYU pragma: keep +#include +#include + cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv) : parse_options_baset( CBMC_OPTIONS, @@ -507,11 +504,7 @@ int cbmc_parse_optionst::doit() std::string filename=cmdline.args[0]; - #ifdef _MSC_VER - std::ifstream infile(widen(filename)); - #else - std::ifstream infile(filename); - #endif + std::ifstream infile(widen_if_needed(filename)); if(!infile) { diff --git a/src/cprover/cprover_parse_options.cpp b/src/cprover/cprover_parse_options.cpp index c55160d6bc6..977ac1186c7 100644 --- a/src/cprover/cprover_parse_options.cpp +++ b/src/cprover/cprover_parse_options.cpp @@ -19,12 +19,9 @@ Author: Daniel Kroening, dkr@amazon.com #include #include #include +#include #include -#ifdef _WIN32 -# include -#endif - #include #include #include @@ -236,11 +233,8 @@ int cprover_parse_optionst::main() if(cmdline.isset("outfile")) { auto file_name = cmdline.get_value("outfile"); -#ifdef _WIN32 - std::ofstream out(widen(file_name)); -#else - std::ofstream out(file_name); -#endif + std::ofstream out(widen_if_needed(file_name)); + if(!out) { std::cerr << "failed to open " << file_name << '\n'; diff --git a/src/goto-analyzer/show_on_source.cpp b/src/goto-analyzer/show_on_source.cpp index f7a1c1981f8..c6dc644b043 100644 --- a/src/goto-analyzer/show_on_source.cpp +++ b/src/goto-analyzer/show_on_source.cpp @@ -9,10 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "show_on_source.h" #include - -#ifdef _MSC_VER -# include -#endif +#include #include @@ -74,11 +71,7 @@ void show_on_source( const ai_baset &ai, message_handlert &message_handler) { -#ifdef _MSC_VER - std::ifstream in(widen(source_file)); -#else - std::ifstream in(source_file); -#endif + std::ifstream in(widen_if_needed(source_file)); messaget message(message_handler); diff --git a/src/goto-cc/cl_message_handler.cpp b/src/goto-cc/cl_message_handler.cpp index bf3d360d107..c2eb19456a5 100644 --- a/src/goto-cc/cl_message_handler.cpp +++ b/src/goto-cc/cl_message_handler.cpp @@ -8,9 +8,7 @@ Author: Michael Tautschnig #include "cl_message_handler.h" -#ifdef _MSC_VER -# include -#endif +#include #include @@ -42,11 +40,8 @@ void cl_message_handlert::print( if(full_path.has_value() && !line.empty()) { -#ifdef _MSC_VER - std::ifstream in(widen(full_path.value())); -#else - std::ifstream in(full_path.value()); -#endif + std::ifstream in(widen_if_needed(full_path.value())); + if(in) { const auto line_number = std::stoull(line); diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 613e17bd94a..7823142a6b7 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -13,10 +13,6 @@ Date: June 2006 #include "compile.h" -#include -#include -#include - #include #include #include @@ -26,27 +22,26 @@ Date: June 2006 #include #include #include +#include #include -#ifdef _MSC_VER -# include -#endif - -#include -#include - #include #include #include #include +#include +#include #include #include #include - #include #include +#include +#include +#include + #define DOTGRAPHSETTINGS "color=black;" \ "orientation=portrait;" \ "fontsize=20;"\ @@ -479,11 +474,7 @@ bool compilet::parse( if(file_name == "-") return parse_stdin(*languagep); -#ifdef _MSC_VER - std::ifstream infile(widen(file_name)); -#else - std::ifstream infile(file_name); -#endif + std::ifstream infile(widen_if_needed(file_name)); if(!infile) { diff --git a/src/goto-cc/gcc_message_handler.cpp b/src/goto-cc/gcc_message_handler.cpp index 3009f2d55c3..814dd836863 100644 --- a/src/goto-cc/gcc_message_handler.cpp +++ b/src/goto-cc/gcc_message_handler.cpp @@ -8,9 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "gcc_message_handler.h" -#ifdef _MSC_VER -# include -#endif +#include #include // IWYU pragma: keep #include @@ -68,11 +66,8 @@ void gcc_message_handlert::print( const auto file_name = location.full_path(); if(file_name.has_value() && !line.empty()) { -#ifdef _MSC_VER - std::ifstream in(widen(file_name.value())); -#else - std::ifstream in(file_name.value()); -#endif + std::ifstream in(widen_if_needed(file_name.value())); + if(in) { const auto line_number = std::stoull(id2string(line)); diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 2a35f5377e9..0dc0dffa550 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -17,16 +17,10 @@ Author: Daniel Kroening, Peter Schrammel #include #include #include -#include - -#include - -#ifdef _MSC_VER #include -#endif - -#include +#include +#include #include #include #include @@ -36,9 +30,10 @@ Author: Daniel Kroening, Peter Schrammel #include #include #include +#include #include -#include +#include solver_factoryt::solver_factoryt( const optionst &_options, @@ -450,11 +445,7 @@ std::unique_ptr open_outfile_and_check( if(filename.empty()) return nullptr; -#ifdef _MSC_VER - auto out = util_make_unique(widen(filename)); -#else - auto out = util_make_unique(filename); -#endif + auto out = util_make_unique(widen_if_needed(filename)); if(!*out) { diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index becae85c0eb..55721374ce6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -18,16 +18,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include -#include // IWYU pragma: keep -#include -#include - -#ifdef _MSC_VER -# include -#endif - #include #include #include @@ -109,6 +102,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "unwind.h" #include "value_set_fi_fp_removal.h" +#include // IWYU pragma: keep +#include +#include + #include "accelerate/accelerate.h" /// invoke main modules @@ -248,11 +245,8 @@ int goto_instrument_parse_optionst::doit() if(have_file) { -#ifdef _MSC_VER - std::ofstream of(widen(filename)); -#else - std::ofstream of(filename); -#endif + std::ofstream of(widen_if_needed(filename)); + if(!of) throw "failed to open file "+filename; @@ -745,11 +739,8 @@ int goto_instrument_parse_optionst::doit() if(cmdline.args.size()==2) { - #ifdef _MSC_VER - std::ofstream out(widen(cmdline.args[1])); - #else - std::ofstream out(cmdline.args[1]); - #endif + std::ofstream out(widen_if_needed(cmdline.args[1])); + if(!out) { log.error() << "failed to write to '" << cmdline.args[1] << "'"; @@ -844,11 +835,8 @@ int goto_instrument_parse_optionst::doit() if(cmdline.args.size()==2) { - #ifdef _MSC_VER - std::ofstream out(widen(cmdline.args[1])); - #else - std::ofstream out(cmdline.args[1]); - #endif + std::ofstream out(widen_if_needed(cmdline.args[1])); + if(!out) { log.error() << "failed to write to " << cmdline.args[1] << "'"; @@ -891,11 +879,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.args.size()==2) { - #ifdef _MSC_VER - std::ofstream out(widen(cmdline.args[1])); - #else - std::ofstream out(cmdline.args[1]); - #endif + std::ofstream out(widen_if_needed(cmdline.args[1])); if(!out) { @@ -1338,11 +1322,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(have_file) { -#ifdef _MSC_VER - std::ofstream of(widen(filename)); -#else - std::ofstream of(filename); -#endif + std::ofstream of(widen_if_needed(filename)); + if(!of) throw "failed to open file "+filename; diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp index 8c73f15d1cb..0905945c8e4 100644 --- a/src/goto-instrument/unwindset.cpp +++ b/src/goto-instrument/unwindset.cpp @@ -13,10 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include - -#ifdef _MSC_VER -# include -#endif +#include #include @@ -234,11 +231,7 @@ void unwindsett::parse_unwindset_file( const std::string &file_name, message_handlert &message_handler) { - #ifdef _MSC_VER - std::ifstream file(widen(file_name)); - #else - std::ifstream file(file_name); - #endif + std::ifstream file(widen_if_needed(file_name)); if(!file) throw "cannot open file "+file_name; diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 20e1ada9e8a..b5d420cc308 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -11,26 +11,23 @@ Author: Daniel Kroening, kroening@kroening.com #include "initialize_goto_model.h" -#include - #include +#include #include #include +#include -#ifdef _MSC_VER -# include -#endif +#include #include #include #include -#include -#include - #include "goto_convert_functions.h" #include "read_goto_binary.h" +#include + /// Generate an entry point that calls a function with the given name, based on /// the functions language mode in the symbol table static bool generate_entry_point_for_function( @@ -74,47 +71,42 @@ void initialize_from_source_files( for(const auto &filename : sources) { - #ifdef _MSC_VER - std::ifstream infile(widen(filename)); - #else - std::ifstream infile(filename); - #endif - - if(!infile) - { - throw system_exceptiont( - "Failed to open input file '" + filename + '\''); - } - - language_filet &lf=language_files.add_file(filename); - lf.language=get_language_from_filename(filename); - - if(lf.language==nullptr) - { - throw invalid_command_line_argument_exceptiont{ - "Failed to figure out type of file", filename}; - } - - languaget &language=*lf.language; - language.set_message_handler(message_handler); - language.set_language_options(options); - - msg.status() << "Parsing " << filename << messaget::eom; - - if(language.parse(infile, filename)) - { - throw invalid_input_exceptiont("PARSING ERROR"); - } - - lf.get_modules(); + std::ifstream infile(widen_if_needed(filename)); + + if(!infile) + { + throw system_exceptiont("Failed to open input file '" + filename + '\''); } - msg.status() << "Converting" << messaget::eom; + language_filet &lf = language_files.add_file(filename); + lf.language = get_language_from_filename(filename); - if(language_files.typecheck(symbol_table, message_handler)) + if(lf.language == nullptr) { - throw invalid_input_exceptiont("CONVERSION ERROR"); + throw invalid_command_line_argument_exceptiont{ + "Failed to figure out type of file", filename}; } + + languaget &language = *lf.language; + language.set_message_handler(message_handler); + language.set_language_options(options); + + msg.status() << "Parsing " << filename << messaget::eom; + + if(language.parse(infile, filename)) + { + throw invalid_input_exceptiont("PARSING ERROR"); + } + + lf.get_modules(); + } + + msg.status() << "Converting" << messaget::eom; + + if(language_files.typecheck(symbol_table, message_handler)) + { + throw invalid_input_exceptiont("CONVERSION ERROR"); + } } void set_up_custom_entry_point( diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index 8c2e1dc574e..73665d1ccb3 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -11,22 +11,19 @@ Module: Read Goto Programs #include "read_goto_binary.h" -#include - #include #include #include #include +#include -#ifdef _MSC_VER -# include -#endif - +#include "elf_reader.h" #include "goto_model.h" #include "link_goto_model.h" -#include "read_bin_goto_object.h" -#include "elf_reader.h" #include "osx_fat_reader.h" +#include "read_bin_goto_object.h" + +#include static bool read_goto_binary( const std::string &filename, @@ -64,11 +61,7 @@ static bool read_goto_binary( goto_functionst &goto_functions, message_handlert &message_handler) { - #ifdef _MSC_VER - std::ifstream in(widen(filename), std::ios::binary); - #else - std::ifstream in(filename, std::ios::binary); - #endif + std::ifstream in(widen_if_needed(filename), std::ios::binary); messaget message(message_handler); @@ -193,11 +186,7 @@ bool is_goto_binary( const std::string &filename, message_handlert &message_handler) { - #ifdef _MSC_VER - std::ifstream in(widen(filename), std::ios::binary); - #else - std::ifstream in(filename, std::ios::binary); - #endif + std::ifstream in(widen_if_needed(filename), std::ios::binary); if(!in) return false; diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp index 5729c9c29b6..46fe4fadd29 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp @@ -10,6 +10,7 @@ Author: Qinheping Hu #include #include +#include #include #include @@ -25,10 +26,6 @@ Author: Qinheping Hu #include #include -#ifdef _MSC_VER -# include -#endif - /// invoke main modules int goto_synthesizer_parse_optionst::doit() { @@ -84,11 +81,8 @@ int goto_synthesizer_parse_optionst::doit() // Output file specified if(cmdline.args.size() == 2) { -#ifdef _MSC_VER - std::ofstream out(widen(cmdline.args[1])); -#else - std::ofstream out(cmdline.args[1]); -#endif + std::ofstream out(widen_if_needed(cmdline.args[1])); + if(!out) { log.error() << "failed to write to '" << cmdline.args[1] << "'"; diff --git a/src/util/unicode.h b/src/util/unicode.h index c0b01ccb917..9e9f6f360e0 100644 --- a/src/util/unicode.h +++ b/src/util/unicode.h @@ -21,6 +21,13 @@ std::wstring widen(const char *s); std::string narrow(const std::wstring &s); std::wstring widen(const std::string &s); +// This removes the need to have a #ifdef whenever using std::fstream. +#ifdef _WIN32 +# define widen_if_needed(s) widen(s) +#else +# define widen_if_needed(s) (s) +#endif + std::string utf32_native_endian_to_utf8(const std::basic_string &s);