Skip to content

Prepare CIL for concurrency#180

Merged
arkocal merged 9 commits intogoblint:developfrom
arkocal:develop
Apr 8, 2025
Merged

Prepare CIL for concurrency#180
arkocal merged 9 commits intogoblint:developfrom
arkocal:develop

Conversation

@arkocal
Copy link
Copy Markdown

@arkocal arkocal commented Mar 11, 2025

Replace references with DLS to enable multiple domains.

@arkocal arkocal changed the title Prepare CIL for concurrency DRAFT: Prepare CIL for concurrency Mar 11, 2025
@arkocal arkocal marked this pull request as draft March 11, 2025 12:24
@michael-schwarz
Copy link
Copy Markdown
Member

Strange, it seems it builds but the CI tests still fail for OCaml <5.0?

(For debugging, the note on how to run a single test under dune from the README may be helpful here.)

@arkocal
Copy link
Copy Markdown
Author

arkocal commented Mar 12, 2025

Strange, it seems it builds but the CI tests still fail for OCaml <5.0?

(For debugging, the note on how to run a single test under dune from the README may be helpful here.)

I have tried, but could not find a solution yet.

Considering that older versions dont even build (due to dependencies) it might also make sense to drop domain_shims and keep this for an OCaml 5 Version in the future.

By adapting test script to use domain_shims (like in 13fc020)
@arkocal arkocal marked this pull request as ready for review March 20, 2025 14:53
string *)
(d: doc) =
let aligns: int list ref = ref [0] in (* A stack of alignment columns *)
let aligns: int list refDLS = refDLS [0] in (* A stack of alignment columns *)
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm confused about this one. This is a local reference, but there's also a global one with the same name. How are these related?
By defining aligns locally, this function has no access to the global one, so it seems like this could be just a ref still. Or am I missing something?

aligns := res :: !aligns;
res.deltaFromPrev := abscol - !topAlignAbsCol;
topAlignAbsCol := abscol
DLS.set aligns (res :: (DLS.get aligns));
Copy link
Copy Markdown
Member

@sim642 sim642 Mar 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's lots of unnecessary parentheses around DLS.get now all over this file.

@sim642 sim642 changed the title DRAFT: Prepare CIL for concurrency Prepare CIL for concurrency Mar 26, 2025
@sim642 sim642 added this to the 2.1.0 milestone Mar 26, 2025
@arkocal arkocal merged commit 9180125 into goblint:develop Apr 8, 2025
13 checks passed
sim642 added a commit to sim642/opam-repository that referenced this pull request Sep 2, 2025
CHANGES:

* Add `_Float16` type support (goblint/cil#190, goblint/cil#193).
* Add C23 `alignof` and `alignas` support (goblint/cil#189, goblint/cil#191).
* Add initializer support for anonymous struct in union (goblint/cil#176, goblint/cil#184).
* Fix enumerator printing (goblint/cil#185).
* Remove global state from `Pretty` (goblint/cil#187).
* Remove OCaml <4.12 support (goblint/cil#180, goblint/cil#181).
* Use `gnu11` standard in most tests (goblint/cil#188, goblint/cil#192).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants