GitLab

Fix the case of the wp formula for load, by changing the representation of wp_expr (adding MapstoStarFull constructor).

work in progress on adding wp for sequence and alloc. The sequence actually results in some issues with management of the environement

- Use the level resource algebra/lattice.
  This allows us to unlock partially owned locations
- Upclose the mapsto predicates.
  This allows us to "downgrade" unlocked locations.

corretness for vcg_wp and optimize. Some admits remain in relation with level management. The issue with the fractions has to be resolved (see definition of optimize)

rename inhale/exhale -> MapstoStar/MapstoWand (and corresponding functions). Add definition of vcg_wp for Store,Load,BinOp and Ret.

wip on combine function (need for vcg_sp) : need to check the new definition of vcg_sp and reprove the correctness of vcg_wp; NB: combine_function is implemented in an inefficient way (should be reimplemented using sorting functions on lists)