Jean-Christophe Léchenet
Jean-Christophe Léchenet
Benjamin also finds surprising that the allocator does not decide on its own to put the return address on the stack when it detects that it does not have enough...
Hum, so there is something fishy about the removal of the error `Cerr_need_spill`.
Ok, I discussed with Benjamin. Before, the checker was backward, so we failed at the call sites when seeing a live register modified by the call. Now the checker is...
Summary of a discussion: something specific (and maybe a bit fishy) was done for registers holding the return address. But the bug is also present even when using `#[returnaddress="stack]`, so...
So it does the same as for the return address? It knows something is wrong but continues nonetheless?
So it really remains to be decided whether we want to fail early in OCaml or later in Coq.
And to be complete, there are other errors that are caught by Coq (and that are different from what they were before). Note that all the examples have uninitialized variables....
There again, errors were rather clearer before.
cc @AntoineSere who mentioned that problem to me. Did I describe the issue faithfully?
Here is a pointer to a failure of a GitHub job : https://github.com/jasmin-lang/jasmin/runs/6080469236?check_suite_focus=true.