A B C D E F G H I J K L M N O P R S T U V W Z

O

Observations - Class in gov.nasa.jpf.symbc

Observations() - Constructor for class gov.nasa.jpf.symbc.Observations

operandNum - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil

optimizedChoices(ThreadInfo, Instruction, StaticBranchChoiceGenerator) - Static method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.SamePathOptimization

optimizedRegionPath - Static variable in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.SamePathOptimization

optimizedReturnPath - Static variable in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.SamePathOptimization

original - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.IfThenElseStmt

original - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.Instruction

outputTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicRegion

An environment able that holds the vars that needs to be populate their summarized output to SPF.

OutputTable - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment

An Environment table that holds all slots that needs to be populated after successful symmetrization of the region.

OutputTable(IR, boolean, SlotParamTable, InputTable, Stmt) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.OutputTable

OutputTable(IR, boolean, SlotParamTable, InputTable, Stmt, Pair<Integer, Integer>) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.OutputTable

OutputTable(boolean) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.OutputTable

outputTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.StaticRegion

An Environment table that holds the output of the region that needs to be popluated later to SPF upon successful veritesting.

A B C D E F G H I J K L M N O P R S T U V W Z