Merge branch 'bugfix/julien/ctype_to_gmp' into 'master'
Fix 2 bugs with integer casts This MR fixes two bugs with integer casts: - when generating a new variable corresponding to a cast ```(ty)t```, its type was the one of the translation of ```t```, not ```ty``` - for a cast ```(ty)t``` the implementation of the type system didn't compute the smallest interval from both operands. It might result in incorrectness of the generated code as reported in https://bts.frama-c.com/view.php?id=2231 (which is now fixed). I guess this patch also solves your gmp issue with SpecCPU Benchmark. See merge request !78
Showing
- src/plugins/e-acsl/tests/bts/bts2231.i 10 additions, 0 deletionssrc/plugins/e-acsl/tests/bts/bts2231.i
- src/plugins/e-acsl/tests/bts/oracle/bts2231.err.oracle 0 additions, 0 deletionssrc/plugins/e-acsl/tests/bts/oracle/bts2231.err.oracle
- src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle 4 additions, 0 deletionssrc/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
- src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c 7 additions, 6 deletionssrc/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
- src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c 57 additions, 0 deletionssrc/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
- src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle 2 additions, 1 deletionsrc/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
- src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle 3 additions, 2 deletionssrc/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
- src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c 5 additions, 4 deletionssrc/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
- src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle 1 addition, 1 deletionsrc/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
- src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c 3 additions, 3 deletionssrc/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
- src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c 2 additions, 2 deletionssrc/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
- src/plugins/e-acsl/translate.ml 1 addition, 1 deletionsrc/plugins/e-acsl/translate.ml
- src/plugins/e-acsl/typing.ml 2 additions, 1 deletionsrc/plugins/e-acsl/typing.ml
Loading
Please register or sign in to comment