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

Incorrect detection of possibly empty array field #375

Closed
treiher opened this issue Jul 29, 2020 · 0 comments · Fixed by #376
Closed

Incorrect detection of possibly empty array field #375

treiher opened this issue Jul 29, 2020 · 0 comments · Fixed by #376
Assignees
@treiher
Labels
bug generator Related to generator package (SPARK code generation)
Projects
RecordFlux 0.5

Comments

@treiher
Copy link
Collaborator

treiher commented Jul 29, 2020

If an array field X is not reachable on all paths, X is detected as possibly empty even if this can never be the case. This leads to the generation of a Set_X_Empty function with an precondition which can never be fulfilled. gnatprove detects this issue and returns a precondition is always False warning.
@treiher treiher added bug generator Related to generator package (SPARK code generation) labels Jul 29, 2020
@treiher treiher added this to To do in RecordFlux 0.5 via automation Jul 29, 2020
@treiher treiher self-assigned this Jul 29, 2020
@treiher treiher moved this from To do to In progress in RecordFlux 0.5 Jul 29, 2020
@treiher treiher moved this from In progress to Ready in RecordFlux 0.5 Jul 29, 2020
treiher added a commit that referenced this issue Jul 29, 2020
@treiher
Fix incorrect detection of possibly empty array fields
f3e1d12 
Ref. #375
@treiher treiher mentioned this issue Jul 29, 2020
Merged
treiher added a commit that referenced this issue Jul 29, 2020
@treiher
Fix incorrect detection of possibly empty array fields
d081e78 
Ref. #375
RecordFlux 0.5 automation moved this from Ready to Merged Jul 29, 2020
treiher added a commit that referenced this issue Jul 29, 2020
@treiher
Fix incorrect detection of possibly empty array fields
023586d 
Ref. #375
@treiher treiher mentioned this issue Aug 4, 2021
Closed
9 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@treiher treiher

Labels
bug generator Related to generator package (SPARK code generation)
Projects
No open projects
RecordFlux 0.5
  
Merged
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Issue 375: Fix incorrect detection of possibly empty array fields AdaCore/RecordFlux
1 participant
@treiher