CBMC: /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/nondet.cpp File Reference

CBMC

Loading...

Searching...

No Matches

nondet.cpp File Reference

#include "nondet.h"
#include <util/arith_tools.h>
#include <ansi-c/allocate_objects.h>

+ Include dependency graph for nondet.cpp:

Go to the source code of this file.

Functions

symbol_exprt generate_nondet_int (const exprt &min_value_expr, const exprt &max_value_expr, const std::string &basename_prefix, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions)

Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions) except the minimum and maximum values are represented as exprts.

symbol_exprt generate_nondet_int (const exprt &min_value_expr, const exprt &max_value_expr, const std::string &basename_prefix, const source_locationt &source_location, const allocate_local_symbolt &alocate_local_symbol, code_blockt &instructions)

Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions) except the minimum and maximum values are represented as exprts, and symbols are allocated using allocate_local_symbolt.

symbol_exprt generate_nondet_int (const mp_integer &min_value, const mp_integer &max_value, const std::string &basename_prefix, const typet &int_type, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions)

Gets a fresh nondet choice in range (min_value, max_value).

code_blockt generate_nondet_switch (const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table)

Pick nondeterministically between imperative actions 'switch_cases'.

Function Documentation

◆ generate_nondet_int() [1/3]

symbol_exprt generate_nondet_int ( const exprt & min_value_expr,

const exprt & max_value_expr,

const std::string & basename_prefix,

const source_locationt & source_location,

allocate_objectst & allocate_objects,

code_blockt & instructions

)

Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions) except the minimum and maximum values are represented as exprts.

Definition at line 15 of file nondet.cpp.

◆ generate_nondet_int() [2/3]

symbol_exprt generate_nondet_int ( const exprt & min_value_expr,

const exprt & max_value_expr,

const std::string & basename_prefix,

const source_locationt & source_location,

const allocate_local_symbolt & alocate_local_symbol,

code_blockt & instructions

)

Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions) except the minimum and maximum values are represented as exprts, and symbols are allocated using allocate_local_symbolt.

Definition at line 38 of file nondet.cpp.

◆ generate_nondet_int() [3/3]

symbol_exprt generate_nondet_int ( const mp_integer & min_value,

const mp_integer & max_value,

const std::string & basename_prefix,

const typet & int_type,

const source_locationt & source_location,

allocate_objectst & allocate_objects,

code_blockt & instructions

)

Gets a fresh nondet choice in range (min_value, max_value).

GOTO generated resembles:

int_type name_prefix::nondet_int = NONDET(int_type)

ASSUME(name_prefix::nondet_int >= min_value)

ASSUME(name_prefix::nondet_int <= max_value)

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

dfcc_ptr_havoc_modet::NONDET

@ NONDET

havocs the pointer to an nondet pointer

@ ASSUME

Definition goto_program.h:34

Parameters: min_value Minimum value (inclusive) of returned int.

max_value Maximum value (inclusive) of returned int.

basename_prefix Basename prefix for the fresh symbol name generated.

int_type The type of the int used to non-deterministically choose one of the switch cases.

allocate_objects Handles allocation of new objects.

source_location The location to mark the generated int with.

[out] instructions Output instructions are written to 'instructions'. These declare, nondet-initialise and range-constrain (with assume statements) a fresh integer.

Returns: Returns a symbol expression for the resulting integer.

Definition at line 72 of file nondet.cpp.

◆ generate_nondet_switch()

code_blockt generate_nondet_switch ( const irep_idt & name_prefix,

const alternate_casest & switch_cases,

const typet & int_type,

const irep_idt & mode,

const source_locationt & source_location,

symbol_table_baset & symbol_table

)

Pick nondeterministically between imperative actions 'switch_cases'.

Parameters: name_prefix Name prefix for fresh symbols (should be function id)

switch_cases List of codet objects to execute in each switch case.

int_type The type of the int used to non-deterministically choose one of the switch cases.

mode Mode (language) of the symbol to be generated.

source_location The location to mark the generated int with.

symbol_table The global symbol table.

Returns: Returns a nondet-switch choosing between switch_cases. The resulting switch block has no default case.

Definition at line 91 of file nondet.cpp.