-
Notifications
You must be signed in to change notification settings - Fork 1
Issue 3: HTTP/2 #8
Conversation
Currently, the compilability of the generated code is not tested correctly (#9). That's why the failing compilation for the current HTTP/2 specification is not detected (AdaCore/RecordFlux#500). The issue was introduced by the message size invariant in ffb015f. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The changes look fine so far, but three comments of the last review still need some action. Also the feature branch should be rebased to the current main
.
The tests are now failing. Is that related to #8 (comment)? It does not happen if i check the spec locally. |
Yes, the verification of the specification works fine, but the generated SPARK code is not correct. I will look into that issue in the course of the day. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Issue AdaCore/RecordFlux#500 is fixed now, the CI checks should not fail anymore. After fixing my small remarks about comments and rebasing to main
this PR should be ready to merge.
Rebased onto main, but there seems to be a problem in the tests with the newly added |
It seems there is a name conflict in the generated code. Such issues should be detected during model verification. Please create an issue for RecordFlux, preferably with a small reproducer. |
LGTM. The branch still needs to be rebased. |
Ref. #3