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

Update rang_big() precondition #33

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Update rang_big() precondition #33

wants to merge 1 commit into from

Conversation

zjma
Copy link
Collaborator

@zjma zjma commented Mar 5, 2025

Description

Update the invariant of a test-only function rand_big.

What is the change being pushed?

rand_big() was commented to take a non-negative x as input,
while it should assume x is a positive integer.
Calling this out in the function comment.

Why are you pushing this change?

The current comment is misleading.

How is this implemented?

Comments are updated.

Type of Change

Tiny refactoring.

Checklist

  • I have performed a self-review of my own code
  • I have commented my code, particularly in hard-to-understand areas
  • I identified and added all keyless stakeholders and component owners affected by this change as reviewers
  • I tested both happy and unhappy path of the functionality
  • I have made corresponding changes to the documentation

@zjma zjma changed the title Update rang_big() invariant Update rang_big() precondition Mar 5, 2025
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