goto_instruction_code.h File Reference

#include <util/cprover_prefix.h>
#include <util/std_code_base.h>
#include <util/std_expr.h>

Include dependency graph for goto_instruction_code.h:

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

Go to the source code of this file.

Classes
class	code_assignt
	A codet representing an assignment in the program. More...
class	code_deadt
	A codet representing the removal of a local variable going out of scope. More...
class	code_declt
	A codet representing the declaration of a local variable. More...
class	code_function_callt
	codet representation of a function call statement. More...
class	code_inputt
	A codet representing the declaration that an input of a particular description has a value which corresponds to the value of a given expression (or expressions). More...
class	code_outputt
	A codet representing the declaration that an output of a particular description has a value which corresponds to the value of a given expression (or expressions). More...
class	code_returnt
	codet representation of a "return from a function" statement. More...

Functions
template<>
bool	can_cast_expr< code_assignt > (const exprt &base)
void	validate_expr (const code_assignt &x)
const code_assignt &	to_code_assign (const codet &code)
code_assignt &	to_code_assign (codet &code)
template<>
bool	can_cast_expr< code_deadt > (const exprt &base)
void	validate_expr (const code_deadt &x)
const code_deadt &	to_code_dead (const codet &code)
code_deadt &	to_code_dead (codet &code)
template<>
bool	can_cast_expr< code_declt > (const exprt &base)
void	validate_expr (const code_declt &x)
const code_declt &	to_code_decl (const codet &code)
code_declt &	to_code_decl (codet &code)
template<>
bool	can_cast_expr< code_function_callt > (const exprt &base)
void	validate_expr (const code_function_callt &x)
const code_function_callt &	to_code_function_call (const codet &code)
code_function_callt &	to_code_function_call (codet &code)
template<>
bool	can_cast_expr< code_inputt > (const exprt &base)
void	validate_expr (const code_inputt &input)
template<>
bool	can_cast_expr< code_outputt > (const exprt &base)
void	validate_expr (const code_outputt &output)
template<>
bool	can_cast_expr< code_returnt > (const exprt &base)
void	validate_expr (const code_returnt &x)
const code_returnt &	to_code_return (const codet &code)
code_returnt &	to_code_return (codet &code)
code_function_callt	havoc_slice_call (const exprt &p, const exprt &size, const namespacet &ns)
	Builds a code_function_callt to __CPROVER_havoc_slice(p, size).

Function Documentation

can_cast_expr< code_assignt >()

template<>

bool can_cast_expr< code_assignt > ( const exprt &  base )

inline

Definition at line 100 of file goto_instruction_code.h.

can_cast_expr< code_deadt >()

template<>

bool can_cast_expr< code_deadt > ( const exprt &  base )

inline

Definition at line 170 of file goto_instruction_code.h.

can_cast_expr< code_declt >()

template<>

bool can_cast_expr< code_declt > ( const exprt &  base )

inline

Definition at line 235 of file goto_instruction_code.h.

can_cast_expr< code_function_callt >()

template<>

bool can_cast_expr< code_function_callt > ( const exprt &  base )

inline

Definition at line 367 of file goto_instruction_code.h.

can_cast_expr< code_inputt >()

template<>

bool can_cast_expr< code_inputt > ( const exprt &  base )

inline

Definition at line 428 of file goto_instruction_code.h.

can_cast_expr< code_outputt >()

template<>

bool can_cast_expr< code_outputt > ( const exprt &  base )

inline

Definition at line 474 of file goto_instruction_code.h.

can_cast_expr< code_returnt >()

template<>

bool can_cast_expr< code_returnt > ( const exprt &  base )

inline

Definition at line 517 of file goto_instruction_code.h.

havoc_slice_call()

code_function_callt havoc_slice_call ( const exprt &  p, const exprt &  size, const namespacet &  ns  )

inline

Builds a code_function_callt to __CPROVER_havoc_slice(p, size).

Parameters

p	The pointer argument.
size	The size argument.
ns	Namespace where the __CPROVER_havoc_slice symbol can be found.

Remarks

: It is a PRECONDITION that __CPROVER_havoc_slice exists in the namespace

Returns

A code_function_callt expression nil_exprt() := __CPROVER_havoc_slice(p, size).

Definition at line 78 of file goto_instruction_code.cpp.

to_code_assign() [1/2]

code_assignt & to_code_assign ( codet &  code )

inline

Definition at line 117 of file goto_instruction_code.h.

to_code_assign() [2/2]

const code_assignt & to_code_assign ( const codet &  code )

inline

Definition at line 110 of file goto_instruction_code.h.

to_code_dead() [1/2]

code_deadt & to_code_dead ( codet &  code )

inline

Definition at line 187 of file goto_instruction_code.h.

to_code_dead() [2/2]

const code_deadt & to_code_dead ( const codet &  code )

inline

Definition at line 180 of file goto_instruction_code.h.

to_code_decl() [1/2]

code_declt & to_code_decl ( codet &  code )

inline

Definition at line 252 of file goto_instruction_code.h.

to_code_decl() [2/2]

const code_declt & to_code_decl ( const codet &  code )

inline

Definition at line 245 of file goto_instruction_code.h.

to_code_function_call() [1/2]

code_function_callt & to_code_function_call ( codet &  code )

inline

Definition at line 384 of file goto_instruction_code.h.

to_code_function_call() [2/2]

const code_function_callt & to_code_function_call ( const codet &  code )

inline

Definition at line 377 of file goto_instruction_code.h.

to_code_return() [1/2]

code_returnt & to_code_return ( codet &  code )

inline

Definition at line 534 of file goto_instruction_code.h.

to_code_return() [2/2]

const code_returnt & to_code_return ( const codet &  code )

inline

Definition at line 527 of file goto_instruction_code.h.

validate_expr() [1/7]

void validate_expr ( const code_assignt &  x )

inline

Definition at line 105 of file goto_instruction_code.h.

validate_expr() [2/7]

void validate_expr ( const code_deadt &  x )

inline

Definition at line 175 of file goto_instruction_code.h.

validate_expr() [3/7]

void validate_expr ( const code_declt &  x )

inline

Definition at line 240 of file goto_instruction_code.h.

validate_expr() [4/7]

void validate_expr ( const code_function_callt &  x )

inline

Definition at line 372 of file goto_instruction_code.h.

validate_expr() [5/7]

void validate_expr ( const code_inputt &  input )

inline

Definition at line 433 of file goto_instruction_code.h.

validate_expr() [6/7]

void validate_expr ( const code_outputt &  output )

inline

Definition at line 479 of file goto_instruction_code.h.

validate_expr() [7/7]

void validate_expr ( const code_returnt &  x )

inline

Definition at line 522 of file goto_instruction_code.h.