Address issue #763, much better diagnostics when applying mkVSU, mkComponent, solve_SF_internal
solve_SF_internal now runs much faster; previously, if the Vprog of the VSU was reordered w.r.r. the Vprog of the semax_body proof (which would almost always be the case), then when applying the semax_body proof there would be a very slow unification.
When the extern initialized global data constains C string constants, the new Lemma globvar2pred_cstring can be very helpful in turning it into a cstring predicate in the program precondition. This is still not applied in an automatic tactic, however.
Address issue #763, much better diagnostics when applying mkVSU, mkComponent, solve_SF_internal
solve_SF_internal now runs much faster; previously, if the Vprog of the VSU was reordered w.r.r. the Vprog of the semax_body proof (which would almost always be the case), then when applying the semax_body proof there would be a very slow unification.
When the extern initialized global data constains C string constants, the new Lemma globvar2pred_cstring can be very helpful in turning it into a cstring predicate in the program precondition. This is still not applied in an automatic tactic, however.