diff --git a/README.md b/README.md index 76cfb40631c2aaebca96e28e296cea06cbdb7c9f..839123047f2f1c1bc5413a732735a18d83566bf9 100644 --- a/README.md +++ b/README.md @@ -68,10 +68,33 @@ the builtin `\ALL` set, the set of every function in the program. One can also use the `\in_file` function to select all functions defined in a given file. +Finally, it is possible to use `\callees(s)` to refer to the functions in `s` and +all their callees recursively. Of course, `\callers(s)` will include `s` and all +their callers recursively up to the main entry point. In presence of function +pointers, MetAcsl will rely on the Callgraph plugin, which either uses the results of Eva +if an analysis has been launched before, or considers the set of all functions that +have a type compatible with the pointer. + For example, the target set `\diff(\ALL, \union({foo, bar}, \in_file("main.c")))` describes all functions except `foo`, `bar` or any function defined in `main.c`. +By default, if a function name does not correspond to a function in the +program under analysis, Frama-C will be aborted. This can be changed by +setting the status of warning category `unknown-func` to a suitable value, +e.g. `-meta-warn-key unknown-func=enable`, to keep a warning when such a +case occurs, or `-meta-warn-key unknown-func=disable` to silently ignore this +fact. + +Note that if you disable the warning in order to use the same meta-properties on +a full code base and on a reduced one where some functions have been removed, the +resulting targets in the reduced case might not be the intersection of the targets +in full case with the functions of the reduced case. For instance, if `f1` calls `f2` +and only `f2` is included in the reduced case, `\callees({f1})` will be the empty set +(since `f1` is ignored as unknown function) in the reduced case, and `{ f1, f2 }` in +the full case. Similarly `\diff(\ALL,\callees({f1}))` will _include_ `f2` in the reduced case, +but not in the full case. + ### Context <a name="context"></a> The context is the situation in a target function in which the property must