We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
KreMLin (version 4e48d26) generated incorrect C code with the -fmerge aggressive options.
-fmerge aggressive
open U32 inline_for_extraction private let test1(b: U32.t{U32.v b < 10}): Tot U32.t = let g = 10ul +^ b in if g >^ 5ul then let d = g -^ 1ul in g +^ d else 0ul let rec test2(a: U32.t{U32.v a < 10}): Tot U32.t (decreases U32.v a) = let c = test1 a in if a >^ 0ul then test2 (a -^ 1ul) else c
uint32_t test2(uint32_t a0) { uint32_t a = a0; while (true) { uint32_t g = (uint32_t)10U + a; uint32_t c; if (g > (uint32_t)5U) { a = g - (uint32_t)1U; c = g + a; } else { c = (uint32_t)0U; } if (a > (uint32_t)0U) { a--; } else { return c; } } KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n", __FILE__, __LINE__, "unreachable, returns inserted above"); KRML_HOST_EXIT(255U); }
The C code above will loop infinitely.
The text was updated successfully, but these errors were encountered:
Is this using the combination of -fmerge and -ftail-calls?
-fmerge
-ftail-calls
Thanks for the repro. From the Changelog,
### Jan 13th, 2020 - New *experimental* option: `-fmerge`, to merge variables, i.e. reuse existing
so, I don't think it's been extensively tested (and it's marked as experimental). I'd happily take a fix if you have one.
Sorry, something went wrong.
No branches or pull requests
KreMLin (version 4e48d26) generated incorrect C code with the
-fmerge aggressive
options.Low* Code
Compiled C Code
The C code above will loop infinitely.
The text was updated successfully, but these errors were encountered: