Merge branch 'feature/eva/builtins-type' into 'master'
[Eva] Checks consistency between the builtin type and the replaced C function Closes #671 See merge request frama-c/frama-c!2499
No related branches found
No related tags found
Showing
- src/kernel_services/plugin_entry_points/db.ml 2 additions, 1 deletionsrc/kernel_services/plugin_entry_points/db.ml
- src/kernel_services/plugin_entry_points/db.mli 22 additions, 17 deletionssrc/kernel_services/plugin_entry_points/db.mli
- src/plugins/e-acsl/tests/memory/oracle_ci/vla.res.oracle 1 addition, 1 deletionsrc/plugins/e-acsl/tests/memory/oracle_ci/vla.res.oracle
- src/plugins/value/domains/cvalue/builtins.ml 84 additions, 42 deletionssrc/plugins/value/domains/cvalue/builtins.ml
- src/plugins/value/domains/cvalue/builtins.mli 20 additions, 10 deletionssrc/plugins/value/domains/cvalue/builtins.mli
- src/plugins/value/domains/cvalue/builtins_float.ml 8 additions, 9 deletionssrc/plugins/value/domains/cvalue/builtins_float.ml
- src/plugins/value/domains/cvalue/builtins_malloc.ml 31 additions, 8 deletionssrc/plugins/value/domains/cvalue/builtins_malloc.ml
- src/plugins/value/engine/compute_functions.ml 1 addition, 2 deletionssrc/plugins/value/engine/compute_functions.ml
- src/plugins/value/engine/transfer_logic.ml 1 addition, 1 deletionsrc/plugins/value/engine/transfer_logic.ml
- src/plugins/value/engine/transfer_stmt.ml 1 addition, 1 deletionsrc/plugins/value/engine/transfer_stmt.ml
- src/plugins/value/legacy/eval_annots.ml 1 addition, 1 deletionsrc/plugins/value/legacy/eval_annots.ml
- src/plugins/value/register.ml 1 addition, 1 deletionsrc/plugins/value/register.ml
- src/plugins/value/value_parameters.ml 0 additions, 20 deletionssrc/plugins/value/value_parameters.ml
- src/plugins/value/value_parameters.mli 0 additions, 1 deletionsrc/plugins/value/value_parameters.mli
- tests/builtins/malloc-deps.c 4 additions, 4 deletionstests/builtins/malloc-deps.c
- tests/builtins/malloc-optimistic.c 2 additions, 2 deletionstests/builtins/malloc-optimistic.c
- tests/builtins/malloc.c 3 additions, 3 deletionstests/builtins/malloc.c
- tests/builtins/malloc_memexec.c 3 additions, 3 deletionstests/builtins/malloc_memexec.c
- tests/builtins/memexec-malloc.c 3 additions, 3 deletionstests/builtins/memexec-malloc.c
- tests/builtins/oracle/malloc-deps.res.oracle 43 additions, 43 deletionstests/builtins/oracle/malloc-deps.res.oracle
Loading
Please register or sign in to comment