From 49546a622ab04cc4e5f8198b1fd24c767a49b7cd Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 28 Apr 2023 14:19:22 +0200
Subject: [PATCH] Add \lhost_read and \lhost_written to the documentation
---
README.md | 13 +++++++++----
1 file changed, 9 insertions(+), 4 deletions(-)
diff --git a/README.md b/README.md
index 939cd44..0b97c4c 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.
--
GitLab