CLI Option for Disabling Support for Global Variables

[ArquintL]

This might be another slightly controversial PR :P
I just had again a case where Gobra wanted me to create "fake" source files for some transitively imported packages.
I'm even on the fence with myself whether I should actually do it or use my option but in any case it might be handy to (temporarily or not) disable the support for global variables.
I reject a program if it's using global variables, init postconditions or import preconditions. Did I forget any other check?

[jcp19]

It seems to me that what you really want is an option to allow lazy imports; disabling globals seems to be an unfortunate side effect, not the goal. Thus, I think this option could be framed differently and could be called `--lazyImport" - somehow, putting things this way sounds less controversial to me 😄

I agree with the restrictions that you suggest, but I would also check for usages of init blocks.

Finally, if you depend on this, I am ok with merging it but there is one detail that is easy to miss which is that the checks seem to be performed superficially. Thus, a program that has 3 packages like this could never succeed past initialization, but Gobra (with this flag) would not report it:

main/main.go

package main

import "pkg1"

func main() {
    ...
}

pkg1/f.go

package pkg1

import "pkg2"

...

pkg2/f.go

package pkg2

func init() {
    panic()
}

[ArquintL]

All suggestions sound good! Enforcing lazy imports for now basically means disabling global variables but it sounds more future proof as we might need to disable additional language features in the future (or reconsider the CLI option).
I'm happy to add another check that disallows init blocks but I agree that a "broken" dependency, i.e. a dependency with a crashing init block, could not be caught this way

[jcp19]

LGTM!

In the future, if you think that disallowing global variables is too restrictive, one could allow them and only skip the proof obligations concerning initialization; additionally we could emit a message saying that initialization code is currently not checked when the user passes the --lazyImport flag, similarly to the message that we emit when a user uses closures.