goto_instruction_code.h File Reference

#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 goto_instruction_codet representing an assignment in the program. More...
class	code_deadt
	A goto_instruction_codet representing the removal of a local variable going out of scope. More...
class	code_declt
	A goto_instruction_codet representing the declaration of a local variable. More...
class	code_function_callt
	goto_instruction_codet representation of a function call statement. More...
class	code_inputt
	A goto_instruction_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 goto_instruction_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
	goto_instruction_codet representation of a "return from a function" statement. More...

Typedefs
using	goto_instruction_codet = codet

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 goto_instruction_codet &code)
code_assignt &	to_code_assign (goto_instruction_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 goto_instruction_codet &code)
code_deadt &	to_code_dead (goto_instruction_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 goto_instruction_codet &code)
code_declt &	to_code_decl (goto_instruction_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 goto_instruction_codet &code)
code_function_callt &	to_code_function_call (goto_instruction_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 goto_instruction_codet &code)
code_returnt &	to_code_return (goto_instruction_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).

Typedef Documentation

goto_instruction_codet

using goto_instruction_codet = codet

Definition at line 15 of file goto_instruction_code.h.

Function Documentation

can_cast_expr< code_assignt >()

template<>

bool can_cast_expr< code_assignt > ( const exprt &  base )

inline

Definition at line 104 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 175 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 241 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 373 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 435 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 481 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 526 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 81 of file goto_instruction_code.cpp.

to_code_assign() [1/2]

const code_assignt & to_code_assign ( const goto_instruction_codet &  code )

inline

Definition at line 114 of file goto_instruction_code.h.

to_code_assign() [2/2]

code_assignt & to_code_assign ( goto_instruction_codet &  code )

inline

Definition at line 121 of file goto_instruction_code.h.

to_code_dead() [1/2]

const code_deadt & to_code_dead ( const goto_instruction_codet &  code )

inline

Definition at line 185 of file goto_instruction_code.h.

to_code_dead() [2/2]

code_deadt & to_code_dead ( goto_instruction_codet &  code )

inline

Definition at line 192 of file goto_instruction_code.h.

to_code_decl() [1/2]

const code_declt & to_code_decl ( const goto_instruction_codet &  code )

inline

Definition at line 251 of file goto_instruction_code.h.

to_code_decl() [2/2]

code_declt & to_code_decl ( goto_instruction_codet &  code )

inline

Definition at line 258 of file goto_instruction_code.h.

to_code_function_call() [1/2]

const code_function_callt & to_code_function_call ( const goto_instruction_codet &  code )

inline

Definition at line 384 of file goto_instruction_code.h.

to_code_function_call() [2/2]

code_function_callt & to_code_function_call ( goto_instruction_codet &  code )

inline

Definition at line 391 of file goto_instruction_code.h.

to_code_return() [1/2]

const code_returnt & to_code_return ( const goto_instruction_codet &  code )

inline

Definition at line 536 of file goto_instruction_code.h.

to_code_return() [2/2]

code_returnt & to_code_return ( goto_instruction_codet &  code )

inline

Definition at line 543 of file goto_instruction_code.h.

validate_expr() [1/7]

void validate_expr ( const code_assignt &  x )

inline

Definition at line 109 of file goto_instruction_code.h.

validate_expr() [2/7]

void validate_expr ( const code_deadt &  x )

inline

Definition at line 180 of file goto_instruction_code.h.

validate_expr() [3/7]

void validate_expr ( const code_declt &  x )

inline

Definition at line 246 of file goto_instruction_code.h.

validate_expr() [4/7]

void validate_expr ( const code_function_callt &  x )

inline

Definition at line 378 of file goto_instruction_code.h.

validate_expr() [5/7]

void validate_expr ( const code_inputt &  input )

inline

Definition at line 440 of file goto_instruction_code.h.

validate_expr() [6/7]

void validate_expr ( const code_outputt &  output )

inline

Definition at line 486 of file goto_instruction_code.h.

validate_expr() [7/7]

void validate_expr ( const code_returnt &  x )

inline

Definition at line 531 of file goto_instruction_code.h.