lower_longjmp.cpp File Reference

#include <goto-programs/lower_longjmp.h>
#include <goto-programs/goto_functions.h>
#include <irep2/irep2_utils.h>
#include <util/irep/migrate.h>
#include <util/symtab/context.h>
#include <util/config/options.h>

Include dependency graph for lower_longjmp.cpp:

Functions
void	lower_longjmp (goto_functionst &goto_functions, contextt &context, const optionst &options)
	Lower longjmp's non-local transfer of control to guarded gotos.

Function Documentation

lower_longjmp()

void lower_longjmp	(	goto_functionst &	goto_functions,
		contextt &	context,
		const optionst &	options )

Lower longjmp's non-local transfer of control to guarded gotos.

The setjmp model stores a fresh token in the jmp_buf, which each call site copies into a frame-local slot. The longjmp model arms __ESBMC_longjmp_{pending,token,value}. After every call, a pending longjmp branches to its function's dispatch block, which resumes after the setjmp site whose slot holds the token, with the longjmp value as setjmp's result, or else returns so the caller dispatches in turn. A no-op for a program that never calls longjmp, and under –enable-unreachability-intrinsic, where the setjmp model reports setjmp as out of scope instead.