[wp] fix polymorphic definitions compilation
- LogicCompiler: make sure that return type is computed in the frame - Lang: tau_of_return -> tau_of_li_type
Showing
- src/plugins/wp/Lang.ml 3 additions, 3 deletionssrc/plugins/wp/Lang.ml
- src/plugins/wp/Lang.mli 1 addition, 1 deletionsrc/plugins/wp/Lang.mli
- src/plugins/wp/LogicCompiler.ml 49 additions, 40 deletionssrc/plugins/wp/LogicCompiler.ml
- src/plugins/wp/tests/wp_acsl/oracle/poly.res.oracle 61 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/oracle/poly.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle_qualif/poly.res.oracle 25 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/oracle_qualif/poly.res.oracle
- src/plugins/wp/tests/wp_acsl/poly.c 59 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/poly.c
Loading
Please register or sign in to comment