[e-acsl] undefine comparison for derivatives of Misc.Id_term
Make Pred_or_term depend on Misc.Term_id instead of Cil_datatype.Term. This should have been the case all along, since Pred_or_term is used in contexts where the physical identity of terms matter. They might be typed differently depending on contexts (cast or no cast) and thus require different translations. Then we undefine the comparison function for both modules which depend on Misc.Id_term, since there is no meaningful comparison for physical equality.
Showing
- src/plugins/e-acsl/src/libraries/analyses_datatype.ml 27 additions, 46 deletionssrc/plugins/e-acsl/src/libraries/analyses_datatype.ml
- src/plugins/e-acsl/src/libraries/analyses_datatype.mli 4 additions, 0 deletionssrc/plugins/e-acsl/src/libraries/analyses_datatype.mli
- src/plugins/e-acsl/tests/arith/oracle/at.res.oracle 6 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/at.res.oracle
- src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle 4 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
- src/plugins/e-acsl/tests/arith/oracle/gen_at.c 134 additions, 89 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_at.c
- src/plugins/e-acsl/tests/arith/oracle/gen_functions.c 122 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_functions.c
- src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c 29 additions, 22 deletionssrc/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
- src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c 42 additions, 34 deletionssrc/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
- src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c 16 additions, 11 deletionssrc/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
- src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c 5 additions, 2 deletionssrc/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
- src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c 5 additions, 2 deletionssrc/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
- src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c 5 additions, 2 deletionssrc/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
- src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c 5 additions, 2 deletionssrc/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
- src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c 16 additions, 8 deletions...ns/e-acsl/tests/constructs/oracle/gen_function_contract.c
- src/plugins/e-acsl/tests/constructs/oracle/gen_result.c 8 additions, 6 deletionssrc/plugins/e-acsl/tests/constructs/oracle/gen_result.c
- src/plugins/e-acsl/tests/constructs/oracle/result.res.oracle 2 additions, 2 deletionssrc/plugins/e-acsl/tests/constructs/oracle/result.res.oracle
- src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c 5 additions, 2 deletionssrc/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
- src/plugins/e-acsl/tests/libc/oracle/gen_str.c 33 additions, 15 deletionssrc/plugins/e-acsl/tests/libc/oracle/gen_str.c
- src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c 4 additions, 0 deletionssrc/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
- src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c 4 additions, 2 deletions...lugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
Loading
Please register or sign in to comment