module greed.memory.lambda_constraint

class LambdaConstraint

Base class for uninstantiated constraints (see the LambdaMemory class)

Extending the Theory of Arrays: memset, memcpy, and Beyond (https://llbmc.org/files/papers/VSTTE13.pdf) see 5.3 "Instantiating Quantifiers"

method __init__

__init__(array=None, new_array=None, parent=None)

method copy

copy(new_state)

method instantiate

instantiate(index)

Instantiate the constraint (on read)

Args:

  • index: The read index

Returns: All instantiated constraints (recursively from the LambdaConstraint hierarchy)

class LambdaMemsetConstraint

Uninstantiated memset constraint

method __init__

__init__(array, start, value, size, new_array, parent)

Args:

  • array: the SMT array on which the memset is applied
  • start: the start index
  • value: the value to write
  • size: how many bytes to write
  • new_array: the new array (after the memset)
  • parent: the parent LambdaConstraint

method copy

copy(new_state)

Copy the constraint (on state copy)

Args:

  • new_state: the new state

method instantiate

instantiate(index)

Instantiate the constraint (on read)

Args:

  • index: The read index

class LambdaMemsetInfiniteConstraint

Uninstantiated memset infinite constraint

method __init__

__init__(array, start, value, new_array, parent)

Args:

  • array: the SMT array on which the memset is applied
  • start: the start index
  • value: the value to write
  • new_array: the new array (after the memset)
  • parent: the parent LambdaConstraint

method copy

copy(new_state)

Copy the constraint (on state copy)

Args:

  • new_state: the new state

method instantiate

instantiate(index)

Instantiate the constraint (on read)

Args:

  • index: The read index

class LambdaMemcopyConstraint

Uninstantiated memcopy constraint

method __init__

__init__(array, start, source, source_start, size, new_array, parent)

Args:

  • array: the SMT array src
  • start: the start index
  • source: the source array
  • source_start: the start index of the source array
  • size: how many bytes to write
  • new_array: the SMT array target of the memcopy
  • parent: the parent LambdaConstraint

method copy

copy(new_state)

Copy the constraint (on state copy)

Args:

  • new_state: the new state

method instantiate

instantiate(index)

Instantiate the constraint (on read)

Args:

  • index: The read index

class LambdaMemcopyInfiniteConstraint

Uninstantiated memcopy infinite constraint

method __init__

__init__(array, start, source, source_start, new_array, parent)

Args:

  • array: the SMT array src
  • start: the start index
  • source: the source array
  • source_start: the start index of the source array
  • new_array: the SMT array target of the memcopy
  • parent: the parent LambdaConstraint

method copy

copy(new_state)

Copy the constraint (on state copy)

Args:

  • new_state: the new state

method instantiate

instantiate(index)

Instantiate the constraint (on read)

Args:

  • index: The read index

This file was automatically generated via lazydocs.