Vincent Laporte comments

Repositories
Issues
Comments

Results 123 comments of


                                            Vincent Laporte

With option returnaddress=stack, the compiler can use LR/ra as a result register

Does `returnaddress=stack` makes sense on risc-v?

With option returnaddress=stack, the compiler can use LR/ra as a result register

No, the `POPPC` instruction takes it from the top of the stack.

[WIP] Refactor extraction to build an easycrypt AST, then pretty-print it.

The fixes to the testing infrastructure should be moved to a different PR (and merged quickly). The removal of extraction for safety deserves a changelog entry and misses some cleaning...