Skip to content

Prover fails to complete #7

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

Closed
AdityaSenthilvel opened this issue Sep 16, 2024 · 2 comments
Closed

Prover fails to complete #7

AdityaSenthilvel opened this issue Sep 16, 2024 · 2 comments
Labels
bug Something isn't working general vcgen

Comments

@AdityaSenthilvel
Copy link

AdityaSenthilvel commented Sep 16, 2024

Facility PushDemo;
uses String_Theory;
Facility Integer_Stack_Fac is Stack_Template(Integer, 5)
realized by Array_Realiz;

Operation MyPush(preserves I: Integer; updates S: Stack);
  ensures (|#S| < 5 and S = <#I> o #S) or |#S| = 5 and S = #S;
Procedure
  Var J: Integer;
  J := I;
  If Depth(S) + 1 <= 5 then
    Push(J, S);
  end;
end;

Operation Main();
Procedure

end Main;

end;

Another example where the prover fails to complete:

@AdityaSenthilvel AdityaSenthilvel added bug Something isn't working general vcgen labels Sep 16, 2024
@AdityaSenthilvel
Copy link
Author

@rhit-fosswe
Copy link

Out of scope for our team (at least for now). Original ticket is from November 5, 2015. It has been updated since then, but it does not seem like the issue is officially fixed, as it is now part of the complete prover refactor.

@rhit-fosswe rhit-fosswe closed this as not planned Won't fix, can't repro, duplicate, stale Sep 27, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working general vcgen
Projects
None yet
Development

No branches or pull requests

2 participants