dfcc_infer_loop_assigns.h File Reference

Infer a set of assigns clause targets for a natural loop. More...

#include <analyses/local_may_alias.h>
#include <goto-instrument/loop_utils.h>
#include "dfcc_loop_nesting_graph.h"

Include dependency graph for dfcc_infer_loop_assigns.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
std::unordered_set< irep_idt >	gen_loop_locals_set (const irep_idt &function_id, goto_functiont &goto_function, const dfcc_loop_nesting_graph_nodet &loop, message_handlert &message_handler, const namespacet &ns)
	Collect identifiers that are local to loop. More...
void	dfcc_infer_loop_assigns_for_function (std::map< std::size_t, assignst > &inferred_loop_assigns_map, goto_functionst &goto_functions, const goto_functiont &goto_function, message_handlert &message_handler, const namespacet &ns)
	Infer assigns clause targets for loops in goto_function from their instructions and an alias analysis at the function level (with inlining), and store the result in inferred_loop_assigns_map, a map from loop numbers to the set of inferred assigns targets. More...

Detailed Description

Infer a set of assigns clause targets for a natural loop.

Definition in file dfcc_infer_loop_assigns.h.

Function Documentation

dfcc_infer_loop_assigns_for_function()

void dfcc_infer_loop_assigns_for_function	(	std::map< std::size_t, assignst > &	inferred_loop_assigns_map,
		goto_functionst &	goto_functions,
		const goto_functiont &	goto_function,
		message_handlert &	message_handler,
		const namespacet &	ns
	)

Infer assigns clause targets for loops in goto_function from their instructions and an alias analysis at the function level (with inlining), and store the result in inferred_loop_assigns_map, a map from loop numbers to the set of inferred assigns targets.

Definition at line 302 of file dfcc_infer_loop_assigns.cpp.

gen_loop_locals_set()

std::unordered_set<irep_idt> gen_loop_locals_set	(	const irep_idt &	function_id,
		goto_functiont &	goto_function,
		const dfcc_loop_nesting_graph_nodet &	loop_node,
		message_handlert &	message_handler,
		const namespacet &	ns
	)

Collect identifiers that are local to loop.

Collect identifiers that are local to loop.

A identifier is or is equivalent to a loop local if

1. it is declared inside the loop, or
2. there is no write or read of it outside the loop.
3. it is not used in loop contracts.

Definition at line 58 of file dfcc_infer_loop_assigns.cpp.