-
Notifications
You must be signed in to change notification settings - Fork 275
Invariant cleanup goto programs jr #2967
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
hannes-steffenhagen-diffblue
merged 14 commits into
diffblue:develop
from
hannes-steffenhagen-diffblue:invariant_cleanup-goto_programs-jr
Oct 16, 2018
Merged
Changes from all commits
Commits
Show all changes
14 commits
Select commit
Hold shift + click to select a range
c20fe41
Cleanup invariants in lazy_goto_model
hannes-steffenhagen-diffblue c5f3488
Cleanup invariants in link_goto_model
hannes-steffenhagen-diffblue 15fec06
Cleanup invariants in loop_ids
hannes-steffenhagen-diffblue 63742c7
Cleanup invariants in osx_fat_reader
hannes-steffenhagen-diffblue b2bf11e
Cleanup invariants in parameter_assignments
hannes-steffenhagen-diffblue 50fd256
Cleanup invariants in pointer_arithmetic
hannes-steffenhagen-diffblue 5145d8c
Cleanup invariants in printf_formatter
hannes-steffenhagen-diffblue 0f35450
Cleanup invariants in read_bin_goto_object
hannes-steffenhagen-diffblue 46a233a
Cleanup invariants in remove_complex
hannes-steffenhagen-diffblue 0b7375e
Cleanup invariants in remove_const_function_pointers
hannes-steffenhagen-diffblue 4011b08
Cleanup invariants in remove_function_pointers
hannes-steffenhagen-diffblue bcc5ed9
Cleanup invariants in remove_unused_functions
hannes-steffenhagen-diffblue 5aaeaf8
Cleanup invariants in remove_vector
hannes-steffenhagen-diffblue 365bb72
Cleanup invariants in replace_calls
hannes-steffenhagen-diffblue File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,8 +1,8 @@ | ||
CORE | ||
main.c | ||
--replace-calls f:g | ||
Functions f and g are not type-compatible | ||
^EXIT=11$ | ||
functions f and g are not type-compatible | ||
^EXIT=1$ | ||
^SIGNAL=0$ | ||
-- | ||
^warning: ignoring |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,8 +1,8 @@ | ||
CORE | ||
main.c | ||
--replace-calls f:g | ||
Functions f and g are not type-compatible | ||
^EXIT=11$ | ||
functions f and g are not type-compatible | ||
^EXIT=1$ | ||
^SIGNAL=0$ | ||
-- | ||
^warning: ignoring |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,8 +1,8 @@ | ||
CORE | ||
main.c | ||
--replace-calls f:g --replace-calls h:f | ||
Function f cannot both be replaced and be a replacement | ||
^EXIT=11$ | ||
function f cannot both be replaced and be a replacement | ||
^EXIT=1$ | ||
^SIGNAL=0$ | ||
-- | ||
^warning: ignoring |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include "printf_formatter.h" | ||
|
||
#include <cassert> | ||
#include <sstream> | ||
|
||
#include <util/c_types.h> | ||
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.
Isn't this (most likely) also an
invalid_user_input_exceptiont
. It's of course possible that your file system is somehow hosed, but in almost all cases the user will be the one who got it wrong.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.
It's quite possible that the root cause is because the user passed in the wrong filename. Or it could fail for other reasons. The only thing we know at this point is that we can't open the file, so we report that as such here.