nondet_volatile.h File Reference

Volatile Variables. More...

#include <goto-programs/goto_model.h>

Include dependency graph for nondet_volatile.h:

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

Go to the source code of this file.

Functions
bool	is_volatile (const symbol_tablet &, const typet &)
void	nondet_volatile (goto_modelt &)

Detailed Description

Volatile Variables.

Definition in file nondet_volatile.h.

Function Documentation

is_volatile()

bool is_volatile	(	const symbol_tablet &	,
		const typet &
	)

Definition at line 19 of file nondet_volatile.cpp.

References irept::get_bool(), irept::id(), is_volatile(), symbol_table_baset::symbols, and to_symbol_type().

Referenced by is_volatile(), and nondet_volatile_rhs().

nondet_volatile()

void nondet_volatile

(

goto_modelt &

)

Definition at line 122 of file nondet_volatile.cpp.

References Forall_goto_functions, goto_modelt::goto_functions, nondet_volatile(), goto_modelt::symbol_table, and goto_functionst::update().