Tests for future shadow memory feature #7479
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
peterschrammel
force-pushed
the
shadow-memory-tests
branch
2 times, most recently
from
f175a6c to
90faa39
Compare
Codecov ReportBase: 78.48% // Head: 78.48% // No change to project coverage 👍
Additional details and impacted files@@ Coverage Diff @@
## develop #7479 +/- ##
========================================
Coverage 78.48% 78.48%
========================================
Files 1663 1663
Lines 191188 191188
========================================
Hits 150054 150054
Misses 41134 41134 Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here. ☔ View full report at Codecov. |
peterschrammel
force-pushed
the
shadow-memory-tests
branch
from
90faa39 to
a3db5c6
Compare
tautschnig
approved these changes
Jan 16, 2023
peterschrammel
force-pushed
the
shadow-memory-tests
branch
from
a3db5c6 to
312305c
Compare
An example from the paper CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory. Bernd Fischer, Salvatore La Torre, Gennaro Parlato, Peter Schrammel. ASE'22.
More or less systematically test shadow memory for various data structure combinations.
More or less systematically test shadow memory for various data structure combinations.
Static memory requires a declaration for global fields.
Dynamic memory requires a declaration for global fields.
Test potential adverse interaction with string constants in value sets.
Test that we can attach integer-valued shadow memory to floats.
Checks that variable shadow memory values are handled correctly.
More or less systematically checks that byte-based accesses into shadow memory of nested structs and arrays work correctly.
More or less systematically tests that access to aggregates of integer-valued shadow memory returns the maximum of the shadow memory value of its constituting bytes.
More or less systematically tests that access to aggregates of bool-valued shadow memory returns the logic OR of the shadow memory value of its constituting bytes.
More or less systematically checks that byte-based shadow memory access to unions works correctly.
Checks that multi-byte accesses to integer-valued shadow memory for unions returns the maximum of the constituting bytes.
Checks that multi-byte accesses to integer-valued shadow memory for unions returns the logical OR of the constituting bytes.
Const char * parameters and pointers into string constants.
Checks that variables-sized arrrays are handled correctly.
Test initialization of various data types with custom values
Shadow memory mirrors pass-by-value and pass-by-reference semantics. Value parameters have their own shadow memory instances.
Checks that accessing shadow memory through void pointers returns the expected error messages, unless the correct casts have been applied.
Checks that shadow memory accesses are not confused by potentially nondeterministic accesses into structs.
Checks that a shadow memory accesses are not confused by potential accesses through NULL pointers.
Test deterministic and nondeterministic pointers to elements.
We must be able to attach shadow memory to the memory returned by __errno().
We must be able to attach memory to the memory returned by getenv().
Checks that the shadow memories of source and destination bufferes are independent.
Check that source and destination buffers have independent shadow memory.
Shadow memory assignments appear in trace.
The --no-shadow-memory-matching option will allow to avoid the allocation of shadow memory for matching variables.
peterschrammel
force-pushed
the
shadow-memory-tests
branch
from
312305c to
2a78b3d
Compare
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.
Tests only, marked FUTURE.