You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This program fails to prove the entailment for main.
letcall_retf=
f 100letmain()(*@ ens res=100 @*)=letidi= i in
id 2;
call_ret id
The above program gives the following specification.
ex v21 v22; ens v22=(fun i v15 (*@ ens v15=i @*) -> i); v22(2, v21); ex v19; call_ret(v22, v19); ens res=v19
It fails to prove the entailment because, in the entailment process for main:
(a) id (v22) is unfolded as v22(i,v15) == ens v15=i, giving the specification:
ex v21 v22; ens v22=(fun i v15 (*@ ens v15=i @*) -> i); ens v21=2; ex v19; call_ret(v22, v19); ens res=v19
(b) call_ret is unfolded as call_ret(f,res) == ex v0; f(100, v0); ens res=v0, giving the specification:
ex v19 v22; ens v22=(fun i v15 (*@ ens v15=i @*) -> i); ex v49; v22(100, v49); ens v19=v49; ens res=v19
Here, call_ret has to be unfolded because the inferred specification (in the first step) is not used. But, the unfolding introduces an additional appearance id (v22), and we are required to unfold id (v22) again (I think the only heuristic available for use here is to unfold).
Note (from discussion)
A workaround requires one to provide an explicit specification ex v0; f(100, v0); ens res=v0 to call_ret. This works because we can use the inferred specification directly and avoid an additional unfold of id (v22). Another workaround is to increase the unfolding bound to 2 to accommodate the additional unfolding of id (v22).
Questions
We can use the rec_flag (from parsing) to allow unfolding of non-recursive predicates during the entailment as discussed, or to directly use the inferred specification when analyzing the method.
The text was updated successfully, but these errors were encountered:
I think the way to fix this is to always unfold non-recursive predicates during entailment. Something like this should work:
Add a field to pred_def to say if the predicate is recursive
When we create a pred_def, traverse its disj_spec body (using a visitor like this to visit_HigherOrder) to check if the predicate name occurs in any function stages. We can deal with mutual recursion later.
When we remember which predicates we've unfolded, don't count non-recursive predicates
Issue
This program fails to prove the entailment for
main
.The above program gives the following specification.
It fails to prove the entailment because, in the entailment process for
main
:(a)
id (v22)
is unfolded asv22(i,v15) == ens v15=i
, giving the specification:(b)
call_ret
is unfolded ascall_ret(f,res) == ex v0; f(100, v0); ens res=v0
, giving the specification:Here,
call_ret
has to be unfolded because the inferred specification (in the first step) is not used. But, the unfolding introduces an additional appearanceid (v22)
, and we are required to unfoldid (v22)
again (I think the only heuristic available for use here is to unfold).Note (from discussion)
A workaround requires one to provide an explicit specification
ex v0; f(100, v0); ens res=v0
tocall_ret
. This works because we can use the inferred specification directly and avoid an additional unfold ofid (v22)
. Another workaround is to increase the unfolding bound to 2 to accommodate the additional unfolding ofid (v22)
.Questions
We can use the
rec_flag
(from parsing) to allow unfolding of non-recursive predicates during the entailment as discussed, or to directly use the inferred specification when analyzing the method.The text was updated successfully, but these errors were encountered: