From 7b8658fa48ae19f4af6472f99aaa1c547ef2a365 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Sun, 3 Nov 2024 20:17:17 -0500 Subject: [PATCH] test: add example test cases for redundant_assignment and missing_return z3 options --- .../z3_option/z3_e9959_redundant_assignment.py | 9 +++++++++ .../z3_option/z3_r9711_missing_return_statement.py | 8 ++++++++ 2 files changed, 17 insertions(+) create mode 100644 examples/custom_checkers/z3_option/z3_e9959_redundant_assignment.py create mode 100644 examples/custom_checkers/z3_option/z3_r9711_missing_return_statement.py diff --git a/examples/custom_checkers/z3_option/z3_e9959_redundant_assignment.py b/examples/custom_checkers/z3_option/z3_e9959_redundant_assignment.py new file mode 100644 index 000000000..2d343a325 --- /dev/null +++ b/examples/custom_checkers/z3_option/z3_e9959_redundant_assignment.py @@ -0,0 +1,9 @@ +def func(x: int) -> int: + ''' + Preconditions: + - x > 10 + ''' + a = 10 + if x > 0: # by function precondition, this condition is True + a = 20 # `a` is reassigned before first use + return a diff --git a/examples/custom_checkers/z3_option/z3_r9711_missing_return_statement.py b/examples/custom_checkers/z3_option/z3_r9711_missing_return_statement.py new file mode 100644 index 000000000..73b18aa8d --- /dev/null +++ b/examples/custom_checkers/z3_option/z3_r9711_missing_return_statement.py @@ -0,0 +1,8 @@ +def func(x: int) -> int: + ''' + Preconditions: + - x in [1, 2, 3, 4, 5] + ''' + if x > 5: + return x + print(x)