[Eva] fix str builtins for negative offsets
Each call to fold_itv must be preceded by a check of the actual validity of the offsets (since fold_itv will take the intersection). In the case of an exact offset, the right side is already taken into account, so we only have to check the left (negative) bounds.
Showing
- src/plugins/value/domains/cvalue/builtins_string.ml 34 additions, 19 deletionssrc/plugins/value/domains/cvalue/builtins_string.ml
- tests/non-free/oracle/strlen.res.oracle 79 additions, 12 deletionstests/non-free/oracle/strlen.res.oracle
- tests/non-free/oracle/strnlen2.res.oracle 84 additions, 17 deletionstests/non-free/oracle/strnlen2.res.oracle
- tests/non-free/strlen.c 26 additions, 0 deletionstests/non-free/strlen.c
- tests/non-free/strnlen2.c 26 additions, 0 deletionstests/non-free/strnlen2.c
Loading
Please register or sign in to comment