Remove cleanup code from Session.Initialize, add precondition

[kanigsson]

We remove the defensive code from Session.Initialize, which
deallocates buffers for global session variables if already
allocated. We add a precondition "Session.Unitialized" to that
procedure to avoid calling it in such situations.

Fixes #788

[kanigsson]

That proof failure on dhcp_client seems strange. I don't have it locally, and it's in a procedure that's not related to my patch AFAICS.

[treiher]

That proof failure on dhcp_client seems strange. I don't have it locally, and it's in a procedure that's not related to my patch AFAICS.

That is strange. I don't have a good idea what is causing this. Let's see if the issue persists after rebasing and fixing the open comment.

[senier]

That proof failure on dhcp_client seems strange. I don't have it locally, and it's in a procedure that's not related to my patch AFAICS.

That is strange. I don't have a good idea what is causing this. Let's see if the issue persists after rebasing and fixing the open comment.

@treiher An instance of #433?

[kanigsson]

Probably it was because I didn't update the sessions. The new CI is all green (pending the last running test).

[treiher]

That proof failure on dhcp_client seems strange. I don't have it locally, and it's in a procedure that's not related to my patch AFAICS.

That is strange. I don't have a good idea what is causing this. Let's see if the issue persists after rebasing and fixing the open comment.

@treiher An instance of #433?

No, #433 is about occasionally failing verification tests found by property tests. The found issues were usually also reproducible locally. #433 collects all found issues for further investigation.

[senier]

No, #433 is about occasionally failing verification tests found by property tests. The found issues were usually also reproducible locally. #433 collects all found issues for further investigation.

I see.