Merge branch 'bugfix/julien/force_gmp' into 'master'
Fix a pair of issues with typing of quantifiers See merge request !115
Showing
- src/plugins/e-acsl/quantif.ml 19 additions, 11 deletionssrc/plugins/e-acsl/quantif.ml
- src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
- src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c 151 additions, 0 deletionssrc/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
- src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c 305 additions, 52 deletionssrc/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
- src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle 20 additions, 0 deletionssrc/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
- src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle 15 additions, 1 deletionsrc/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
- src/plugins/e-acsl/tests/gmp/quantif.i 9 additions, 0 deletionssrc/plugins/e-acsl/tests/gmp/quantif.i
- src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c 2 additions, 2 deletionssrc/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
- src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
- src/plugins/e-acsl/translate.ml 3 additions, 3 deletionssrc/plugins/e-acsl/translate.ml
- src/plugins/e-acsl/typing.ml 80 additions, 65 deletionssrc/plugins/e-acsl/typing.ml
- src/plugins/e-acsl/typing.mli 8 additions, 2 deletionssrc/plugins/e-acsl/typing.mli
Loading
Please register or sign in to comment