This module contains the logic of what assertions need to be applied depending on the analysis step.
This module reads the values of the following flags:
For a module:
:- module(_,[p/1],[assertions]). :- pred p(X) => atm(X). p(X) :- X = a.
If fixp_stick_to_success is set to on, the analysis result will be:
:- module(_,[p/1],[assertions]). :- true pred p(X) => atm(X). p(X) :- X = a.
Because the value of the assertion is used as it is. If it is set to off, it will use the assertion only when it allows to gain precision (useless in this case).
:- module(_,[p/1],[assertions,regtypes]). :- true pred p(X) => rta(X). p(X) :- X = a. :- regtype rta/1. rta(a).
For example in the following module:
:- module(_,[main/0,p/1],[assertions]). main :- p(a). :- pred p(X) : atm(X). p(X).
Since the plai does not normalize heads it is imposible to generalize p(a) to p(X) : atm(X), the variables that the abstract substitution approximates must be in the head. However p(X) : rta(X) can be generalized only by changing the abstract substitution because the variable is already in the head.
The fixpoint would have to be modified so that applying assertions can change the goals
NewProj and NewCall are the result of applying the assertions that correspond to the call_to_success analysis point.
Currently, the implementation has only one option which is applying true and trust call assertions, and true success assertions (that are applicable to Sg:Proj).
Succeeds if there are applicable assertions to Sg:Proj understood by domain AbsInt and Prime is the answer pattern.
This predicate succeeds if there are assertions that are applicable to Head:Proj (normalized). If no Sts is specified all trusted status are returned
Joins an abstract success pattern from an assertion with a previous value for the call pattern Head:AsrProj.