Volatile Variables. More...

#include <functional>

Include dependency graph for nondet_volatile.h:

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

Macros
#define	NONDET_VOLATILE_OPT "nondet-volatile"

#define	NONDET_VOLATILE_VARIABLE_OPT "nondet-volatile-variable"

#define	NONDET_VOLATILE_MODEL_OPT "nondet-volatile-model"

#define	OPT_NONDET_VOLATILE

#define	HELP_NONDET_VOLATILE

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. More...

void	nondet_volatile (goto_modelt &goto_model, std::function< bool(const exprt &)> should_havoc=[](const exprt &) { return true;})
	Havoc reads from volatile expressions. More...

Detailed Description

Volatile Variables.

Definition in file nondet_volatile.h.

Macro Definition Documentation

◆ HELP_NONDET_VOLATILE

#define HELP_NONDET_VOLATILE

Value:

  " {y--" NONDET_VOLATILE_OPT "} \t " \
  "makes reads from volatile variables non-deterministic\n" \
  " {y--" NONDET_VOLATILE_VARIABLE_OPT "} {uvariable} \t " \
  "makes reads from given volatile variable non-deterministic\n" \
  " {y--" NONDET_VOLATILE_MODEL_OPT "} {uvariable}:{umodel} \t " \
  "models reads from given volatile variable by a call to the given model\n" \

Definition at line 32 of file nondet_volatile.h.

◆ NONDET_VOLATILE_MODEL_OPT

#define NONDET_VOLATILE_MODEL_OPT "nondet-volatile-model"

Definition at line 25 of file nondet_volatile.h.

◆ NONDET_VOLATILE_OPT

#define NONDET_VOLATILE_OPT "nondet-volatile"

Definition at line 23 of file nondet_volatile.h.

◆ NONDET_VOLATILE_VARIABLE_OPT

#define NONDET_VOLATILE_VARIABLE_OPT "nondet-volatile-variable"

Definition at line 24 of file nondet_volatile.h.

◆ OPT_NONDET_VOLATILE

#define OPT_NONDET_VOLATILE

Value:

  "(" NONDET_VOLATILE_OPT ")" \
  "(" NONDET_VOLATILE_VARIABLE_OPT "):" \
  "(" NONDET_VOLATILE_MODEL_OPT "):"

Definition at line 27 of file nondet_volatile.h.

Function Documentation

◆ nondet_volatile() [1/2]

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.

◆ nondet_volatile() [2/2]

void nondet_volatile	(	goto_modelt &	goto_model,
		std::function< bool(const exprt &)>	should_havoc = `[](const exprt &) { return true;}`
	)

Havoc reads from volatile expressions.