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.

Sign up for GitHub

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

Jump to bottom

Improve provability of context predicate #664

Open
treiher opened this issue May 12, 2021 · 0 comments
Open

Improve provability of context predicate #664

treiher opened this issue May 12, 2021 · 0 comments
Assignees
@kanigsson
Labels
generator Related to generator package (SPARK code generation)
Projects
RecordFlux 2023-02-24

Comments

@treiher
Copy link
Collaborator

treiher commented May 12, 2021

The predicate of the context type gets very big for complex message specifications. It is very hard (or even impossible) for GNATprove to prove the predicate in certain circumstances. It should be possible to improve the provability by splitting the context predicate in smaller functions.
@treiher treiher added the generator Related to generator package (SPARK code generation) label May 12, 2021
@treiher treiher added this to To do in RecordFlux 0.7 via automation May 12, 2021
@senier senier added this to To do in RecordFlux 0.6 via automation Jan 13, 2022
@senier senier removed this from To do in RecordFlux 0.7 Jan 13, 2022
@senier senier mentioned this issue Jan 26, 2022
Closed
31 tasks
@kanigsson kanigsson moved this from To do to Implementation in RecordFlux 0.6 Feb 14, 2022
@kanigsson kanigsson moved this from Implementation to Design in RecordFlux 0.6 Feb 14, 2022
@kanigsson kanigsson self-assigned this Feb 14, 2022
@treiher treiher moved this from Design to To do in RecordFlux 0.6 Mar 25, 2022
@senier senier removed this from To do in RecordFlux 0.6 Aug 23, 2022
@senier senier added this to To do in RecordFlux Future via automation Aug 23, 2022
@senier senier removed this from To do in RecordFlux Future Aug 23, 2022
@senier senier added this to To do in RecordFlux 0.6 via automation Aug 23, 2022
@senier senier removed this from To do in RecordFlux 0.6 Aug 23, 2022
@senier senier added this to To do in RecordFlux Future via automation Aug 23, 2022
@senier senier removed this from Medium in RecordFlux Future Nov 1, 2022
@senier senier added this to To do in RecordFlux 0.8 via automation Nov 1, 2022
@senier senier moved this from To do to Implementation in RecordFlux 0.8 Nov 1, 2022
@senier senier removed this from Implementation in RecordFlux 0.8 Nov 29, 2022
@senier senier added this to To do in RecordFlux 2023-01-06 via automation Nov 29, 2022
@senier senier removed this from To do in RecordFlux 2023-01-06 Jan 3, 2023
@senier senier added this to To do in RecordFlux 2023-02-24 via automation Jan 3, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@kanigsson kanigsson

Labels
generator Related to generator package (SPARK code generation)
Projects
No open projects
RecordFlux 2023-02-24
To do
Milestone
No milestone
Development

No branches or pull requests
2 participants
@kanigsson @treiher