Jean-Christophe Léchenet
Jean-Christophe Léchenet
Similar error ``` inline fn sum (stack u64[2] a) -> reg u64 { stack u64 r; r = a[0]; r += a[1]; return r; } export fn f (reg u64...
Remark from Benjamin : maybe we want to compile non-inlined functions taking reg arrays as parameters.
Benjamin's remark: maybe we can be more strict on non-inline function than on inline ones. For instance, passing constants to functions could be accepted if they are inline, and not...
I discovered that for `VMOV`, but there are certainly other instructions with the same problem.
I guess so. But I think this could also be solved without such a refactoring (probably a tedious work though). As usual, I am used to creating an issue as...
Btw, at least from a user perspective, this issue is similar to https://github.com/jasmin-lang/jasmin/issues/69 where another annotation is silently ignored.
Indeed, the annotation has an impact only the type of the argument. It's probably better to close this.
> * in target `easycrypt`, what version is tested? It seems that it's a commit hard-coded in `scripts/easycrypt.nix`. Is it what we want to test? I think that you can...
+1 to targetting `main` for now, then the latest release. > Do you plan to check whether the EasyCrypt generated by Jasmin is valid? Currently, if I am not wrong,...
Turns out that the same mispositioning happens for `while` loops.