[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 79 from proof validrefs-junkrefs (previous step)

r1 ' + refs1 = refs + r0 ' + refs0, st[r -- i '] = refval(r1), validrefs(str, refs, st[r -- _type] .type .type, st), st[r -- _type] .type ≤ ty, 0 ≤ i, 0 < st[r -- _length] .intval, is_array(str, r, st), i < st[r -- _length] .intval, junkrefs(str, r1 ' + refs1, st[r -- _type] .type .type, st), ¬ is_valid_ref(str, r0, st) ∨ refs = [] ∧ ¬ st[r0 -- _type] .type ≤ st[r -- _type] .type .type ∨ refs ≠ [] ∧ ( is_obj(refs .last, st) ∧ mkfs(class, ty0, fieldvar) ' ∈ instfields(st[refs .last -- _type] .type .class) ∧ is_referencevalue(st[refs .last -- mkfs(class, ty0, fieldvar) ']) ∧ r0 = st[refs .last -- mkfs(class, ty0, fieldvar) '] .refval ∧ ¬ st[st[refs .last -- mkfs(class, ty0, fieldvar) '] .refval -- _type] .type ≤ ty0 ∨ is_array(refs .last, st) ∧ 0 ≤ i0 ∧ i0 < st[refs .last -- _length] .intval ∧ is_referencevalue(st[refs .last -- i0 ']) ∧ r0 = st[refs .last -- i0 '] .refval ∧ ¬ st[st[refs .last -- i0 '] .refval -- _type] .type ≤ st[refs .last -- _type] .type .type) ⊦ r0 = jvmref, r = jvmref, ¬ r1 ∈ refs ∧ r1 ≠ r0 ∧ ¬ r1 ∈ refs0, validrefs(str, r ' + refs, ty, st) ∧ ( ¬ is_valid_ref(str, r0, st) ∨ is_obj((r ' + refs) .last, st) ∧ (∃ fs. fs ' ∈ instfields(st[(r ' + refs) .last -- _type] .type .class) ∧ is_referencevalue(st[(r ' + refs) .last -- fs ']) ∧ r0 = st[(r ' + refs) .last -- fs '] .refval ∧ ¬ st[st[(r ' + refs) .last -- fs '] .refval -- _type] .type ≤ fs .type) ∨ is_array((r ' + refs) .last, st) ∧ (∃ i. ¬ i < 0 ∧ ¬ st[(r ' + refs) .last -- _length] .intval ≤ i ∧ is_referencevalue(st[(r ' + refs) .last -- i ']) ∧ r0 = st[(r ' + refs) .last -- i '] .refval ∧ ¬ st[st[(r ' + refs) .last -- i '] .refval -- _type] .type ≤ st[(r ' + refs) .last -- _type] .type .type))

Heuristic weak cut applied rule cut formula

And obtained the following new goals

