nondet_volatile.cpp File Reference

Volatile Variables. More...

#include "nondet_volatile.h"
#include <util/c_types.h>
#include <util/cmdline.h>
#include <util/fresh_symbol.h>
#include <util/options.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/string_utils.h>
#include <goto-programs/goto_model.h>

Include dependency graph for nondet_volatile.cpp:

Go to the source code of this file.

Classes
class	nondet_volatilet

Functions
void	parse_nondet_volatile_options (const cmdlinet &cmdline, optionst &options)
void	nondet_volatile (goto_modelt &goto_model, const optionst &options)
	Havoc reads from volatile expressions, if enabled in the options.

Detailed Description

Volatile Variables.

Definition in file nondet_volatile.cpp.

Function Documentation

nondet_volatile()

void nondet_volatile	(	goto_modelt &	goto_model,
		const optionst &	options
	)

Havoc reads from volatile expressions, if enabled in the options.

Parameters

goto_model	the goto model in which to havoc volatile reads
options	command line options

Definition at line 456 of file nondet_volatile.cpp.

parse_nondet_volatile_options()

void parse_nondet_volatile_options	(	const cmdlinet &	cmdline,
		optionst &	options
	)

Definition at line 410 of file nondet_volatile.cpp.