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

order of annotations is now preserved almost #618

Merged
merged 1 commit into from
Mar 25, 2021

Conversation

petravandenbos-utwente
Copy link
Contributor

@petravandenbos-utwente petravandenbos-utwente commented Mar 25, 2021

Since merge 07d831b a contract is printed as follows:

  • Select all context annotations: i.e. the annotations occurring in the pre- and post-condition of a contract.
  • Print all non-context pre-condition annotations
  • Print all context annotations.
  • Print all post-condition annotations

Problem:
Annotations are printed in an order such that VerCors cannot verify the contract anymore, e.g. it prints a contract:
requires a == 1;
context Perm(a,1\2);

Solution:
This pull-request works in almost all cases, except for contrived contracts as shown in issue #619

@petravandenbos-utwente petravandenbos-utwente temporarily deployed to Default March 25, 2021 16:09 Inactive
@sonarcloud
Copy link

sonarcloud bot commented Mar 25, 2021

Kudos, SonarCloud Quality Gate passed!

Bug A 0 Bugs
Vulnerability A 0 Vulnerabilities
Security Hotspot A 0 Security Hotspots
Code Smell A 0 Code Smells

0.0% 0.0% Coverage
0.0% 0.0% Duplication

@petravandenbos-utwente petravandenbos-utwente changed the title order of annotations is now preserved order of annotations is now preserved almost Mar 25, 2021
@petravandenbos-utwente petravandenbos-utwente deleted the some-printer-fixes branch March 25, 2021 16:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants