Memory analyzer squash #10
Closed
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
This code takes a static symbol, zero initalizes the typet of the symbol and then fills it up with values if possible. Following the declared structure in the typet, the analyzer queries the gdb api for values of the attributes of typet. It the symbol is a primtive type, the analyzer directly queries for the value of the symbol.
These test have been used as driving example for the memory analyzer. They test basic functionality and handling of cycles in structs.
To make private methos avilable to unit tests, it is a common practice to redefine the private keyword. While GCC doesn't carea bout this, older clang versions don't support this behavior and issue a warning. As all warnings are converted into errors, this waring breaks the build. To allow the intended behavior during testing, the -Wno-key-macro flag is added.
This commit adds the required files for the CMakeBuild system to build and generate the memory-analyzer
There has been a concurrency issue for one of the Travis CI builds. The ansi-c lib was not available, when travis tried to build the memory-analyzer binary.
Older gcc versions only compile c11 if the -std=c11 flag is set. Further this script assumed goto-gcc to be on the path. This is no longer required.
This adds an updated chain.sh file, and disables the existing regression tests. They currently fail due to two issues: goto code to c conversion currently ignores array sizes (i.e., even int arrays of known sizes are output as int[]), and void pointers are not handled (i.e., analyze_symbol() may try to zero initialize an object of type void, yielding an invariant violation).
This update the gdb api to return more information about pointers (via the method get_memory() which returns an object of type pointer_valuet describing the pointer and pointed-to data). Unit tests for the new functionality are included.
…pr.h A previous commit introduced e.g. function is_pointer() to check type.id() == ID_pointer. These have become obsolete as these expressions are now used directly.
This updates the symbol analyzer which is used by the memory analyzer. The class is refactored and updated to use the new gdb api.
We were doing this in multiple places, this should make it a bit easier to keep set properties consistent among different places. Ideally we could eventually move away from mentioning targets from modules here on the top level (and instead have each module call cprover_default_properties) but this isn't done in this commit. Because memory analyzer depends on GDB being present and further uses platform specific functionality at the moment it had some ifdef functionality to disable itself. This made the code a bit more complicated than it needed to be, and also lead to the code effectively building defunct executables. This removes these ifdefs and instead excludes memory-analyzer (and related tests) from the build unless requested (via WITH_MEMORY_ANALYZER environment variable or CMake option depending on whether it is a Make or CMake build respectively). Also force building memory-analyzer on Linux and test it there by default (unless explicitly unset). Behaviour on other platforms should be preserved.
and update the chain script accordingly.
mostly the description and expected output.
mostly white spaces and cprover_default_properties.
Add memory_addresst and documentation.
Better names and small code refactoring.
and add documentation.
Remove ui_message_handler dependence, fix header, etc.
to the new interface.
to CPROVER manual.
danpoe
force-pushed
the
feature/memory-analyzer
branch
from
c19aa7b to
35abeee
Compare
|
Thanks, cherry-picked the commits onto diffblue#4261. |
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.
I did some squashing but not sure if it's in any way better. It starts after this commit: diffblue@fc269bf.