Merge branch 'feature/eva/valid-string-reduction' into 'master'
[Eva] Reduction on ACSL valid_string and valid_read_string predicates See merge request frama-c/frama-c!4536
Showing
- src/plugins/eva/engine/compute_functions.ml 4 additions, 5 deletionssrc/plugins/eva/engine/compute_functions.ml
- src/plugins/eva/engine/transfer_stmt.ml 2 additions, 11 deletionssrc/plugins/eva/engine/transfer_stmt.ml
- src/plugins/eva/engine/transfer_stmt.mli 0 additions, 1 deletionsrc/plugins/eva/engine/transfer_stmt.mli
- src/plugins/eva/legacy/eval_op.ml 16 additions, 10 deletionssrc/plugins/eva/legacy/eval_op.ml
- src/plugins/eva/legacy/eval_terms.ml 100 additions, 88 deletionssrc/plugins/eva/legacy/eval_terms.ml
- tests/builtins/oracle/strchr.res.oracle 47 additions, 46 deletionstests/builtins/oracle/strchr.res.oracle
- tests/builtins/oracle/strlen.res.oracle 1 addition, 1 deletiontests/builtins/oracle/strlen.res.oracle
- tests/builtins/oracle/strnlen2.res.oracle 1 addition, 1 deletiontests/builtins/oracle/strnlen2.res.oracle
- tests/builtins/oracle/wcslen.res.oracle 2 additions, 3 deletionstests/builtins/oracle/wcslen.res.oracle
- tests/builtins/strchr.c 4 additions, 2 deletionstests/builtins/strchr.c
- tests/libc/oracle/libgen_h.res.oracle 2 additions, 2 deletionstests/libc/oracle/libgen_h.res.oracle
- tests/libc/oracle/stdlib_c_env.res.oracle 1 addition, 7 deletionstests/libc/oracle/stdlib_c_env.res.oracle
- tests/value/oracle/reduce_by_valid.res.oracle 1 addition, 1 deletiontests/value/oracle/reduce_by_valid.res.oracle
- tests/value/oracle/strings_logic.res.oracle 282 additions, 0 deletionstests/value/oracle/strings_logic.res.oracle
- tests/value/oracle/summary.4.res.oracle 1 addition, 5 deletionstests/value/oracle/summary.4.res.oracle
- tests/value/oracle_multidim/strings_logic.res.oracle 8 additions, 0 deletionstests/value/oracle_multidim/strings_logic.res.oracle
- tests/value/strings_logic.c 211 additions, 0 deletionstests/value/strings_logic.c
Loading
Please register or sign in to comment