Skip to content

introduce widen_if_needed #7938

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Oct 5, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 2 additions & 9 deletions src/ansi-c/c_preprocess.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,7 @@ Author: Daniel Kroening, [email protected]
#include <util/run.h>
#include <util/suffix.h>
#include <util/tempfile.h>

#ifdef _MSC_VER
# include <util/unicode.h>
#endif
#include <util/unicode.h>

#include <fstream>

Expand Down Expand Up @@ -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)
{
Expand Down
21 changes: 7 additions & 14 deletions src/cbmc/cbmc_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -16,17 +16,9 @@ Author: Daniel Kroening, [email protected]
#include <util/help_formatter.h>
#include <util/invariant.h>
#include <util/make_unique.h>
#include <util/unicode.h>
#include <util/version.h>

#include <cstdlib> // exit()
#include <fstream> // IWYU pragma: keep
#include <iostream>
#include <memory>

#ifdef _MSC_VER
# include <util/unicode.h>
#endif

#include <goto-programs/initialize_goto_model.h>
#include <goto-programs/link_to_library.h>
#include <goto-programs/loop_ids.h>
Expand Down Expand Up @@ -69,6 +61,11 @@ Author: Daniel Kroening, [email protected]

#include "c_test_input_generator.h"

#include <cstdlib> // exit()
#include <fstream> // IWYU pragma: keep
#include <iostream>
#include <memory>

cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
: parse_options_baset(
CBMC_OPTIONS,
Expand Down Expand Up @@ -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)
{
Expand Down
12 changes: 3 additions & 9 deletions src/cprover/cprover_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -19,12 +19,9 @@ Author: Daniel Kroening, [email protected]
#include <util/parse_options.h>
#include <util/signal_catcher.h>
#include <util/ui_message.h>
#include <util/unicode.h>
#include <util/version.h>

#ifdef _WIN32
# include <util/unicode.h>
#endif

#include <goto-programs/adjust_float_expressions.h>
#include <goto-programs/goto_inline.h>
#include <goto-programs/initialize_goto_model.h>
Expand Down Expand Up @@ -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';
Expand Down
11 changes: 2 additions & 9 deletions src/goto-analyzer/show_on_source.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,7 @@ Author: Daniel Kroening, [email protected]
#include "show_on_source.h"

#include <util/message.h>

#ifdef _MSC_VER
# include <util/unicode.h>
#endif
#include <util/unicode.h>

#include <analyses/ai.h>

Expand Down Expand Up @@ -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);

Expand Down
11 changes: 3 additions & 8 deletions src/goto-cc/cl_message_handler.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,7 @@ Author: Michael Tautschnig

#include "cl_message_handler.h"

#ifdef _MSC_VER
# include <util/unicode.h>
#endif
#include <util/unicode.h>

#include <fstream>

Expand Down Expand Up @@ -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);
Expand Down
25 changes: 8 additions & 17 deletions src/goto-cc/compile.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,6 @@ Date: June 2006

#include "compile.h"

#include <cstring>
#include <fstream>
#include <iostream>

#include <util/cmdline.h>
#include <util/config.h>
#include <util/file_util.h>
Expand All @@ -26,27 +22,26 @@ Date: June 2006
#include <util/symbol_table_builder.h>
#include <util/tempdir.h>
#include <util/tempfile.h>
#include <util/unicode.h>
#include <util/version.h>

#ifdef _MSC_VER
# include <util/unicode.h>
#endif

#include <ansi-c/ansi_c_entry_point.h>
#include <ansi-c/c_object_factory_parameters.h>

#include <goto-programs/goto_convert_functions.h>
#include <goto-programs/name_mangler.h>
#include <goto-programs/read_goto_binary.h>
#include <goto-programs/write_goto_binary.h>

#include <ansi-c/ansi_c_entry_point.h>
#include <ansi-c/c_object_factory_parameters.h>
#include <langapi/language.h>
#include <langapi/language_file.h>
#include <langapi/mode.h>

