Minor fix to simpl_typed_mapsto; new entail_examples2

git-svn-id: https://svn.princeton.edu/appel/vst@5825 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Improve "findvars" (part of "go_lower") so that it does not
require "name" hypotheses as it did before (though those 
are still recommended to help it choose better names).

Clean up "new_store_tac" by removing dead stuff.


git-svn-id: https://svn.princeton.edu/appel/vst@5826 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
New file "globals_lemmas.v" to deal with automation and lemmas
for extern global variables (and initializers).

Cleanup and generalize "new_store_tac", now handles stores
to general l-values where it didn't before.


git-svn-id: https://svn.princeton.edu/appel/vst@5827 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
more cleanup of new_store tac.

Also, bring verif_sumarray and verif_message up to date with
recent changes to treatment of extern global variables.


git-svn-id: https://svn.princeton.edu/appel/vst@5828 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
In forward.v:
New "no_loads_expr" to give better diagnostic message to user
in case of trying to have memory references within a right-hand-side
that is supposed to be pure.

In globals_lemmas.v:
New lemmas and tactics for automatically expanding globvar2pred
into typed_mapsto_.


git-svn-id: https://svn.princeton.edu/appel/vst@5829 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Bring up to date with CompCert 2.1, and this will be VST 1.2

git-svn-id: https://svn.princeton.edu/appel/vst@5830 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Lots of progress on nicer processing of the separation logic
for external global variables and their initializers (main_pre).


git-svn-id: https://svn.princeton.edu/appel/vst@5831 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Minor fix to fancy_intro tactic;
new elim_globals_only and elim_globals_only' lemmas;
more things marked "computable" (so entailer computes them automatically);
cleaned up verif_revarray.


git-svn-id: https://svn.princeton.edu/appel/vst@5832 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Clean up all the function-call tactics in forward.v

git-svn-id: https://svn.princeton.edu/appel/vst@5833 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Little tweak to prop_right_solve;  better handling of extern initialized arrays

git-svn-id: https://svn.princeton.edu/appel/vst@5834 e2b0c78b-04ed-0310-b50c-832c51d4eb4a