Code

Refactoring of symex_assign_symbol#4642

Code

Merged

tautschnig merged 13 commits intodiffblue:developdiffblue/cbmc:developfrom

romainbrenguier:refactor/symex_assignromainbrenguier/cbmc:refactor/symex_assignCopy head branch name to clipboard

May 13, 2019

Commits

Commits on May 13, 2019

• Rename guarded_rhs and use move instead of swap

  Show description for 940779d
  romainbrenguier

  committed
  940779d

  Copy full SHA for 940779d

• Better scope guarded_rhs

  Show description for 5111b4d
  romainbrenguier

  committed
  5111b4d

  Copy full SHA for 5111b4d

• Make shift_indexed_access_to_lhs return an exprt

  Show description for cf576fc
  romainbrenguier

  committed
  cf576fc

  Copy full SHA for cf576fc

• Return modified lhs in shift_indexed_access_to_lhs

  Show description for ab30a67
  romainbrenguier

  committed
  ab30a67

  Copy full SHA for ab30a67

• Make rewrite_with_to_field_symbols return an assignmentt

  Show description for 9221e0e
  romainbrenguier

  committed
  9221e0e

  Copy full SHA for 9221e0e

• Make rewrite_to_field_symbols take assignmentt argument

  Show description for 892aacd
  romainbrenguier

  committed
  892aacd

  Copy full SHA for 892aacd

• Make shift_indexed_access_to_lhs take assignment argument

  Show description for d51c192
  romainbrenguier

  committed
  d51c192

  Copy full SHA for d51c192

• Make assignment return rename lhs

  Show description for faeb70c
  romainbrenguier

  committed
  faeb70c

  Copy full SHA for faeb70c

• Replace record_events by a stack

  Show description for 822c493
  romainbrenguier

  committed
  822c493

  Copy full SHA for 822c493

• Avoid unneccessary copy

  Show description for 5d0ac3a
  romainbrenguier

  committed
  5d0ac3a

  Copy full SHA for 5d0ac3a

• Mark l2_full_lhs const

  Show description for ae52ed3
  romainbrenguier

  committed
  ae52ed3

  Copy full SHA for ae52ed3

• Make get_original_name return the expression

  Show description for d6418ff
  romainbrenguier

  committed
  d6418ff

  Copy full SHA for d6418ff

• Replace set_indices by an invariant

  Show description for fdc03e0
  romainbrenguier

  committed
  fdc03e0

  Copy full SHA for fdc03e0