runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
34 stars 19 forks source link

set noreturn attribute on finish-rewriting call site #1087

Closed dwightguth closed 1 month ago

dwightguth commented 1 month ago

This is one of a sequence of PRs designed to make progress towards generating stack maps so that we can trigger the GC during allocation rather than in between rewrite steps only. The first few PRs will be preliminaries that add small features that will be used by future PRs.

In this PR we simply add the noreturn attribute to the call site of the finish_rewriting function so that llvm is able to statically understand that the unreachable instruction after the call site is in fact unreachable.