Add support for loops formed via labels and gotos

[viper-admin]

Created by @mschwerhoff on 2017-02-21 17:18
Last updated on 2019-07-23 11:19

[viper-admin]

@mschwerhoff commented on 2017-02-21 18:11

Currently affected test cases:

• all/invariants/while1.sil
• all/invariants/while3.sil
• all/invariants/loops1.sil
• all/invariants/loops2.sil
• all/issues/silicon/0269.sil

[viper-admin]

@gauravpartha on 2019-07-23 11:19:

• changed the assignee from (none) to @gauravpartha

[gauravpartha]

Fixed by #389.

There still is an incompleteness in while3.sil, see #390.