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

Typedef Documentation

goto_instruction_codet

using goto_instruction_codet = codet

Definition at line 16 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 105 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 176 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 242 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 374 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 436 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 482 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 527 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]

const code_assignt& to_code_assign ( const goto_instruction_codet &  code )

inline

Definition at line 115 of file goto_instruction_code.h.

to_code_assign() [2/2]

code_assignt& to_code_assign ( goto_instruction_codet &  code )

inline

Definition at line 122 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 186 of file goto_instruction_code.h.

to_code_dead() [2/2]

code_deadt& to_code_dead ( goto_instruction_codet &  code )

inline

Definition at line 193 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 252 of file goto_instruction_code.h.

to_code_decl() [2/2]

code_declt& to_code_decl ( goto_instruction_codet &  code )

inline

Definition at line 259 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 385 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 392 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 537 of file goto_instruction_code.h.

to_code_return() [2/2]

code_returnt& to_code_return ( goto_instruction_codet &  code )

inline

Definition at line 544 of file goto_instruction_code.h.

validate_expr() [1/7]

void validate_expr ( const code_assignt &  x )

inline

Definition at line 110 of file goto_instruction_code.h.

validate_expr() [2/7]

void validate_expr ( const code_deadt &  x )

inline

Definition at line 181 of file goto_instruction_code.h.

validate_expr() [3/7]

void validate_expr ( const code_declt &  x )

inline

Definition at line 247 of file goto_instruction_code.h.

validate_expr() [4/7]

void validate_expr ( const code_function_callt &  x )

inline

Definition at line 379 of file goto_instruction_code.h.

validate_expr() [5/7]

void validate_expr ( const code_inputt &  input )

inline

Definition at line 441 of file goto_instruction_code.h.

validate_expr() [6/7]

void validate_expr ( const code_outputt &  output )

inline

Definition at line 487 of file goto_instruction_code.h.

validate_expr() [7/7]

void validate_expr ( const code_returnt &  x )

inline

Definition at line 532 of file goto_instruction_code.h.