cprover
nondet_volatile.cpp File Reference
#include "nondet_volatile.h"
#include <util/cmdline.h>
#include <util/fresh_symbol.h>
#include <util/options.h>
#include <util/std_expr.h>
#include <util/string_utils.h>
#include <util/symbol_table.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. More...
 

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_modelthe goto model in which to havoc volatile reads
optionscommand line options

Definition at line 452 of file nondet_volatile.cpp.

◆ parse_nondet_volatile_options()

void parse_nondet_volatile_options ( const cmdlinet cmdline,
optionst options 
)

Definition at line 406 of file nondet_volatile.cpp.