Expr-to-C: output type information with nondet_symbol #7675
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
tautschnig
requested review from
chris-ryder,
peterschrammel and
remi-delmas-3000
as code owners
Codecov ReportPatch coverage:
Additional details and impacted files@@ Coverage Diff @@
## develop #7675 +/- ##
===========================================
+ Coverage 78.54% 78.55% +0.01%
===========================================
Files 1686 1686
Lines 192905 192905
===========================================
+ Hits 151512 151536 +24
+ Misses 41393 41369 -24
☔ View full report in Codecov by Sentry. |
TGWDB
approved these changes
Apr 20, 2023
TGWDB
added a commit
that referenced
this pull request
May 3, 2023
peterschrammel
approved these changes
May 5, 2023
| @@ -1663,7 +1663,7 @@ std::string expr2ct::convert_symbol(const exprt &src) | |||
| std::string expr2ct::convert_nondet_symbol(const nondet_symbol_exprt &src) | |||
| { | |||
| const irep_idt id=src.get_identifier(); | |||
| return "nondet_symbol("+id2string(id)+")"; | |||
| return "nondet_symbol<" + convert(src.type()) + ">(" + id2string(id) + ")"; | |||
There was a problem hiding this comment.
Do we use that syntax elsewhere? An alternative would be cast syntax?
There was a problem hiding this comment.
I believe that the output of --program-only is the only place where this can currently be observed.
TGWDB
added a commit
that referenced
this pull request
May 11, 2023
TGWDB
added a commit
that referenced
this pull request
May 11, 2023
This is a debugging aid to make the output of `--program-only` more helpful when trying to see whether a call to malloc/calloc included type information (via a sizeof annotation).
tautschnig
force-pushed
the
features/nondet-type-info
branch
from
dbbc575 to
1a22d3e
Compare
tautschnig
assigned tautschnig and unassigned kroening, remi-delmas-3000 and peterschrammel
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.
This is a debugging aid to make the output of
--program-onlymore helpful when trying to see whether a call to malloc/calloc included type information (via a sizeof annotation).