At the moment the detection of loop in SafeLoopBound is not fully implemented.
What has to be implemented is a check whether the path can be reproduced.
This requires modifications of WPreSeqSeg to include the pre-conditions on the size of the stack (operands and capacity) along with the optional conditions on the stack element values.
First step is:
fix the computation of WpreSeqSeg
add an iteration to test all the previous nodes that have the same PC.
At the moment the detection of loop in
SafeLoopBound
is not fully implemented. What has to be implemented is a check whether the path can be reproduced.This requires modifications of
WPreSeqSeg
to include the pre-conditions on the size of the stack (operands and capacity) along with the optional conditions on the stack element values.First step is:
WpreSeqSeg