Inline assembly is not implemented

[ellab123]

The test below generates translation error:

contract AssemblyTest
{
    bool b;
    int x;
    constructor () public {
  }

function foo() public {
        b = bar(x);
        if (!b)
            assert(false);
    }
function bar(int x) public returns (bool) { 
    uint256 size;
    assembly { size := x }
    return size > 0;
    }
}

[shuvendu-lahiri]

We stub out the body of the method where inline assembly is present, so it is a non-deterministic method. Users can write further specifications in Boogie level.

[shuvendu-lahiri]

"With this feature a function that contains an inline assembly is translated into a procedure with no implementation, which generates a non-deterministic result. Related regression test is Assembly1.sol." from #243