#include <linking/linking.h>
#include <linking/static_lifetime_init.h>

#include <cstring>
#include <fstream>
#include <iostream>

#define DOTGRAPHSETTINGS "color=black;" \
"orientation=portrait;" \
"fontsize=20;"\
Expand Down Expand Up @@ -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)
{
Expand Down
11 changes: 3 additions & 8 deletions src/goto-cc/gcc_message_handler.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,7 @@ Author: Daniel Kroening, [email protected]

#include "gcc_message_handler.h"

#ifdef _MSC_VER
# include <util/unicode.h>
#endif
#include <util/unicode.h>

#include <fstream> // IWYU pragma: keep
#include <iostream>
Expand Down Expand Up @@ -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));
Expand Down
19 changes: 5 additions & 14 deletions src/goto-checker/solver_factory.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,16 +17,10 @@ Author: Daniel Kroening, Peter Schrammel
#include <util/make_unique.h>
#include <util/message.h>
#include <util/options.h>
#include <util/version.h>

#include <iostream>

#ifdef _MSC_VER
#include <util/unicode.h>
#endif

#include <solvers/stack_decision_procedure.h>
#include <util/version.h>

#include <goto-symex/solver_hardness.h>
#include <solvers/flattening/bv_dimacs.h>
#include <solvers/prop/prop.h>
#include <solvers/prop/solver_resource_limits.h>
Expand All @@ -36,9 +30,10 @@ Author: Daniel Kroening, Peter Schrammel
#include <solvers/sat/satcheck.h>
#include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
#include <solvers/smt2_incremental/smt_solver_process.h>
#include <solvers/stack_decision_procedure.h>
#include <solvers/strings/string_refinement.h>

#include <goto-symex/solver_hardness.h>
#include <iostream>

solver_factoryt::solver_factoryt(
const optionst &_options,
Expand Down Expand Up @@ -450,11 +445,7 @@ std::unique_ptr<std::ofstream> open_outfile_and_check(
if(filename.empty())
return nullptr;

#ifdef _MSC_VER
auto out = util_make_unique<std::ofstream>(widen(filename));
#else
auto out = util_make_unique<std::ofstream>(filename);
#endif
auto out = util_make_unique<std::ofstream>(widen_if_needed(filename));

if(!*out)
{
Expand Down
47 changes: 14 additions & 33 deletions src/goto-instrument/goto_instrument_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -18,16 +18,9 @@ Author: Daniel Kroening, [email protected]
#include <util/options.h>
#include <util/string2int.h>
#include <util/string_utils.h>
#include <util/unicode.h>
#include <util/version.h>

#include <fstream> // IWYU pragma: keep
#include <iostream>
#include <memory>

#ifdef _MSC_VER
# include <util/unicode.h>
#endif

#include <goto-programs/class_hierarchy.h>
#include <goto-programs/ensure_one_backedge_per_target.h>
#include <goto-programs/goto_check.h>
Expand Down Expand Up @@ -109,6 +102,10 @@ Author: Daniel Kroening, [email protected]
#include "unwind.h"
#include "value_set_fi_fp_removal.h"

#include <fstream> // IWYU pragma: keep
#include <iostream>
#include <memory>

#include "accelerate/accelerate.h"

/// invoke main modules
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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] << "'";
Expand Down Expand Up @@ -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] << "'";
Expand Down Expand Up @@ -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)
{
Expand Down Expand Up @@ -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;

Expand Down
11 changes: 2 additions & 9 deletions src/goto-instrument/unwindset.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,7 @@ Author: Daniel Kroening, [email protected]
#include <util/string2int.h>
#include <util/string_utils.h>
#include <util/symbol_table.h>

#ifdef _MSC_VER
# include <util/unicode.h>
#endif
#include <util/unicode.h>

#include <goto-programs/abstract_goto_model.h>

Expand Down Expand Up @@ -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;
Expand Down
Loading