viper-admin

> **@mschwerhoff** commented on 2018-09-28 15:51 Thank you for the graphs! Here is a not-so-short description of why you get the observed behaviour: Consider the following `while` loop: ```text while...

> **@fpoli** commented on 2018-09-28 15:54 Thanks for the explanation!

> **@alexanderjsummers** commented on 2018-09-28 16:17 btw Carbon just pushes the gotos down to the Boogie level at the moment. Since it never adds invariants there, this works (a) as...

> **@fpoli** commented on 2018-10-01 09:49 Btw, we plan to work around this by introducing extra boolean local variables, such that any problematic `if (expr) ...` becomes `var b: Bool...

> **@dohrau** on 2019-07-29 14:45: > * changed the assignee from (none) to **@dohrau**

> **@gauravpartha** on 2019-07-15 08:15: > * changed `attachment` from `(none)` to `goto_while_loop_issue_392.vpr`

> **@gauravpartha** on 2019-07-15 08:16: > * changed `attachment` from `(none)` to `goto_while_loop_issue_392.vpr` > * edited the description

> **@mschwerhoff** commented on 2019-07-15 08:28 Jumping _into_ a loop results in a irreducible CFG, which isn’t supported. The program should be rejected by Viper. If you agree that the...

> **@gauravpartha** commented on 2019-07-15 08:34 In my opinion this is a reducible CFG \(correct me if I am wrong\). The node at `label loopHead` dominates the backedge from `i...

> **@alexanderjsummers** commented on 2019-07-15 08:42 Is it possible to check the cfg which is actually generated \(and that it is indeed reducible\)? Whether this is the case or not...