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

Add unit tests for empty sets in test_z3_visitor.py #1063

Open
Raine-Yang-UofT opened this issue Jul 9, 2024 · 0 comments
Open

Add unit tests for empty sets in test_z3_visitor.py #1063

Raine-Yang-UofT opened this issue Jul 9, 2024 · 0 comments

Comments

@Raine-Yang-UofT
Copy link
Contributor

Currently, the test cases for parsing list/set/tuple and in/not in operators to Z3 constraints only include tests for empty lists and tuples, but not sets. This is because the only way to represent an empty set in function preconditions is to use the set() function (since {} represents an empty dictionary). However, the parse_assertion function in contracts/__init__.py, which converts precondition docstrings to Python expressions, cannot infer the return value of set(). As a result, ExprWrapper, the class that converts function preconditions to Z3 expressions, skips preconditions that involve empty sets.

Proposed solution:

  1. Enhance parse_assertion Function:

Modify the parse_assertion function to correctly infer the set() function as an empty set.

  1. Add Unit Tests:

Update the container_list and container_expected lists in tests/test_z3_visitor.py to include the following test cases:

# Add to container_list:
    """
    def in_empty_set(x: int):
        '''
        Preconditions:
            - x in set()
        '''
        pass
    """,
    """
    def not_in_empty_set(x: int):
        '''
        Preconditions:
            - x not in set()
        '''
        pass
    """,

# Add to container_expected:
    [z3.BoolVal(False)],
    [z3.BoolVal(True)],
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

No branches or pull requests

1 participant