Support for solidity global variables

[beillahi]

pragma solidity ^0.5.0;

contract test {

    function g() public returns (uint) {

       return block.timestamp;
    }
}
-----------------
test::[implicit_constructor]: OK
test::g: SKIPPED
Use --show-warnings to see 2 warnings.
Some functions were skipped. Use --verbose to see details.
No errors found.

and

pragma solidity ^0.5.0;

contract test {

    function g() public returns (uint) {

       return block.difficulty;
    }
}
-----------------
test::[implicit_constructor]: OK
test::g: SKIPPED
Use --show-warnings to see 2 warnings.
Some functions were skipped. Use --verbose to see details.
No errors found.

[hajduakos]

Can we treat these special members as nondeterministic variables (so that there is no error)? Or do you need some special assumptions on them?

[beillahi]

Giving these variables nondeterministic values should be fine