Merge branch 'bugfix/basile/eacsl-120-gmp-z-to-q' into 'master'
[eacsl] Add support to create GMP rational from GMP integer Closes e-acsl#120 See merge request frama-c/frama-c!2700
Showing
- src/plugins/e-acsl/doc/Changelog 2 additions, 0 deletionssrc/plugins/e-acsl/doc/Changelog
- src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h 12 additions, 0 deletionssrc/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
- src/plugins/e-acsl/src/analyses/typing.ml 11 additions, 6 deletionssrc/plugins/e-acsl/src/analyses/typing.ml
- src/plugins/e-acsl/src/analyses/typing.mli 6 additions, 2 deletionssrc/plugins/e-acsl/src/analyses/typing.mli
- src/plugins/e-acsl/src/code_generator/gmp.ml 43 additions, 32 deletionssrc/plugins/e-acsl/src/code_generator/gmp.ml
- src/plugins/e-acsl/src/code_generator/logic_functions.ml 4 additions, 1 deletionsrc/plugins/e-acsl/src/code_generator/logic_functions.ml
- src/plugins/e-acsl/src/code_generator/loops.ml 1 addition, 1 deletionsrc/plugins/e-acsl/src/code_generator/loops.ml
- src/plugins/e-acsl/src/code_generator/rational.ml 1 addition, 6 deletionssrc/plugins/e-acsl/src/code_generator/rational.ml
- src/plugins/e-acsl/src/code_generator/translate.ml 1 addition, 1 deletionsrc/plugins/e-acsl/src/code_generator/translate.ml
- src/plugins/e-acsl/tests/gmp-only/arith.i 3 additions, 0 deletionssrc/plugins/e-acsl/tests/gmp-only/arith.i
- src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle 2 additions, 0 deletionssrc/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle
- src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c 46 additions, 0 deletionssrc/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
Loading
Please register or sign in to comment