loop_invariant Namespace Reference

Functions
bool	is_inert_scan_instruction (goto_programt::const_targett t)
	Instructions with no effect a caller needs to account for: no write to a tracked variable, no control-flow or heap/external effect.

Function Documentation

is_inert_scan_instruction()

bool loop_invariant::is_inert_scan_instruction

(

goto_programt::const_targett

t

)

Instructions with no effect a caller needs to account for: no write to a tracked variable, no control-flow or heap/external effect.

Shared by two scans that both need exactly this and nothing more – the window between a synthesised marker and the loop head it was emitted for, and goto_invariant_synthesis's reading of a loop body.