Add \lhost_read and \lhost_written to the documentation

README.md

@@ -132,16 +132,21 @@ hold. It can be one of the following :
     `meta lenient` to its contract, in case the invariant needs to be locally
     broken.
 - `\writing` : `P` is to be valid each time the memory is written to in the body
-  of the target function. In this context, `P` can use the `\written`
-  meta-variable, which is the address of the location (or set of locations) being modified.
-  + By default, if `f` calls `g` and `g` has no definition, every state 
+  of the target function. In this context, `P` can use the following metavariables:
+  - `\written`, which is the address of the location (or set of locations) being modified;
+  - `\lhost_written`, which is the address of the base object (i.e with fields and array
+    indices removed) of the location(s) being modified.
+  
+  Prototypes without a definition lead to a special treatment:
+  + By default, if `f` calls `g` and `g` has no definition, every state
     modification that could happen in `g` (according to its `assigns`
     specification) is considered by being **equivalent to assignements in the
     body of `f`** and thus will be checked.
   + In that case, if `g` does not specify a memory footprint, it is **assumed** that it
     respects all related meta-properties.
   + This can be disabled with option `-meta-no-check-ext`
-- `\reading` : symmetrical to `\writing`. `P` can use the `\read` variable.
+- `\reading` : symmetrical to `\writing`. `P` can use the `\read` and `\lhost_read`
+    meta-variables.
   + Undefined callees are checked using their `\from` specification if existing.
 - `\calling` : the property must hold at each function call and can refer to the
   `\called` variable.