Several fixes for SV-COMP #172
Merged
Conversation
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
The last number of the symbol is not necessarily the location number since it may be the unwinding number. Handle that it localSSAt::get_loc_with_symbol_def.
|
@peterschrammel do you think that disabling |
If --values-refine is on, we first try the intervals domain and then the zones domain. Until now, this has been supported for AI only, now support for k-induction, too. This requires some tests to use --intervals instead of --values-refine since the zones invariant inference takes too long.
Standard invariants seem to cause more trouble than with array invariants (already fixed). Let us try to disable them completely since they should bring no significant benefits. There are some tests which still require standard invariants with k-induction. Add the option explicitly and we will debug them later.
There must be no code between creating dynamic objects (replace malloc) and splitting them into instances since if the code in between changes numbering of GOTO nodes, the split objects may have a different location number than the original objects (which contain also a concrete object). This may cause some trouble later, especially with the zones domain, when it would add differences between fields of objects that can never be allocated at the same time (have contradictory allocation guards). Such template rows would make the invariant incomputable, yielding false negative results.
viktormalik
force-pushed
the
svcomp-fixes
branch
from
55c0e80 to
9bf6ad4
Compare
Array domain uses some extra renamings in post_renaming_map. These are cleared in the array domain constructor, however, they remain there if no array template is created (when there are no array variables), which may intercept other domains. Fix the problem by removing the renamings if no array template is created.
Contains a fix of GOTO intstruction scopes in witnesses.
Signed-off-by: František Nečas <[email protected]>
|
Added some more fixes and updated the description. After this is merged, I'll do a new release. |
|
cc @FrNecas |
peterschrammel
approved these changes
Jan 9, 2023
|
|
||
| /// Makes user input nondeterministic, i.e. arguments of fscanf starting | ||
| /// from the second one are assigned a nondeterministic value. | ||
| void twols_parse_optionst::make_scanf_nondet(goto_modelt &goto_model) |
There was a problem hiding this comment.
(Not for this PR) Shouldn't this rather have a fix in CBMC's models library?
There was a problem hiding this comment.
IIRC I saw Michael fixing this in CBMC so it should already be fixed, we just need to update again, so this is a temporary workaround :)
There was a problem hiding this comment.
I thought about cherry-picking that fix to our fork, but I don't think it would have been that straight forward, there were more changes in the source code of C function models.
There was a problem hiding this comment.
Ok, then we can revert on the next CBMC prerequisites upgrade.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
List of changes:
--values-refineand--k-induction- so far, we supported--values-refinefor AI only, which was fine since it was needed for heap for which we disabled k-induction. Now with the new unwinding, we need to support--values-refinefor k-induction, too.--std-invariantsfor--k-inductionas it causes more problems than just for the array invariants (fixed in Support arrays with standard invariants #171). It also makes heap-data examples not to pass.*scanfcalls) non-deterministic.