Closed
Conversation
The CBMC code base normaly checks the id of an irept subtype against some magic id. But for some tests, it is necessary to check against more than one id. So this functions are use do the checks. This should further support code readability as a combination of different ids gets a name.
Applying CBMC on large code bases requires sometimes to model a test environment. Running a program until a certain point and let it crash, allows to analyze the memory state at this point in time. In continuation, the memory state might be reconstructed as base for the test environment model. By using gdb to analyze the core dump, I don't have to take care of reading and interpreting the core dump myself.
On multiple locations in the code base, magic numbers are used to mark the base of an intenger conversion. This commit introduces constants and replaces the magic numbers in some places.
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.
mmuesly
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
Contributor
Author
|
I messed up with whitespace changes in f8f661c, so I will fix this and create a new PR. |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
The idea of the memory-analyzer, is to create the global state required for some verification harnesses from a core dump file.
In order to do so, you have to feed in a binary with debug symbols and a core file, that matches the binary. An you also have to feed in the static symbols from global state, you care about.
The memory-analyzer will print out c code that is suitable to include it into a test harness in continuation.
This PR won't compile without #2599