represent numerical values in CBMC trace in hex #2510
Conversation
polgreen
requested review from
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: f1cfe44).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77958102
|
The error on this appears to come because CBMC on Appveyor represents an unsigned int as an unsigned long, e.g., instead of |
|
I'm guessing this is because on all Microsoft environments |
|
Sure, I realise they are the same size, but it still seems like a bug to output long for everything. If nothing else it adds noise when trying to follow through an error trace. |
|
Hmmm, looks like the c-type for constants is guessed from their width, here: Obviously by guessing it can't give the right answer when |
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 9478104).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77990353
|
I've tweaked the regex now so that it works on windows and on linux |
|
Yeah, I couldn't be arsed wading into this either :) |
src/goto-programs/goto_trace.cpp
Outdated
| return oss.str(); | ||
| } | ||
|
|
||
| std::string trace_value_lowlevel( |
There was a problem hiding this comment.
Suggest just trace_value, as lowlevel suggests this is a fallback like expr2lisp or something
There was a problem hiding this comment.
There's already a trace_value function so I think introducing another one would make this pretty confusing. Is trace_numeric_value any better?
There was a problem hiding this comment.
Yeah that's fine, or integer_value if this is int types only
src/goto-programs/goto_trace.cpp
Outdated
| return oss.str(); | ||
| } | ||
|
|
||
| std::string trace_value_lowlevel( | ||
| const exprt &expr, |
There was a problem hiding this comment.
This could use a Doxy comment explaining what format you'll get and the customisations available via options
|
@smowton The width guessing in the parser is correct: the ISO C standard says so. The reason for the problem with the type of the literals is more subtle, unfortunately. On windows, the width of long and int are the same; the types only differ in a comment #c_type. The following happens: After symbolic simulation, we hash the expressions, using a hash that ignores the comments. Thus, on Windows, they get hashed to the same irep. I think we need to promote that comment to be a proper irep field. |
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 9c1eb1a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78078212
polgreen
requested review from
chrisr-diffblue,
forejtv,
martin-cs and
romainbrenguier
as code owners
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: a018652).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78157896
6409eae Merge pull request diffblue#2449 from tautschnig/c++-template-cleanup 1134455 Merge pull request diffblue#2443 from tautschnig/vs-rdecl 6e9e655 Merge pull request diffblue#2520 from smowton/smowton/feature/constant-propagator-selectivity 9013779 Merge pull request diffblue#2383 from tautschnig/no-sed 56a487e Constant propagator: add callback to filter tracked values a354513 Merge pull request diffblue#2510 from polgreen/hex_trace 3545be4 Merge pull request diffblue#2523 from peterschrammel/do-not-ignore-full-slice 819c683 Merge pull request diffblue#2493 from jeannielynnmoulton/jeannie/InnerClasses a018652 allow unsigned long instead of unsigned in regression test for hex_trace d5bbdd8 represent numerical values in CBMC trace in hex 19bddce Do not ignore --full-slice 5350133 Refactor inner class parsing. 6e554d9 Merge pull request diffblue#2500 from diffblue/git-version-speedup 9ba55e2 Marks anonymous classes as inner classes b96c7ba move build commands for version.h from common to util/ 6ce7b13 Clarifies language in documentation. c0c1029 Fixes parsing for anonymous classes 1930aef Refactors parsing of inner classes attribute. b28562b Adds unit test for parsing inner classes. c336455 Stores inner class data in java class types. 457bac9 Parses InnerClasses attribute of java bytecode. 34bd58f Clean up unused template instantiation symbols fea1f47 Remove unused parameter from rDeclarator e00c6ee Set BUILD_ENV via make variable instead of patching via sed git-subtree-dir: cbmc git-subtree-split: 6409eae
This adds an option to represent numeric values in the CBMC trace in hex