diff --git a/README.md b/README.md
index 939cd4468fcffd2386934ab8a9a1cfb71b6dcd65..0b97c4cd5310ada3e59352a37c1dca364028f880 100644
--- a/README.md
+++ b/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.
diff --git a/meta_annotate.ml b/meta_annotate.ml
index 8f23b9addb9d75cc0f019c6333b069b0f151c21d..fb3814426499c2b5687263d8782a2c6618f6028e 100644
--- a/meta_annotate.ml
+++ b/meta_annotate.ml
@@ -236,6 +236,8 @@ let addr_of_tlval tlval =
   let typ = Cil.typeOfTermLval tlval in
   Logic_utils.mk_logic_AddrOf tlval typ
 
+let addr_of_tlhost (h,_) = addr_of_tlval (h, TNoOffset)
+
 (* Instantiate properties at any call site, replacing \called by
  * the called function. *)
 class calling_visitor flags all_mp table = object (self)
@@ -337,7 +339,12 @@ class writing_visitor flags all_mp table = object(self)
     | TVar lv, _ when flags.simpl && Meta_simplify.is_not_orig_variable lv -> ()
     | written ->
       let addr_term = addr_of_tlval written in
-      let assoc_list = [("\\written", RepVariable addr_term)] in
+      let base_addr_term = addr_of_tlhost written in
+      let assoc_list =
+        [ "\\written", RepVariable addr_term;
+          "\\lhost_written", RepVariable base_addr_term
+        ]
+      in
       List.iter (self # instantiate ~post stmt assoc_list) mp_todo
 
   (* Inspect function specs to see what it assigns and instantiate the
@@ -402,9 +409,13 @@ class reading_visitor flags all_mp table = object (self)
   inherit context_visitor flags all_mp table
 
   (* Instantiates the property while replacing \read terms *)
-  method reading_instance ?post stmt written =
-    let addr_term = addr_of_tlval written in
-    let assoc_list = [("\\read", RepVariable addr_term)] in
+  method reading_instance ?post stmt read =
+    let addr_term = addr_of_tlval read in
+    let base_addr_term = addr_of_tlhost read in
+    let assoc_list =
+      ["\\read", RepVariable addr_term;
+       "\\lhost_read", RepVariable base_addr_term ]
+    in
     List.iter (self#instantiate ~post stmt assoc_list) mp_todo
 
   (* Hashtable : stmt -> set of tlvals used in it. Used to avoid duplicate
diff --git a/meta_parse.ml b/meta_parse.ml
index d95011ce3029c8bd35b0d113d5932836c3ecdfec..26930abbb138a745f5c97951d5caee644dbb0ac7 100644
--- a/meta_parse.ml
+++ b/meta_parse.ml
@@ -88,7 +88,9 @@ let mp_contexts = [
 ]
 let mp_metavariables = [
   "\\written";
+  "\\lhost_written";
   "\\read";
+  "\\lhost_read";
   "\\called";
   "\\called_arg";
   "\\func";
diff --git a/tests/meta/lhost.c b/tests/meta/lhost.c
new file mode 100644
index 0000000000000000000000000000000000000000..1cb4bf5d6cc014cf7424d6fda888c9f60eed3734
--- /dev/null
+++ b/tests/meta/lhost.c
@@ -0,0 +1,41 @@
+/* run.config
+OPT: @META@ @PRINT@
+*/
+
+struct S {
+  unsigned owner;
+  int data;
+};
+
+extern unsigned current_id;
+
+int read(struct S* s) {
+  if (s->owner != current_id) return -1;
+  return s->data;
+}
+
+int write(struct S* s, int val) {
+  if (s->owner != current_id) return -1;
+  s->data = val;
+  return 0;
+}
+
+/*@ meta \prop,
+  \name(only_owner_reads),
+  \targets(\ALL),
+  \context(\reading),
+  \tguard(
+    \assert_type((struct S*)\lhost_read) &&
+    (!\separated(&(\lhost_read->data),\read) ==>
+     \lhost_read->owner == current_id));
+*/
+
+/*@ meta \prop,
+  \name(only_owner_writes),
+  \targets(\ALL),
+  \context(\writing),
+  \tguard(
+    \assert_type((struct S*)\lhost_written) &&
+    (!\separated(&(\lhost_written->data),\written) ==>
+     \lhost_written->owner == current_id));
+*/
diff --git a/tests/meta/oracle/lhost.res.oracle b/tests/meta/oracle/lhost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..95c2a6d20b5379f8e2566cfd005a18737913ea1d
--- /dev/null
+++ b/tests/meta/oracle/lhost.res.oracle
@@ -0,0 +1,48 @@
+[kernel] Parsing lhost.c (with preprocessing)
+[meta] Translation is enabled
+[meta] Will process 2 properties
+[meta] Successful translation
+/* Generated by Frama-C */
+struct S {
+   unsigned int owner ;
+   int data ;
+};
+extern unsigned int current_id;
+
+int read(struct S *s)
+{
+  int __retres;
+  /*@ assert
+      only_owner_reads: meta:
+        ¬\separated(&s->data, &s->owner) ⇒ s->owner ≡ current_id;
+  */
+  if (s->owner != current_id) {
+    __retres = -1;
+    goto return_label;
+  }
+  /*@ assert only_owner_reads: meta: s->owner ≡ current_id; */
+  __retres = s->data;
+  return_label: return __retres;
+}
+
+int write(struct S *s, int val)
+{
+  int __retres;
+  /*@ assert
+      only_owner_reads: meta:
+        ¬\separated(&s->data, &s->owner) ⇒ s->owner ≡ current_id;
+  */
+  if (s->owner != current_id) {
+    __retres = -1;
+    goto return_label;
+  }
+  /*@ assert only_owner_writes: meta: s->owner ≡ current_id; */
+  s->data = val;
+  __retres = 0;
+  return_label: return __retres;
+}
+
+/*@ meta "only_owner_reads"; */
+/*@ meta "only_owner_writes";
+*/
+
diff --git a/tests/wp-cache/cache/0588e618c975117e3785fa4d66fed46f.json b/tests/wp-cache/cache/0588e618c975117e3785fa4d66fed46f.json
new file mode 100644
index 0000000000000000000000000000000000000000..0d952f7ad060b33ff1dad591274b0058f0faac97
--- /dev/null
+++ b/tests/wp-cache/cache/0588e618c975117e3785fa4d66fed46f.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }
diff --git a/tests/wp-cache/cache/13d660fa98b598e2134cd946b0ba2a8a.json b/tests/wp-cache/cache/13d660fa98b598e2134cd946b0ba2a8a.json
new file mode 100644
index 0000000000000000000000000000000000000000..c8cfbc791b361925f2d710c3e0f2a0f9fb25a30a
--- /dev/null
+++ b/tests/wp-cache/cache/13d660fa98b598e2134cd946b0ba2a8a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.0042,
+  "steps": 20 }
diff --git a/tests/wp-cache/cache/2d96805770b0ec5c2f9255ad9a5d7276.json b/tests/wp-cache/cache/2d96805770b0ec5c2f9255ad9a5d7276.json
new file mode 100644
index 0000000000000000000000000000000000000000..f0f9a7ffeac0a74484402549f59baaa7be7e94ac
--- /dev/null
+++ b/tests/wp-cache/cache/2d96805770b0ec5c2f9255ad9a5d7276.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.0127,
+  "steps": 157 }
diff --git a/tests/wp-cache/cache/490d75cd8dab49c2df21e84795e3b74e.json b/tests/wp-cache/cache/490d75cd8dab49c2df21e84795e3b74e.json
new file mode 100644
index 0000000000000000000000000000000000000000..88a2cedc2e65eabf6ae0cdb91ac304b5be3b55b1
--- /dev/null
+++ b/tests/wp-cache/cache/490d75cd8dab49c2df21e84795e3b74e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.0092,
+  "steps": 158 }
diff --git a/tests/wp-cache/cache/512ef9917d88325cb9e069a736fc68f1.json b/tests/wp-cache/cache/512ef9917d88325cb9e069a736fc68f1.json
new file mode 100644
index 0000000000000000000000000000000000000000..0d952f7ad060b33ff1dad591274b0058f0faac97
--- /dev/null
+++ b/tests/wp-cache/cache/512ef9917d88325cb9e069a736fc68f1.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }
diff --git a/tests/wp-cache/cache/561ca350c5a578955503471a70e73595.json b/tests/wp-cache/cache/561ca350c5a578955503471a70e73595.json
new file mode 100644
index 0000000000000000000000000000000000000000..0d952f7ad060b33ff1dad591274b0058f0faac97
--- /dev/null
+++ b/tests/wp-cache/cache/561ca350c5a578955503471a70e73595.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }
diff --git a/tests/wp-cache/cache/7f825a3f0d00a2b9dd277996970ab2b8.json b/tests/wp-cache/cache/7f825a3f0d00a2b9dd277996970ab2b8.json
new file mode 100644
index 0000000000000000000000000000000000000000..0d952f7ad060b33ff1dad591274b0058f0faac97
--- /dev/null
+++ b/tests/wp-cache/cache/7f825a3f0d00a2b9dd277996970ab2b8.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }
diff --git a/tests/wp-cache/cache/85080d53aa62a2fdd83edcfe01fea489.json b/tests/wp-cache/cache/85080d53aa62a2fdd83edcfe01fea489.json
new file mode 100644
index 0000000000000000000000000000000000000000..4e35328529edd4310e1ef8ac4d76676f7494f65e
--- /dev/null
+++ b/tests/wp-cache/cache/85080d53aa62a2fdd83edcfe01fea489.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.0129,
+  "steps": 47 }
diff --git a/tests/wp-cache/cache/8774631f76e90ef51813133252fbb84c.json b/tests/wp-cache/cache/8774631f76e90ef51813133252fbb84c.json
new file mode 100644
index 0000000000000000000000000000000000000000..4ee2aed6d3e13d0f381f74a6653ed0315b0c2e8f
--- /dev/null
+++ b/tests/wp-cache/cache/8774631f76e90ef51813133252fbb84c.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.005,
+  "steps": 29 }
diff --git a/tests/wp-cache/cache/920df4df73bbe741b5b8449893a70e1e.json b/tests/wp-cache/cache/920df4df73bbe741b5b8449893a70e1e.json
new file mode 100644
index 0000000000000000000000000000000000000000..d6ae3eeac467c4c39698f97e0072aa748cab4332
--- /dev/null
+++ b/tests/wp-cache/cache/920df4df73bbe741b5b8449893a70e1e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.008,
+  "steps": 20 }
diff --git a/tests/wp-cache/cache/f20dcefc53944c4ad0a5f8cf9d78a9b5.json b/tests/wp-cache/cache/f20dcefc53944c4ad0a5f8cf9d78a9b5.json
new file mode 100644
index 0000000000000000000000000000000000000000..0d952f7ad060b33ff1dad591274b0058f0faac97
--- /dev/null
+++ b/tests/wp-cache/cache/f20dcefc53944c4ad0a5f8cf9d78a9b5.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }