[typing] Fixed long-standing issue with contract over last return of function
Block and goto were not properly created, leading to potential issue with an `ensures \false` contract for such statement, since we are transforming a return into a fall-through (hence subject to `ensures`) statement
Showing
- src/kernel_internals/typing/oneret.ml 24 additions, 30 deletionssrc/kernel_internals/typing/oneret.ml
- src/plugins/aorai/tests/aorai/oracle/test_recursion2.0.res.oracle 4 additions, 4 deletions...ins/aorai/tests/aorai/oracle/test_recursion2.0.res.oracle
- src/plugins/aorai/tests/aorai/oracle/test_recursion2.1.res.oracle 4 additions, 4 deletions...ins/aorai/tests/aorai/oracle/test_recursion2.1.res.oracle
- tests/impact/oracle/alias.res.oracle 1 addition, 1 deletiontests/impact/oracle/alias.res.oracle
- tests/impact/oracle/depend3.res.oracle 1 addition, 1 deletiontests/impact/oracle/depend3.res.oracle
- tests/libc/oracle/fc_libc.0.res.oracle 1 addition, 1 deletiontests/libc/oracle/fc_libc.0.res.oracle
- tests/metrics/oracle/func_ptr.0.res.oracle 3 additions, 3 deletionstests/metrics/oracle/func_ptr.0.res.oracle
- tests/metrics/oracle/func_ptr.1.res.oracle 1 addition, 1 deletiontests/metrics/oracle/func_ptr.1.res.oracle
- tests/metrics/oracle/reach.res.oracle 4 additions, 4 deletionstests/metrics/oracle/reach.res.oracle
- tests/metrics/oracle/unreachable.res.oracle 3 additions, 3 deletionstests/metrics/oracle/unreachable.res.oracle
- tests/pdg/oracle/pb_infinite_loop.2.res.oracle 21 additions, 11 deletionstests/pdg/oracle/pb_infinite_loop.2.res.oracle
- tests/pdg/oracle/simple_intra_slice.res.oracle 425 additions, 415 deletionstests/pdg/oracle/simple_intra_slice.res.oracle
- tests/slicing/oracle/csmith.1.res.oracle 46 additions, 22 deletionstests/slicing/oracle/csmith.1.res.oracle
- tests/slicing/oracle/csmith.2.res.oracle 21 additions, 10 deletionstests/slicing/oracle/csmith.2.res.oracle
- tests/slicing/oracle/simple_intra_slice.res.oracle 35 additions, 18 deletionstests/slicing/oracle/simple_intra_slice.res.oracle
- tests/slicing/oracle/slice_no_body.res.oracle 4 additions, 0 deletionstests/slicing/oracle/slice_no_body.res.oracle
- tests/spec/oracle/stmt_contract.res.oracle 7 additions, 2 deletionstests/spec/oracle/stmt_contract.res.oracle
- tests/syntax/oracle/unroll_labels.0.res.oracle 26 additions, 26 deletionstests/syntax/oracle/unroll_labels.0.res.oracle
- tests/syntax/oracle/unroll_labels.1.res.oracle 26 additions, 26 deletionstests/syntax/oracle/unroll_labels.1.res.oracle
Loading
Please register or sign in to comment