Merge branch 'fix/eva/offsetmap' into 'master'
[Eva] Fixes unsoundness in offsetmaps, and imprecision in memset builtin See merge request frama-c/frama-c!4640
No related branches found
No related tags found
Showing
- src/kernel_services/abstract_interp/offsetmap.ml 32 additions, 12 deletionssrc/kernel_services/abstract_interp/offsetmap.ml
- src/plugins/eva/domains/cvalue/builtins_memory.ml 54 additions, 34 deletionssrc/plugins/eva/domains/cvalue/builtins_memory.ml
- tests/builtins/memset.c 22 additions, 1 deletiontests/builtins/memset.c
- tests/builtins/oracle/memset.res.oracle 134 additions, 16 deletionstests/builtins/oracle/memset.res.oracle
- tests/value/offsetmap.i 36 additions, 2 deletionstests/value/offsetmap.i
- tests/value/oracle/offsetmap.0.res.oracle 50 additions, 4 deletionstests/value/oracle/offsetmap.0.res.oracle
- tests/value/oracle/offsetmap.1.res.oracle 50 additions, 10 deletionstests/value/oracle/offsetmap.1.res.oracle
- tests/value/oracle/offsetmap.2.res.oracle 237 additions, 0 deletionstests/value/oracle/offsetmap.2.res.oracle
- tests/value/oracle/struct2.res.oracle 2 additions, 1 deletiontests/value/oracle/struct2.res.oracle
- tests/value/oracle_apron/offsetmap.0.res.oracle 4 additions, 4 deletionstests/value/oracle_apron/offsetmap.0.res.oracle
- tests/value/oracle_apron/offsetmap.1.res.oracle 8 additions, 10 deletionstests/value/oracle_apron/offsetmap.1.res.oracle
- tests/value/oracle_apron/offsetmap.2.res.oracle 22 additions, 0 deletionstests/value/oracle_apron/offsetmap.2.res.oracle
- tests/value/oracle_equality/offsetmap.2.res.oracle 4 additions, 0 deletionstests/value/oracle_equality/offsetmap.2.res.oracle
- tests/value/oracle_equality/struct2.res.oracle 6 additions, 6 deletionstests/value/oracle_equality/struct2.res.oracle
- tests/value/oracle_multidim/struct2.res.oracle 3 additions, 3 deletionstests/value/oracle_multidim/struct2.res.oracle
- tests/value/oracle_octagon/offsetmap.2.res.oracle 4 additions, 0 deletionstests/value/oracle_octagon/offsetmap.2.res.oracle
- tests/value/oracle_symblocs/offsetmap.2.res.oracle 4 additions, 0 deletionstests/value/oracle_symblocs/offsetmap.2.res.oracle
- tests/value/oracle_symblocs/struct2.res.oracle 6 additions, 6 deletionstests/value/oracle_symblocs/struct2.res.oracle
Loading
Please register or sign in to comment