python-by-contract-corpus icon indicating copy to clipboard operation
python-by-contract-corpus copied to clipboard

Contract counterexamples detected by CrossHair

Open pschanely opened this issue 3 years ago • 0 comments

I've found 30 contract counterexamples via CrossHair in the correct solutions. They appear to be largely missing preconditions. Some may result from inconsistent expectations between CrossHair and icontract (especially perhaps when it comes to exceptions?) Anyway, let's review these at some point and decide whether we want to make changes. Note that it's useful to backport any changes to the recorded failures as well, because we want those files to only contain one bug in each.

Running crosshair on: /Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_11_seating_system.py
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_11_seating_system.py:166: error: PreconditionFailed: Precondition "len(table) > 0
    and len(table[0]) > 0
    and all(
        len(row) == len(table[0])
        for row in table
    )" was not satisfied before calling "__init__" when calling parse_layout([])
Return code: 1

Running crosshair on: /Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_18_operation_order.py
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_18_operation_order.py:104: error: RecursionError: maximum recursion depth exceeded in comparison when calling serialize(Node(head=Node(head=Node(head=0, tail=[]), tail=[Tail(op=<Operation.MUL: '*'>, right=Node(head=Node(head=Node(head=Node(head=Node(head=0, tail=[]), tail=[Tail(op=<Operation.ADD: '+'>, right=Node(head=Node(head=Node(head=0, tail=[Tail(op=<Operation.MUL: '*'>, right=Node(head=Node(head=Node(head=Node(head=Node(head=0, tail=[]), tail=[..., Tail(op=<Operation.MUL: '*'>, right=Node(head=0, tail=[]))]), tail=[]), tail=[]), tail=[Tail(op=<Operation.MUL: '*'>, right=0)]))]), tail=[]), tail=[])), Tail(op=<Operation.MUL: '*'>, right=Node(head=0, tail=[]))]), tail=[]), tail=[]), tail=[Tail(op=<Operation.MUL: '*'>, right=0)]))]), tail=[]))
Return code: 1

Running crosshair on: /Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_19_monster_messages.py
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_19_monster_messages.py:74: error: "lambda text, result:" yields false when calling match(<python_by_contract_corpus.correct.aoc2020.day_19_monster_messages.RuleSequence object at 0x7fe033d9bd00>, '') (which returns '')
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_19_monster_messages.py:96: error: "lambda text, result:" yields false when calling match(<python_by_contract_corpus.correct.aoc2020.day_19_monster_messages.RuleLiteral object at 0x7fe0309bd3c0>, '') (which returns '')
Return code: 1

Running crosshair on: /Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_22_crab_combat.py
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_22_crab_combat.py:194: error: ValueError: invalid literal for int() with base 10: 'Player 1:' when calling parse_lines(['Player 1:', 'Player 1:', 'Player 2:', ''])
Return code: 1

Running crosshair on: /Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_5_binary_boarding.py
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_5_binary_boarding.py:38: error: false when calling apply(0, 5, 'R') (which returns (3, 5))
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_5_binary_boarding.py:43: error: false when calling apply(0, 5, 'F') (which returns (0, 2))
Return code: 1

Running crosshair on: /Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_7_handy_haversacks.py
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_7_handy_haversacks.py:31: error: ValueError: not enough values to unpack (expected 2, got 1) when calling parse_rule('')
Return code: 1

Running crosshair on: /Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_9_encoding_error.py
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/aoc2020/day_9_encoding_error.py:12: error: false when calling solve([0, 0, 0], -1) (which returns (-1, 0))
Return code: 1

Running crosshair on: /Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_03/problem_04.py
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_03/problem_04.py:54: error: KeyError: '' when calling decode('')
Return code: 1

Running crosshair on: /Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_05/problem_03.py
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_05/problem_03.py:95: error: false when calling __new__('', -1, 0.0, 1.0, True, True) (which returns [[-inf, 0.0), [1.0, inf)])
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_05/problem_03.py:103: error: Error while evaluating post condition: IndexError: list index out of range when calling __new__(0, -1, 0.0, 1.0, False, False) (which returns [])
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_05/problem_03.py:108: error: Error while evaluating post condition: IndexError: list index out of range when calling __new__(0, -1, 0.0, 1.0, False, False) (which returns [])
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_05/problem_03.py:113: error: false when calling __new__(0, -1, 0.0, 1.0, False, False) (which returns [])
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_05/problem_03.py:118: error: false when calling __new__('', -1, 0.0, 1.0, False, True) (which returns [[1.0, inf)])
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_05/problem_03.py:123: error: false when calling __new__(0, -1, 0.0, 1.0, True, False) (which returns [[-inf, 0.0)])
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_05/problem_03.py:128: error: false when calling __new__('', -1, 0.0, 1.0, True, True) (which returns [[-inf, 0.0), [1.0, inf)])
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_05/problem_03.py:202: error: false when calling bin_index([[-1.0, 0.0)], 0.0) (which returns -1)
Return code: 1

Running crosshair on: /Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_09/problem_03.py
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_09/problem_03.py:158: error: ValueError: Unexpected unfinished block: 
 when calling parse(('', ''))
Return code: 1

Running crosshair on: /Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_11/problem_02.py
/Users/pschanely/proj/python-by-contract-corpus/python_by_contract_corpus/correct/ethz_eprog_2019/exercise_11/problem_02.py:180: error: SyntaxError: Unparsable source code: 

pschanely avatar Jun 07 '22 20:06 pschanely