Merge branch 'feature/thibaut/function-with-struct-type' into 'master'
Improve support for functions returning structures See merge request frama-c/frama-c!3891
Showing
- src/plugins/e-acsl/doc/Changelog 3 additions, 0 deletionssrc/plugins/e-acsl/doc/Changelog
- src/plugins/e-acsl/src/code_generator/assigns.ml 5 additions, 7 deletionssrc/plugins/e-acsl/src/code_generator/assigns.ml
- src/plugins/e-acsl/src/code_generator/assigns.mli 3 additions, 3 deletionssrc/plugins/e-acsl/src/code_generator/assigns.mli
- src/plugins/e-acsl/src/code_generator/gmp.ml 37 additions, 34 deletionssrc/plugins/e-acsl/src/code_generator/gmp.ml
- src/plugins/e-acsl/src/code_generator/logic_functions.ml 10 additions, 4 deletionssrc/plugins/e-acsl/src/code_generator/logic_functions.ml
- src/plugins/e-acsl/src/code_generator/loops.ml 1 addition, 5 deletionssrc/plugins/e-acsl/src/code_generator/loops.ml
- src/plugins/e-acsl/src/code_generator/rational.ml 0 additions, 7 deletionssrc/plugins/e-acsl/src/code_generator/rational.ml
- src/plugins/e-acsl/src/code_generator/rational.mli 0 additions, 5 deletionssrc/plugins/e-acsl/src/code_generator/rational.mli
- src/plugins/e-acsl/src/code_generator/smart_exp.ml 5 additions, 0 deletionssrc/plugins/e-acsl/src/code_generator/smart_exp.ml
- src/plugins/e-acsl/src/code_generator/smart_exp.mli 2 additions, 0 deletionssrc/plugins/e-acsl/src/code_generator/smart_exp.mli
- src/plugins/e-acsl/src/code_generator/translate_ats.ml 1 addition, 4 deletionssrc/plugins/e-acsl/src/code_generator/translate_ats.ml
- src/plugins/e-acsl/src/code_generator/translate_utils.ml 1 addition, 2 deletionssrc/plugins/e-acsl/src/code_generator/translate_utils.ml
- src/plugins/e-acsl/tests/arith/functions.c 7 additions, 1 deletionsrc/plugins/e-acsl/tests/arith/functions.c
- src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle 33 additions, 21 deletionssrc/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
- src/plugins/e-acsl/tests/arith/oracle/gen_functions.c 119 additions, 44 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_functions.c
- src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c 7 additions, 6 deletionssrc/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
Loading
Please register or sign in to comment