Default the value of CilType.Location.Byte
to -1 if missing in JSON
#1563
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.
While refactoring some GobPie's classes to records, I accidentally removed a seemingly unused field
from the
GoblintLocation
class.This made Goblint crash when using breakpoints for which the requests are done using
Location
.Instead of putting the field back into GobPie, we decided to fix it in Goblint, as the
of_yojson
of a location is anyways only used by GobPie.