Skip to content

Commit

Permalink
Report resolution errors to downstream system
Browse files Browse the repository at this point in the history
  • Loading branch information
keyboardDrummer committed Mar 21, 2024
1 parent 675e5a5 commit d29d5f2
Showing 1 changed file with 24 additions and 3 deletions.
27 changes: 24 additions & 3 deletions Source/ExecutionEngine/ExecutionEngine.cs
Original file line number Diff line number Diff line change
Expand Up @@ -702,9 +702,30 @@ private async Task<PipelineOutcome> VerifyEachImplementation(TextWriter outputWr

}

public IReadOnlyList<IVerificationTask> GetVerificationTasks(Program program) {
program.Resolve(Options);
program.Typecheck(Options);
class CollectingErrorSink : IErrorSink
{
public readonly List<(IToken Token, string Message)> Errors = new();

public void Error(IToken tok, string msg)
{
Errors.Add((tok, msg));
}
}

public IReadOnlyList<IVerificationTask> GetVerificationTasks(Program program)
{
var sink = new CollectingErrorSink();
var resolutionErrors = program.Resolve(Options, sink);
var errors = string.Join("\n", sink.Errors.Select(t => $"{t.Token}: {t.Message}"));
if (resolutionErrors > 0)
{
throw new Exception($"Boogie program had {resolutionErrors} resolution errors:\n{errors}");
}
var typeErrors = program.Typecheck(Options, sink);
if (typeErrors > 0)
{
throw new Exception($"Boogie program had {typeErrors} type errors:\n{errors}");
}

EliminateDeadVariables(program);
CollectModSets(program);
Expand Down

0 comments on commit d29d5f2

Please sign in to comment.