[kernel] Better casts introduction
- always remove FC's internal attribute everywhere before deciding whether a cast is needed. - ACSL and C decisions to cast are similar - only unroll type for checking equality. If a cast is needed, keep typedef (if any) as target
Showing
- src/kernel_internals/typing/cabs2cil.ml 14 additions, 16 deletionssrc/kernel_internals/typing/cabs2cil.ml
- src/kernel_services/ast_queries/cil.ml 14 additions, 19 deletionssrc/kernel_services/ast_queries/cil.ml
- src/kernel_services/ast_queries/logic_utils.ml 9 additions, 7 deletionssrc/kernel_services/ast_queries/logic_utils.ml
- src/plugins/e-acsl/tests/arith/oracle/gen_arith.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_arith.c
- src/plugins/e-acsl/tests/arith/oracle/gen_array.c 11 additions, 11 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_array.c
- src/plugins/e-acsl/tests/arith/oracle/gen_at.c 8 additions, 8 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_at.c
- src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c 17 additions, 17 deletions...csl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
- src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c
- src/plugins/e-acsl/tests/arith/oracle/gen_cast.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_cast.c
- src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_comparison.c
- src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c 1 addition, 1 deletion...gins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
- src/plugins/e-acsl/tests/arith/oracle/gen_functions.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_functions.c
- src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
- src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c
- src/plugins/e-acsl/tests/arith/oracle/gen_let.c 3 additions, 3 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_let.c
- src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c 2 additions, 3 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_longlong.c
- src/plugins/e-acsl/tests/arith/oracle/gen_not.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_not.c
- src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c 2 additions, 2 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
- src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
- src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c 3 additions, 3 deletionssrc/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
Loading
Please register or sign in to comment