Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Feb 28, 2023

Previously when using d_plaintype (or any other plain printing which includes the type) twice in a row on a recursive struct, the first output has TComp outside and TCompLoop on the fields:

TPtr(TComp(struct __pthread_internal_list,
              __prev : TPtr(TCompLoop(struct __pthread_internal_list, _, ), ),
              __next : TPtr(TCompLoop(struct __pthread_internal_list, _, ), ), ,
        ), )

Due to the statefulness of the plain printer, a second call with exactly the same type already has TCompLoop outside:

TPtr(TCompLoop(struct __pthread_internal_list, _, ), )

This is annoying for incremental analysis in Goblint, where messages will differ only in this aspect because the incremental run will skip over some earlier evaluation that made the first call, moving the first call with the different output to a different place. It shows spurious differences in messagesCompare.

By removing the compinfo after recursing, the plain printer becomes functionally pure, so all calls consistently print the first output from above.

@sim642 sim642 added the bug label Feb 28, 2023
@sim642 sim642 added this to the 2.0.2 milestone Apr 5, 2023
@sim642 sim642 requested a review from michael-schwarz May 2, 2023 12:55
@sim642 sim642 merged commit 4d70d89 into develop May 8, 2023
@sim642 sim642 deleted the tcomploop branch May 8, 2023 07:30
sim642 added a commit to sim642/opam-repository that referenced this pull request Sep 11, 2023
CHANGES:

* Rename `Rmtmps` to `RmUnused` (goblint/cil#135).
* Add option to add return statement to `noreturn` functions (goblint/cil#129).
* Fix empty `if`s being removed (goblint/cil#140).
* Fix `_Float128` support (goblint/cil#118, goblint/cil#119).
* Fix C11 `_Alignas` computation (goblint/cil#130).
* Fix renaming and merging of `inline` functions based on C standard (goblint/cil#120, goblint/cil#124).
* Fix `Pretty` not resetting all global state between calls (goblint/cil#133, goblint/cil#134).
* Fix `fundec` location in merger (goblint/cil#139).
* Fix `cilly` patcher (goblint/cil#128).
* Disable basename by default in parser.
nberth pushed a commit to nberth/opam-repository that referenced this pull request Jun 18, 2024
CHANGES:

* Rename `Rmtmps` to `RmUnused` (goblint/cil#135).
* Add option to add return statement to `noreturn` functions (goblint/cil#129).
* Fix empty `if`s being removed (goblint/cil#140).
* Fix `_Float128` support (goblint/cil#118, goblint/cil#119).
* Fix C11 `_Alignas` computation (goblint/cil#130).
* Fix renaming and merging of `inline` functions based on C standard (goblint/cil#120, goblint/cil#124).
* Fix `Pretty` not resetting all global state between calls (goblint/cil#133, goblint/cil#134).
* Fix `fundec` location in merger (goblint/cil#139).
* Fix `cilly` patcher (goblint/cil#128).
* Disable basename by default in parser.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants