Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Drop OSEK support #736

Merged
merged 12 commits into from
May 13, 2022
Merged

Drop OSEK support #736

merged 12 commits into from
May 13, 2022

Conversation

michael-schwarz
Copy link
Member

@michael-schwarz michael-schwarz commented May 12, 2022

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
Copy link
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.

@michael-schwarz
Copy link
Member Author

And I checked that postsub can finally be removed now!

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

@sim642
Copy link
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
Unused since the removal of FlagModes in #736.
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
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 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
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).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
cleanup Refactoring, clean-up
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Remove OSEK analyses
2 participants