Given our program and its Control Flow Graph, implement some form of basic analysis:
Blocks are analyzed by taking the first non-empty post-condition starting from the bottom of the block.
We apply the function of analysis of atomic command, thus extracting preconditions in sequence.
Once we reach the top of the block, we generate n analyses in parallel, one for each predecessor of our block.
These analyses will copy the topmost precondition of the previous block in the last postcondition of the block the jump to, and repeat the analysis from there.
When spawning new analyses, we check that we haven't visited too often the block we are jumping to in our whole path. For now this limit can be enforced by setting a recursion limit.
The analysis stops at the recursion limit or when reaching the topmost block. In future it may be necessary to evaluate if a precondition is never satisfied (equals to false) and so the analysis can be dropped.
Given our program and its Control Flow Graph, implement some form of basic analysis:
nanalyses in parallel, one for each predecessor of our block.When spawning new analyses, we check that we haven't visited too often the block we are jumping to in our whole path. For now this limit can be enforced by setting a recursion limit.
The analysis stops at the recursion limit or when reaching the topmost block. In future it may be necessary to evaluate if a precondition is never satisfied (equals to false) and so the analysis can be dropped.