Skip to content

Drop OSEK support#736

Merged
michael-schwarz merged 12 commits intomasterfrom
rm_osek
May 13, 2022
Merged

Drop OSEK support#736
michael-schwarz merged 12 commits intomasterfrom
rm_osek

Conversation

@michael-schwarz
Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz commented May 12, 2022 •
edited
Loading

For reference, Goblint v1.1.1 still contains all the OSEK analyses, but we are removing them to ease the maintenance burden. Should you be interested in these OSEK analyses, feel free to reach out!

TODOs:

  • Remove interrupt edges
  • See what sort of hacks we can get rid of now

Closes #735

@michael-schwarz michael-schwarz added the cleanup Refactoring, clean-up label May 12, 2022
@michael-schwarz michael-schwarz added this to the v2.0.0 milestone May 12, 2022
@michael-schwarz michael-schwarz marked this pull request as ready for review May 12, 2022 13:22
@sim642 sim642 self-requested a review May 12, 2022 13:27
sim642
sim642 reviewed May 12, 2022
View reviewed changes
Copy link
Copy Markdown
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

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

There's also something in scripts/old/osek.

And I checked that postsub can finally be removed now! Disappointingly, presub is still used by ARINC.

sim642
sim642 reviewed May 12, 2022
View reviewed changes
sim642
sim642 reviewed May 12, 2022
View reviewed changes
sim642
sim642 approved these changes May 13, 2022
View reviewed changes
@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented May 13, 2022

And I checked that postsub can finally be removed now!

Should we do this here or save it for another PR?

@sim642
Copy link
Copy Markdown
Member

sim642 commented May 13, 2022

Should we do this here or save it for another PR?

Maybe separate, because I think we could actually get rid of presub's only usages in ARINC as well. There it's just being used to get the context of base analysis (only!) and compute its hash. One possibility might be to even compute the hash of ctx.control_context instead, which would also account for other analyses. It's an easy change to make, but should probably be tested, since it could also completely break ARINC support (if it isn't already).
Or the safer alternative would be a query instead, which works because queries are answered on the pre-state anyway.

If we manage that, then the whole idea of topological sorting of analyses and not having dependency cycles becomes unnecessary (they had to be sorted for postsub to be able to access the post-state of dependent analyses). AFAIK we somewhere currently omit declaring a dependency, because it would cause a cycle, but we actually have a dependency that another analysis answers some query. With joint-querying it's not really necessary to order the analyses.

@michael-schwarz michael-schwarz merged commit 001855b into master May 13, 2022
@michael-schwarz michael-schwarz deleted the rm_osek branch May 13, 2022 14:25
sim642 added a commit that referenced this pull request Jul 20, 2022
@sim642
Remove ppx_distr_guards dependency
4f57a8d 
Unused since the removal of FlagModes in #736.
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
@sim642
[new release] goblint (2.0.0)
6efdfdf 
CHANGES:

Goblint "lean" release after a lot of cleanup.

* Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474).
* Add interactive analysis (goblint/analyzer#391).
* Add server mode (goblint/analyzer#522).
* Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448).
* Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419).
* Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722).
* Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595).
* Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655).
* Add pthread extraction to Promela (goblint/analyzer#220).
* Add location spans to output (goblint/analyzer#428, goblint/analyzer#449).
* Improve race reporting (goblint/analyzer#550, goblint/analyzer#551).
* Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785).
* Refactor warnings (goblint/analyzer#55, goblint/analyzer#783).
* Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499).
* Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675).
* Add bash completion (goblint/analyzer#669).
* Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).
@sim642 sim642 mentioned this pull request Aug 18, 2022
Merged
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
@sim642
[new release] goblint (2.0.0)
1c281d5 
CHANGES:

Goblint "lean" release after a lot of cleanup.

* Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474).
* Add interactive analysis (goblint/analyzer#391).
* Add server mode (goblint/analyzer#522).
* Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448).
* Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419).
* Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722).
* Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595).
* Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655).
* Add pthread extraction to Promela (goblint/analyzer#220).
* Add location spans to output (goblint/analyzer#428, goblint/analyzer#449).
* Improve race reporting (goblint/analyzer#550, goblint/analyzer#551).
* Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785).
* Refactor warnings (goblint/analyzer#55, goblint/analyzer#783).
* Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499).
* Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675).
* Add bash completion (goblint/analyzer#669).
* Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).
@sim642 sim642 mentioned this pull request Aug 2, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sim642 sim642 sim642 approved these changes

Assignees

No one assigned

Labels

cleanup Refactoring, clean-up

Projects

None yet

Milestone

v2.0.0

Development

Successfully merging this pull request may close these issues.

Remove OSEK analyses

2 participants

@michael-schwarz @sim642