bug in concurrency encoding for arrays and structs #123
Labels
Comments
|
So what is the bug here - all of the tests are marked "CORE", none is "KNOWNBUG"? |
|
regression/cbmc-concurrency/struct_and_array1 was labelled KNOWNBUG -- I assume that this one is related. One can add another test that dynamically allocates the shared chunk of memory -- doesn't work either. Side remark: There are currently 150 regression tests marked as KNOWNBUG in the test suite. Maybe we should go through them and dump them all into the issue tracker so that they get eventually resolved. Currently, it is unclear why they are marked as KNOWNBUG (maybe just to silence them, maybe they have been resolved, maybe they are obsolete) or whether anyone is doing something about resolving them. |
|
On the side remark: A systematic approach to the 150 KNOWNBUGs would be super! Please do! |
|
I put it on my list. |
|
I do volunteer to sort out the ones in ansi-c. In fact I've just submitted the first PR #131 on those. |
smowton
pushed a commit
to smowton/cbmc
that referenced
this issue
May 9, 2018
…int_sett Implemented proper dump of taint sets
|
Also see #184 |
|
See also #208 |
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 11, 2021
Writing to an object that is composed of multiple fields is generally treated in a field-sensitive (and thus: single-field) manner, which had fixed several issues in handling shared arrays or structs. When the specific field being updated cannot be determined during symbolic execution (as is the case with non-const indices into arrays), we update all fields that make up the full object. Such a full-object update must then be treated as an atomic operation to avoid losing intermittent writes performed by other threads. Fixes: diffblue#123
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 15, 2021
Writing to an object that is composed of multiple fields is generally treated in a field-sensitive (and thus: single-field) manner, which had fixed several issues in handling shared arrays or structs. When the specific field being updated cannot be determined during symbolic execution (as is the case with non-const indices into arrays), we update all fields that make up the full object. Such a full-object update must then be treated as an atomic operation to avoid losing intermittent writes performed by other threads. Fixes: diffblue#123
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
May 14, 2021
Writing to an object that is composed of multiple fields is generally treated in a field-sensitive (and thus: single-field) manner, which had fixed several issues in handling shared arrays or structs. When the specific field being updated cannot be determined during symbolic execution (as is the case with non-const indices into arrays), we update all fields that make up the full object. Such a full-object update must then be treated as an atomic operation to avoid losing intermittent writes performed by other threads. Fixes: diffblue#123
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
May 14, 2021
Writing to an object that is composed of multiple fields is generally treated in a field-sensitive (and thus: single-field) manner, which had fixed several issues in handling shared arrays or structs. When the specific field being updated cannot be determined during symbolic execution (as is the case with non-const indices into arrays), we update all fields that make up the full object. Such a full-object update must then be treated as an atomic operation to avoid losing intermittent writes performed by other threads. Fixes: diffblue#123
3 tasks
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 26, 2022
Writing to an object that is composed of multiple fields is generally treated in a field-sensitive (and thus: single-field) manner, which had fixed several issues in handling shared arrays or structs. When the specific field being updated cannot be determined during symbolic execution (as is the case with non-const indices into arrays), we update all fields that make up the full object. Such a full-object update must then be treated as an atomic operation to avoid losing intermittent writes performed by other threads. Fixes: diffblue#123
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Oct 27, 2022
Writing to an object that is composed of multiple fields is generally treated in a field-sensitive (and thus: single-field) manner, which had fixed several issues in handling shared arrays or structs. When the specific field being updated cannot be determined during symbolic execution (as is the case with non-const indices into arrays), we update all fields that make up the full object. Such a full-object update must then be treated as an atomic operation to avoid losing intermittent writes performed by other threads. Fixes: diffblue#123
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Nov 20, 2022
Writing to an object that is composed of multiple fields is generally treated in a field-sensitive (and thus: single-field) manner, which had fixed several issues in handling shared arrays or structs. When the specific field being updated cannot be determined during symbolic execution (as is the case with non-const indices into arrays), we update all fields that make up the full object. Such a full-object update must then be treated as an atomic operation to avoid losing intermittent writes performed by other threads. Fixes: diffblue#123
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Nov 22, 2022
Writing to an object that is composed of multiple fields is generally treated in a field-sensitive (and thus: single-field) manner, which had fixed several issues in handling shared arrays or structs. When the specific field being updated cannot be determined during symbolic execution (as is the case with non-const indices into arrays), we update all fields that make up the full object. Such a full-object update must then be treated as an atomic operation to avoid losing intermittent writes performed by other threads. Fixes: diffblue#123
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Nov 22, 2022
Writing to an object that is composed of multiple fields is generally treated in a field-sensitive (and thus: single-field) manner, which had fixed several issues in handling shared arrays or structs. When the specific field being updated cannot be determined during symbolic execution (as is the case with non-const indices into arrays), we update all fields that make up the full object. Such a full-object update must then be treated as an atomic operation to avoid losing intermittent writes performed by other threads. Fixes: diffblue#123
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Nov 23, 2022
Writing to an object that is composed of multiple fields is generally treated in a field-sensitive (and thus: single-field) manner, which had fixed several issues in handling shared arrays or structs. When the specific field being updated cannot be determined during symbolic execution (as is the case with non-const indices into arrays), we update all fields that make up the full object. Such a full-object update must then be treated as an atomic operation to avoid losing intermittent writes performed by other threads. Fixes: diffblue#123
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 23, 2023
Writing to an object that is composed of multiple fields is generally treated in a field-sensitive (and thus: single-field) manner, which had fixed several issues in handling shared arrays or structs. When the specific field being updated cannot be determined during symbolic execution (as is the case with non-const indices into arrays), we update all fields that make up the full object. Such a full-object update must then be treated as an atomic operation to avoid losing intermittent writes performed by other threads. Fixes: diffblue#123
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
May 12, 2023
Writing to an object that is composed of multiple fields is generally treated in a field-sensitive (and thus: single-field) manner, which had fixed several issues in handling shared arrays or structs. When the specific field being updated cannot be determined during symbolic execution (as is the case with non-const indices into arrays), we update all fields that make up the full object. Such a full-object update must then be treated as an atomic operation to avoid losing intermittent writes performed by other threads. Fixes: diffblue#123
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
regression tests coming...
The text was updated successfully, but these errors were encountered: