Merge remote-tracking branch 'origin/master' into feature/dune/devel_tools

CHANGELOG.md

-# Current development
+# Version 0.3
+
+- compatibility with Frama-C 25.0 Manganese
+
+# Version 0.2
 
 - add warning category `unknown-func` which aborts by default
 - add `\func` meta-variables in all contexts

README.md

@@ -7,8 +7,17 @@ constraints easily.  For more information, see [[2]](#paper).
 
 ## Installation
 
-If your Frama-C is installed via `opam`, you just have to run `opam install .`  
-Otherwise, run the usual `autoconf && ./configure && make && make install`
+You can install a stable version of MetAcsl through [`opam`](https://opam.ocaml.org) (package `frama-c-metacsl`).
+
+If you want to compile it manually from the git repository, you need to have Frama-C installed,
+and to ensure that the MetAcsl branch you intend to work on is compatible with it
+(NB: the `master` branches from both repositories are supposed to stay synchronized).
+
+Optional dependencies, needed for using the [deduction](#deduction) capabilities of MetAcsl include:
+- [Why3](https://why3.lri.fr) (only for checking the consistency of MetAcsl's deduction model)
+- [SWI Prolog](https://www.swi-prolog.org/)
+
+Then, run the usual `autoconf && ./configure && make && make install`
 
 ## Usage
 
@@ -333,7 +342,7 @@ particular may pose problem. If a limit on the size of the set can be
 determined, on can use `-meta-static-bindings L` to use static arrays of size L
 instead.
 
-### Deduction (experimental) 
+### Deduction (experimental) <a name="deduction"></a>
 
 In some specific cases, MetAcsl is able to deduce a meta-property from others.
 Such a deduction must be manually requested by the `proof:deduce` flag. For the

frama-c-metacsl.opam

@@ -36,7 +36,7 @@ build: [
 ]
 name: "frama-c-metacsl"
 synopsis: "MetACSL plugin of Frama-C for writing pervasives properties"
-version: "0.2"
+version: "0.3+dev"
 description:"""
 MetACSL let users write properties that need to be checked at particular
 contexts (e.g. each time a location is written to inside a given set

frama-c-metacsl.opam.template

 name: "frama-c-metacsl"
 synopsis: "MetACSL plugin of Frama-C for writing pervasives properties"
-version: "0.2"
+version: "0.3+dev"
 description:"""
 MetACSL let users write properties that need to be checked at particular
 contexts (e.g. each time a location is written to inside a given set