Module Bap_primus_track_visited

Tracks program terms evaluated by Primus.

This module provides a component and an interface to the visitation tracker that keeps records of all basic block terms visited during Primus evaluation.

During the initialization the component adds all basic blocks that have the visited attribute to the list of already visited blocks. This is done only when the system starts and the visited set is not synchronized anymore. Also, when a Primus system is started, the component will mark with the dead attribute all terms that are not already marked with with the visited attribute.

Finally, when the system is stopped, the component will update the product data structure and mark all terms that was visited during the system run with the visited attribute.

Although the visitation tracks only basic blocks it adds the visited and dead attributes to all subterms of a visited block.

If a function is stubbed then when a stub is invoked the whole body of a function is also marked as visited (and the blocks of the function are added to the visited set).