New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

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

Jump to bottom

Redefined variables when branching on preprocessor flags #151

Open

s-zanella opened this issue Oct 8, 2019 · 1 comment

Labels

bug

Contributor

s-zanella commented Oct 8, 2019 •

edited

Loading

Conditionals that branch on a boolean variable marked as @CIfDef may extract to code that redefines variables.

[@CIfDef]
assume val b : bool
assume val f : unit -> St UInt8.t

inline_for_extraction let g () =
  if b then
    let n = f () in
    ()

let test () = 
  g ();
  g ()

extracts to

void test()
{
  #if DEBUG
  uint8_t n1 = f();
  #endif
  #if DEBUG
  uint8_t n1 = f();
  #endif
}

which redefines n1. There should be an additional pass to generate unique names, or the variables could be defined in their own block.

The text was updated successfully, but these errors were encountered:

s-zanella added the bug label

Contributor Author

s-zanella commented Nov 5, 2019

I've seen a similar bug with variables redefined in different branches of a switch statement.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment