cprover
nondet_volatile.cpp File Reference

Volatile Variables. More...

#include "nondet_volatile.h"
#include <util/std_expr.h>
#include <util/symbol_table.h>
+ Include dependency graph for nondet_volatile.cpp:

Go to the source code of this file.

Functions

bool is_volatile (const symbol_tablet &symbol_table, const typet &src)
 
void nondet_volatile_rhs (const symbol_tablet &symbol_table, exprt &expr)
 
void nondet_volatile_lhs (const symbol_tablet &symbol_table, exprt &expr)
 
void nondet_volatile (symbol_tablet &symbol_table, goto_programt &goto_program)
 
void nondet_volatile (goto_modelt &goto_model)
 

Detailed Description

Volatile Variables.

Definition in file nondet_volatile.cpp.

Function Documentation

◆ is_volatile()

bool is_volatile ( const symbol_tablet symbol_table,
const typet src 
)

Definition at line 19 of file nondet_volatile.cpp.

◆ nondet_volatile() [1/2]

void nondet_volatile ( symbol_tablet symbol_table,
goto_programt goto_program 
)

Definition at line 80 of file nondet_volatile.cpp.

◆ nondet_volatile() [2/2]

void nondet_volatile ( goto_modelt goto_model)

Definition at line 122 of file nondet_volatile.cpp.

◆ nondet_volatile_lhs()

void nondet_volatile_lhs ( const symbol_tablet symbol_table,
exprt expr 
)

Definition at line 57 of file nondet_volatile.cpp.

◆ nondet_volatile_rhs()

void nondet_volatile_rhs ( const symbol_tablet symbol_table,
exprt expr 
)

Definition at line 37 of file nondet_volatile.cpp.