Proof step 55:
refs = [], r1 ' + refs1 = refs + r0 ' + refs0, st[r -- i '] = refval(r1), validrefs(str, refs, st[r -- _type] .type .type, st), st[r -- _type] .type ≤ ty, 0 ≤ i, 0 < st[r -- _length] .intval, is_array(str, r, st), i < st[r -- _length] .intval, junkrefs(str, r1 ' + refs1, st[r -- _type] .type .type, st), ¬ is_valid_ref(str, r0, st) ∨ refs = [] ∧ ¬ st[r0 -- _type] .type ≤ st[r -- _type] .type .type ∨ refs ≠ [] ∧ ( is_obj(refs .last, st) ∧ mkfs(class, ty0, fieldvar) ' ∈ instfields(st[refs .last -- _type] .type .class) ∧ is_referencevalue(st[refs .last -- mkfs(class, ty0, fieldvar) ']) ∧ r0 = st[refs .last -- mkfs(class, ty0, fieldvar) '] .refval ∧ ¬ st[st[refs .last -- mkfs(class, ty0, fieldvar) '] .refval -- _type] .type ≤ ty0 ∨ is_array(refs .last, st) ∧ 0 ≤ i0 ∧ i0 < st[refs .last -- _length] .intval ∧ is_referencevalue(st[refs .last -- i0 ']) ∧ r0 = st[refs .last -- i0 '] .refval ∧ ¬ st[st[refs .last -- i0 '] .refval -- _type] .type ≤ st[refs .last -- _type] .type .type) ⊦ r0 = jvmref, r = jvmref, ¬ r1 ∈ refs ∧ r1 ≠ r0 ∧ ¬ r1 ∈ refs0, validrefs(str, r ' + refs, ty, st) ∧ ( ¬ is_valid_ref(str, r0, st) ∨ is_obj((r ' + refs) .last, st) ∧ (∃ fs. fs ' ∈ instfields(st[(r ' + refs) .last -- _type] .type .class) ∧ is_referencevalue(st[(r ' + refs) .last -- fs ']) ∧ r0 = st[(r ' + refs) .last -- fs '] .refval ∧ ¬ st[st[(r ' + refs) .last -- fs '] .refval -- _type] .type ≤ fs .type) ∨ is_array((r ' + refs) .last, st) ∧ (∃ i. ¬ i < 0 ∧ ¬ st[(r ' + refs) .last -- _length] .intval ≤ i ∧ is_referencevalue(st[(r ' + refs) .last -- i ']) ∧ r0 = st[(r ' + refs) .last -- i '] .refval ∧ ¬ st[st[(r ' + refs) .last -- i '] .refval -- _type] .type ≤ st[(r ' + refs) .last -- _type] .type .type))
Proof step 78:
r1 ' + refs1 = refs + r0 ' + refs0, st[r -- i '] = refval(r1), validrefs(str, refs, st[r -- _type] .type .type, st), st[r -- _type] .type ≤ ty, 0 ≤ i, 0 < st[r -- _length] .intval, is_array(str, r, st), i < st[r -- _length] .intval, junkrefs(str, r1 ' + refs1, st[r -- _type] .type .type, st), ¬ is_valid_ref(str, r0, st) ∨ refs = [] ∧ ¬ st[r0 -- _type] .type ≤ st[r -- _type] .type .type ∨ refs ≠ [] ∧ ( is_obj(refs .last, st) ∧ mkfs(class, ty0, fieldvar) ' ∈ instfields(st[refs .last -- _type] .type .class) ∧ is_referencevalue(st[refs .last -- mkfs(class, ty0, fieldvar) ']) ∧ r0 = st[refs .last -- mkfs(class, ty0, fieldvar) '] .refval ∧ ¬ st[st[refs .last -- mkfs(class, ty0, fieldvar) '] .refval -- _type] .type ≤ ty0 ∨ is_array(refs .last, st) ∧ 0 ≤ i0 ∧ i0 < st[refs .last -- _length] .intval ∧ is_referencevalue(st[refs .last -- i0 ']) ∧ r0 = st[refs .last -- i0 '] .refval ∧ ¬ st[st[refs .last -- i0 '] .refval -- _type] .type ≤ st[refs .last -- _type] .type .type) ⊦ refs = [], r0 = jvmref, r = jvmref, ¬ r1 ∈ refs ∧ r1 ≠ r0 ∧ ¬ r1 ∈ refs0, validrefs(str, r ' + refs, ty, st) ∧ ( ¬ is_valid_ref(str, r0, st) ∨ is_obj((r ' + refs) .last, st) ∧ (∃ fs. fs ' ∈ instfields(st[(r ' + refs) .last -- _type] .type .class) ∧ is_referencevalue(st[(r ' + refs) .last -- fs ']) ∧ r0 = st[(r ' + refs) .last -- fs '] .refval ∧ ¬ st[st[(r ' + refs) .last -- fs '] .refval -- _type] .type ≤ fs .type) ∨ is_array((r ' + refs) .last, st) ∧ (∃ i. ¬ i < 0 ∧ ¬ st[(r ' + refs) .last -- _length] .intval ≤ i ∧ is_referencevalue(st[(r ' + refs) .last -- i ']) ∧ r0 = st[(r ' + refs) .last -- i '] .refval ∧ ¬ st[st[(r ' + refs) .last -- i '] .refval -- _type] .type ≤ st[(r ' + refs) .last -- _type] .type .type))

Rule argument

[fma-arg: refs = []]

Additional information

[[CONCRETESIMPRULES : ()], [EXTRAFMAS : (refs = [])]]