(Ugly version) Improve function ensures clause error reporting

[keyboardDrummer]

Description

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

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