34 lines
1.4 KiB
Plaintext
34 lines
1.4 KiB
Plaintext
rule rule1 :=
|
|
for (!pc: int) in pcsForOpcode(CALL)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size > 3
|
|
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);
|
|
|
|
rule rule2 :=
|
|
for (!pc: int) in pcsForOpcode(CALL)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv: array<AbsDom>, ?r: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size > 3,
|
|
Halt{}(?storInv,?r,true)
|
|
=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);
|
|
|
|
rule rule3 :=
|
|
for (!pc: int) in pcsForOpcode(CALL)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size > 3,
|
|
isAbstract(select ?sa (?size - 4))
|
|
=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl);
|
|
|
|
rule rule4 :=
|
|
for (!pc: int) in pcsForOpcode(CALL)
|
|
clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?storInv: array<AbsDom>, ?r: AbsDom]
|
|
ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
|
|
?size > 3,
|
|
?p = select ?sa (?size - 4),
|
|
isConcrete(?p),
|
|
extractConcrete(?p) >= 0,
|
|
Halt(?storInv, ?r, true)
|
|
=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, store ?mem (extractConcrete (?p)) ?r, ?in, [@T], ?cl);
|