Skip to content

Commit 9268b98

Browse files
ange1506ange1506
authored
Refactor command for inferLikelyInvariants function
1 parent f6e5016 commit 9268b98

1 file changed

Lines changed: 1 addition & 2 deletions

File tree

‎invcon/daikon/Daikon.py‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -149,8 +149,7 @@ def getContractDtraces(contractName, contractStorageObject):
149149

150150

151151
def inferLikelyInvaraints(data_trace_file, invariant_file):
152-
cmd = f"""export DAIKONDIR=/app/daikon-5.8.6/daikon-5.8.6
153-
java -cp $DAIKONDIR/daikon.jar daikon.Daikon --config_option daikon.inv.binary.sequenceScalar.SeqBigIntGreaterEqual.enabled=false --config_option daikon.inv.binary.sequenceScalar.SeqBigIntGreaterThan.enabled=false --config_option daikon.inv.binary.sequenceScalar.SeqBigIntLessEqual.enabled=false --config_option daikon.inv.binary.sequenceScalar.SeqBigIntLessThan.enabled=false --config_option daikon.inv.binary.twoScalar.BigIntGreaterEqual.enabled=false --config_option daikon.inv.binary.twoScalar.BigIntGreaterThan.enabled=true --config_option daikon.inv.binary.twoScalar.BigIntLessEqual.enabled=true --config_option daikon.inv.binary.twoScalar.BigIntNonEqual.enabled=false --config_option daikon.inv.binary.twoScalar.BigIntEqual.enabled=true --config_option daikon.inv.binary.twoScalar.BigIntLessThan.enabled=true --config_option daikon.inv.binary.twoScalar.LinearBinaryBigInt.enabled=false --config_option daikon.derive.unary.SequenceSum.enabled=true --config_option daikon.derive.ternary.InvConUserBookkeeping.enabled=true --config_option daikon.derive.senary.InvConUserBookkeeping2.enabled=true --config_option daikon.VarInfo.declared_type_comparability=false --config_option daikon.PptRelation.enable_object_user=false --config_option daikon.PptTopLevel.pairwise_implications=false --config_option daikon.Debug.logDetail=true --config_option daikon.Daikon.undo_opts=false --config_option daikon.PptSliceEquality.set_per_var=false --config_option daikon.DynamicConstants.use_dynamic_constant_optimization=true --config_option daikon.inv.filter.ParentFilter.enabled=true --config_option daikon.inv.filter.DerivedParameterFilter.enabled=false --config_option daikon.inv.filter.ObviousFilter.enabled=true --config_option daikon.inv.filter.UnmodifiedVariableEqualityFilter.enabled=true --config_option daikon.inv.filter.UnjustifiedFilter.enabled=true --config_option daikon.inv.filter.ReadonlyPrestateFilter.enabled=false --config_option daikon.inv.binary.twoString.StringLessEqual.enabled=false --config_option daikon.inv.binary.twoString.StringGreaterEqual.enabled=false --config_option daikon.inv.binary.twoString.StringLessThan.enabled=false --config_option daikon.inv.binary.twoString.StringGreaterThan.enabled=false --config_option daikon.inv.binary.twoScalar.NumericBigInt.Divides.enabled=false --config_option daikon.inv.binary.sequenceScalar.MemberBigInt.enabled=false --config_option daikon.inv.binary.sequenceString.MemberString.enabled=false --config_option daikon.inv.unary.scalar.OneOfBigInt.enabled=true --config_option daikon.inv.unary.sequence.EltOneOfBigInt.enabled=false --config_option daikon.inv.unary.stringsequence.EltOneOfString.enabled=false --config_option daikon.inv.unary.stringsequence.OneOfStringSequence.enabled=false --config_option daikon.inv.unary.sequence.OneOfSequence.enabled=false --config_option daikon.inv.unary.sequence.OneOfBigIntSequence.enabled=false --config_option daikon.inv.unary.string.OneOfString.enabled=false --config_option daikon.derive.unary.SequenceLength.enabled=false --config_option daikon.derive.unary.StringLength.enabled=false {data_trace_file} -o {invariant_file}.gz > {invariant_file} """
152+
cmd = f"""java -cp /app/daikon-5.8.6/daikon.jar daikon.Daikon --config_option daikon.inv.binary.sequenceScalar.SeqBigIntGreaterEqual.enabled=false --config_option daikon.inv.binary.sequenceScalar.SeqBigIntGreaterThan.enabled=false --config_option daikon.inv.binary.sequenceScalar.SeqBigIntLessEqual.enabled=false --config_option daikon.inv.binary.sequenceScalar.SeqBigIntLessThan.enabled=false --config_option daikon.inv.binary.twoScalar.BigIntGreaterEqual.enabled=false --config_option daikon.inv.binary.twoScalar.BigIntGreaterThan.enabled=true --config_option daikon.inv.binary.twoScalar.BigIntLessEqual.enabled=true --config_option daikon.inv.binary.twoScalar.BigIntNonEqual.enabled=false --config_option daikon.inv.binary.twoScalar.BigIntEqual.enabled=true --config_option daikon.inv.binary.twoScalar.BigIntLessThan.enabled=true --config_option daikon.inv.binary.twoScalar.LinearBinaryBigInt.enabled=false --config_option daikon.derive.unary.SequenceSum.enabled=true --config_option daikon.derive.ternary.InvConUserBookkeeping.enabled=true --config_option daikon.derive.senary.InvConUserBookkeeping2.enabled=true --config_option daikon.VarInfo.declared_type_comparability=false --config_option daikon.PptRelation.enable_object_user=false --config_option daikon.PptTopLevel.pairwise_implications=false --config_option daikon.Debug.logDetail=true --config_option daikon.Daikon.undo_opts=false --config_option daikon.PptSliceEquality.set_per_var=false --config_option daikon.DynamicConstants.use_dynamic_constant_optimization=true --config_option daikon.inv.filter.ParentFilter.enabled=true --config_option daikon.inv.filter.DerivedParameterFilter.enabled=false --config_option daikon.inv.filter.ObviousFilter.enabled=true --config_option daikon.inv.filter.UnmodifiedVariableEqualityFilter.enabled=true --config_option daikon.inv.filter.UnjustifiedFilter.enabled=true --config_option daikon.inv.filter.ReadonlyPrestateFilter.enabled=false --config_option daikon.inv.binary.twoString.StringLessEqual.enabled=false --config_option daikon.inv.binary.twoString.StringGreaterEqual.enabled=false --config_option daikon.inv.binary.twoString.StringLessThan.enabled=false --config_option daikon.inv.binary.twoString.StringGreaterThan.enabled=false --config_option daikon.inv.binary.twoScalar.NumericBigInt.Divides.enabled=false --config_option daikon.inv.binary.sequenceScalar.MemberBigInt.enabled=false --config_option daikon.inv.binary.sequenceString.MemberString.enabled=false --config_option daikon.inv.unary.scalar.OneOfBigInt.enabled=true --config_option daikon.inv.unary.sequence.EltOneOfBigInt.enabled=false --config_option daikon.inv.unary.stringsequence.EltOneOfString.enabled=false --config_option daikon.inv.unary.stringsequence.OneOfStringSequence.enabled=false --config_option daikon.inv.unary.sequence.OneOfSequence.enabled=false --config_option daikon.inv.unary.sequence.OneOfBigIntSequence.enabled=false --config_option daikon.inv.unary.string.OneOfString.enabled=false --config_option daikon.derive.unary.SequenceLength.enabled=false --config_option daikon.derive.unary.StringLength.enabled=false {data_trace_file} -o {invariant_file}.gz > {invariant_file} """
154153
status = os.system(cmd)
155154
print(status)
156155
print(f"finished!\n please check invariant file: {invariant_file}")

0 commit comments

Comments
 (0)