-
Notifications
You must be signed in to change notification settings - Fork 277
Invariant cleanup goto programs sz #2968
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
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include "set_properties.h" | ||
|
||
#include <util/exception_utils.h> | ||
|
||
#include <algorithm> | ||
#include <unordered_set> | ||
|
||
|
@@ -111,7 +113,9 @@ void set_properties( | |
set_properties(it->second.body, property_set); | ||
|
||
if(!property_set.empty()) | ||
throw "property "+id2string(*property_set.begin())+" not found"; | ||
throw invalid_command_line_argument_exceptiont( | ||
"property " + id2string(*property_set.begin()) + " unknown", | ||
"--property id"); | ||
} | ||
|
||
void label_properties(goto_functionst &goto_functions) | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -21,6 +21,8 @@ Date: December 2016 | |
#include <util/cprover_prefix.h> | ||
#include <util/prefix.h> | ||
|
||
#include <util/invariant.h> | ||
|
||
#include <goto-programs/goto_functions.h> | ||
#include <goto-programs/remove_skip.h> | ||
|
||
|
@@ -32,8 +34,8 @@ void slice_global_inits(goto_modelt &goto_model) | |
const irep_idt entry_point=goto_functionst::entry_point(); | ||
goto_functionst &goto_functions=goto_model.goto_functions; | ||
|
||
if(!goto_functions.function_map.count(entry_point)) | ||
throw "entry point not found"; | ||
if(goto_functions.function_map.count(entry_point) == 0) | ||
throw user_input_error_exceptiont("entry point not found"); | ||
|
||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'd say it's misleading to throw this exception. A goto program without entry point is in no way malformed or incorrect. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Ok, I think that |
||
// Get the call graph restricted to functions reachable from | ||
// the entry point: | ||
|
@@ -73,7 +75,8 @@ void slice_global_inits(goto_modelt &goto_model) | |
|
||
goto_functionst::function_mapt::iterator f_it; | ||
f_it=goto_functions.function_map.find(INITIALIZE_FUNCTION); | ||
assert(f_it!=goto_functions.function_map.end()); | ||
if(f_it == goto_functions.function_map.end()) | ||
throw incorrect_goto_program_exceptiont("initialize function not found"); | ||
|
||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This isn't an internal invariant, but a well-formed-ness condition on the goto binary. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Changed to incorrect goto exception. |
||
goto_programt &goto_program=f_it->second.body; | ||
|
||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -14,8 +14,27 @@ Date: December 2016 | |
#ifndef CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H | ||
#define CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H | ||
|
||
#include <util/exception_utils.h> | ||
|
||
class goto_modelt; | ||
|
||
class user_input_error_exceptiont : public cprover_exception_baset | ||
{ | ||
public: | ||
explicit user_input_error_exceptiont(std::string message) | ||
: message(std::move(message)) | ||
{ | ||
} | ||
|
||
std::string what() const override | ||
{ | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Add 'override' |
||
return message; | ||
} | ||
|
||
private: | ||
std::string message; | ||
}; | ||
|
||
void slice_global_inits(goto_modelt &); | ||
|
||
#endif |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -16,9 +16,10 @@ Author: Daniel Kroening, [email protected] | |
#include <util/arith_tools.h> | ||
#include <util/c_types.h> | ||
#include <util/config.h> | ||
#include <util/invariant.h> | ||
#include <util/message.h> | ||
#include <util/std_expr.h> | ||
#include <util/std_code.h> | ||
#include <util/std_expr.h> | ||
#include <util/symbol_table.h> | ||
|
||
#include <goto-programs/format_strings.h> | ||
|
@@ -279,9 +280,9 @@ void string_instrumentationt::do_sprintf( | |
|
||
if(arguments.size()<2) | ||
{ | ||
error().source_location=target->source_location; | ||
error() << "sprintf expected to have two or more arguments" << eom; | ||
throw 0; | ||
throw incorrect_source_program_exceptiont( | ||
"sprintf expected to have two or more arguments", | ||
target->source_location); | ||
} | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This isn't really a property of the goto-program, but one of the original source code. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Introduced new exception for source code errors (used a few times in this file). |
||
|
||
goto_programt tmp; | ||
|
@@ -321,10 +322,9 @@ void string_instrumentationt::do_snprintf( | |
|
||
if(arguments.size()<3) | ||
{ | ||
error().source_location=target->source_location; | ||
error() << "snprintf expected to have three or more arguments" | ||
<< eom; | ||
throw 0; | ||
throw incorrect_source_program_exceptiont( | ||
"snprintf expected to have three or more arguments", | ||
target->source_location); | ||
} | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Same here. |
||
|
||
goto_programt tmp; | ||
|
@@ -364,9 +364,8 @@ void string_instrumentationt::do_fscanf( | |
|
||
if(arguments.size()<2) | ||
{ | ||
error().source_location=target->source_location; | ||
error() << "fscanf expected to have two or more arguments" << eom; | ||
throw 0; | ||
throw incorrect_source_program_exceptiont( | ||
"fscanf expected to have two or more arguments", target->source_location); | ||
} | ||
|
||
goto_programt tmp; | ||
|
@@ -650,9 +649,8 @@ void string_instrumentationt::do_strchr( | |
|
||
if(arguments.size()!=2) | ||
{ | ||
error().source_location=target->source_location; | ||
error() << "strchr expected to have two arguments" << eom; | ||
throw 0; | ||
throw incorrect_source_program_exceptiont( | ||
"strchr expected to have two arguments", target->source_location); | ||
} | ||
|
||
goto_programt tmp; | ||
|
@@ -677,9 +675,8 @@ void string_instrumentationt::do_strrchr( | |
|
||
if(arguments.size()!=2) | ||
{ | ||
error().source_location=target->source_location; | ||
error() << "strrchr expected to have two arguments" << eom; | ||
throw 0; | ||
throw incorrect_source_program_exceptiont( | ||
"strrchr expected to have two arguments", target->source_location); | ||
} | ||
|
||
goto_programt tmp; | ||
|
@@ -704,9 +701,8 @@ void string_instrumentationt::do_strstr( | |
|
||
if(arguments.size()!=2) | ||
{ | ||
error().source_location=target->source_location; | ||
error() << "strstr expected to have two arguments" << eom; | ||
throw 0; | ||
throw incorrect_source_program_exceptiont( | ||
"strstr expected to have two arguments", target->source_location); | ||
} | ||
|
||
goto_programt tmp; | ||
|
@@ -738,9 +734,8 @@ void string_instrumentationt::do_strtok( | |
|
||
if(arguments.size()!=2) | ||
{ | ||
error().source_location=target->source_location; | ||
error() << "strtok expected to have two arguments" << eom; | ||
throw 0; | ||
throw incorrect_source_program_exceptiont( | ||
"strtok expected to have two arguments", target->source_location); | ||
} | ||
|
||
goto_programt tmp; | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -14,9 +14,30 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include "goto_functions.h" | ||
|
||
#include <util/exception_utils.h> | ||
|
||
class message_handlert; | ||
class goto_modelt; | ||
|
||
class incorrect_source_program_exceptiont : public cprover_exception_baset | ||
{ | ||
public: | ||
incorrect_source_program_exceptiont( | ||
std::string message, | ||
source_locationt source_location) | ||
: message(std::move(message)), source_location(std::move(source_location)) | ||
{ | ||
} | ||
std::string what() const override | ||
{ | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. override |
||
return message + " (at: " + source_location.as_string() + ")"; | ||
} | ||
|
||
private: | ||
std::string message; | ||
source_locationt source_location; | ||
}; | ||
|
||
void string_instrumentation( | ||
symbol_tablet &, | ||
message_handlert &, | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -13,7 +13,6 @@ Date: June 2011 | |
|
||
#include "vcd_goto_trace.h" | ||
|
||
#include <cassert> | ||
#include <ctime> | ||
|
||
#include <util/numbering.h> | ||
|
@@ -55,8 +54,7 @@ std::string as_vcd_binary( | |
} | ||
else if(expr.id()==ID_union) | ||
{ | ||
assert(expr.operands().size()==1); | ||
return as_vcd_binary(expr.op0(), ns); | ||
return as_vcd_binary(to_union_expr(expr).op(), ns); | ||
} | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'd write .op() above. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Ok. |
||
|
||
// build "xxx" | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -17,6 +17,8 @@ Author: Daniel Kroening, [email protected] | |
#include <util/std_code.h> | ||
#include <util/base_type.h> | ||
|
||
#include <util/invariant.h> | ||
|
||
bool has_nondet(const exprt &dest) | ||
{ | ||
forall_operands(it, dest) | ||
|
@@ -263,6 +265,6 @@ exprt wp( | |
return post; // ignored | ||
else if(statement==ID_fence) | ||
return post; // ignored | ||
else | ||
throw "sorry, wp("+id2string(statement)+"...) not implemented"; | ||
INVARIANT_WITH_DIAGNOSTICS( | ||
false, "sorry, wp(", id2string(statement), "...) is not implemented"); | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -13,8 +13,10 @@ Author: CM Wintersteiger | |
|
||
#include <fstream> | ||
|
||
#include <util/message.h> | ||
#include <util/exception_utils.h> | ||
#include <util/invariant.h> | ||
#include <util/irep_serialization.h> | ||
#include <util/message.h> | ||
#include <util/symbol_table.h> | ||
|
||
#include <goto-programs/goto_model.h> | ||
|
@@ -148,22 +150,18 @@ bool write_goto_binary( | |
irep_serializationt::ireps_containert irepc; | ||
irep_serializationt irepconverter(irepc); | ||
|
||
switch(version) | ||
{ | ||
case 1: | ||
case 2: | ||
case 3: | ||
throw "version no longer supported"; | ||
|
||
case 4: | ||
const int current_goto_version = 4; | ||
if(version < current_goto_version) | ||
throw invalid_command_line_argument_exceptiont( | ||
"version " + std::to_string(version) + " no longer supported", | ||
"supported version = " + std::to_string(current_goto_version)); | ||
else if(version > current_goto_version) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. If you print the current version, also print the version of the goto binary. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Done. |
||
throw invalid_command_line_argument_exceptiont( | ||
"unknown goto binary version " + std::to_string(version), | ||
"supported version = " + std::to_string(current_goto_version)); | ||
else | ||
return write_goto_binary_v4( | ||
out, symbol_table, goto_functions, irepconverter); | ||
|
||
default: | ||
throw "unknown goto binary version"; | ||
} | ||
|
||
return false; | ||
} | ||
|
||
/// Writes a goto program to disc | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That new exception isn't caught!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Added
catch
blocks to all call sites.