Load reference from array ..., arrayref, index => ..., value YN: fixed choice selection in symcrete support (Yannic Noller <nolleryc@gmail.com>)

Load reference from array ..., arrayref, index => ..., value

Store into reference array ..., arrayref, index, value => ... YN: fixed choice selection in symcrete support (Yannic Noller <nolleryc@gmail.com>)

Store into reference array ..., arrayref, index, value => ...

Symbolic version of the ANEWARRAY class from jpf-core. Has some extra code to detect if a symbolic variable is being used as the size of the new array

@author Kasper Luckow TODO: There might be issues with non-determinism

@author Kasper Luckow

Load byte or boolean from array ..., arrayref, index => ..., value YN: added symcrete support (Yannic Noller <nolleryc@gmail.com>)

Load byte or boolean from array ..., arrayref, index => ..., value

Store into byte or boolean array ..., arrayref, index, value => ... YN: added symcrete support (Yannic Noller <nolleryc@gmail.com>)

Store into byte or boolean array ..., arrayref, index, value => ...

@author Mithun Acharya Taken from Tao Xie's CSC 591t class In fact, this is same as issta2006.BinTree.BinTree.java

@author Mithun Acharya launch configuration +vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory +vm.classpath=. +vm.storage.class= +

@author Mithun Acharya Arguments for concrete execution: BSTDriverSequences Arguments for symbolic execution: +vm.insn_factory.class=gov.nasa.jpf.s

@author Mithun Acharya Taken from Inkumsah, Xie's ASE08 paper

@author Mithun Acharya

Taken from issta2006.BinTree

@author Sarfraz Khurshid (khurshid@lcs.mit.edu)

Minimal model for BufferedImage that makes everything symbolic. @author Rody Kersten

@author corina pasareanu corina.pasareanu@sv.cmu.edu

Load char from array ..., arrayref, index => ..., value YN: added symcrete support (Yannic Noller <nolleryc@gmail.com>)

Load char from array ..., arrayref, index => ..., value

Store into char array ..., arrayref, index, value => ... YN: added symcrete support (Yannic Noller <nolleryc@gmail.com>)

Store into char array ..., arrayref, index, value => ...

@author jburnim@cs.berkeley.edu

A visitor for both constraints and expressions. Ideally, constraints should be an extension of expressions themselves, but, alas!, they are not. Each

Convert double to float ..., value => ..., result

Convert double to int ..., value => ..., result

Convert double to long ..., value => ..., result

Load double from array ..., arrayref, index => ..., value YN: added symcrete support (Yannic Noller <nolleryc@gmail.com>)

Load double from array ..., arrayref, index => ..., value