Improve function ensures clause error reporting, and isolate expression proofs

[keyboardDrummer]

Changes

• Report the return location when function postconditions fail to prove, instead of always pointing to the function name. Example below
• Isolate proofs inside expressions from the surrounding proofs
• Expression proofs still affect the proof of the ensures clause of the surrounding function, unless inside a let binding.

Example of improved error reporting:

function ElseError(x: int): int // previous primary error location
  ensures ElseError(x) == 0 // related error location
{
  if x == 0 then
    0 
  else 
    1 // new primary error location
}
function ThenError(x: int): int // previous primary error location
  ensures ThenError(x) == 0 // related error location
{
  if x == 0 then
    1 // new primary error location
  else 
    0 
}

function CaseError(x: int): int // previous primary error location
  ensures CaseError(x) == 1 // related error location
{
  match x {
    case 0 => 1
    case 1 => 0 // new primary error location
    case _ => 1 
  }
}

function LetError(x: int): int // previous primary error location
  ensures LetError(x) == 1 // related error location
{
  var r := 3;
  r // new primary error location
}

How has this been tested?

• Added CLI test ast/functions/ensuresReporting.dfy
• Added CLI test ast/expressions/statementExpressionScope.dfy

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.