Merge branch 'stable/iron'

CHANGELOG.md

+# Version 0.4
+
+- compatibility with Frama-C 26.0 Iron
+- ensure Wookey case study can be handled (with non-free ACSL-importer plug-in)
+
 # Version 0.3
 
 - compatibility with Frama-C 25.0 Manganese

Makefile

@@ -24,6 +24,8 @@
 
 FRAMAC_SHARE:=$(shell frama-c-config -print-share-path)
 
+include $(FRAMAC_SHARE)/Makefile.common
+
 ##########################################################################
 # Build
 

README.md

@@ -11,13 +11,23 @@ You can install a stable version of MetAcsl through [`opam`](https://opam.ocaml.
 
 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).
+(NB: the `master` branches from both repositories are supposed to stay synchronized,
+ as well as any `stable/*` branch).
 
 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`
+Since version 0.4, MetAcsl uses [`dune`](https://dune.build/) as build system (following Frama-C's lead),
+so that you can install MetAcsl with the following commands:
+```
+dune build
+dune install
+```
+
+This will install MetAcsl in the same place as Frama-C.
+
+For convenience, you can still use `make && make install` to perform the same thing.
 
 ## Usage
 

case_studies/wookey/README.md

@@ -5,8 +5,9 @@ To get the wookey source themselves, and configure them so that they are
 ready for analysis, just run `setup.sh` in a repo with no uncommitted change.
 `setup.sh` depends on the software below.
 
-Once setup is done, go to the `loader` directory and do `make gen_prove`
-(assuming you have a working Frama-C installation with MetACSL installed).
+Once setup is done, go to the `loader` directory and do `make loader.meta`
+(assuming you have a working Frama-C installation with MetAcsl installed,
+as well as the proprietary ACSL-Importer plug-in).
 
 ## Dependencies:
 - repo

case_studies/wookey/loader/GNUmakefile

@@ -12,7 +12,8 @@ export FRAMA_C_MEMORY_FOOTPRINT = 8
 # It is an optional include, unnecessary if frama-c is in the PATH
 -include path.mk
 FRAMAC?=frama-c
-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
+FC_SCRIPTS_PATH:=$(shell $(FRAMAC)-config -print-lib-path)/analysis-scripts
+include $(FC_SCRIPTS_PATH)/prologue.mk
 
 #
 ###############################################################################
@@ -114,4 +115,4 @@ clean::
 	rm -rf $(MAIN_TARGET).parse
 	rm -rf $(MAIN_TARGET).meta
 
-include $(shell $(FRAMAC)-config -print-lib-path)/analysis-scripts/epilogue.mk
+include $(FC_SCRIPTS_PATH)/epilogue.mk

dune-project

@@ -30,7 +30,7 @@
 (package (name frama-c-metacsl)
  (depends
   (ocaml (>= 4.08.1))
-  (frama-c (and (>= 24.0) (< 25.0)))
+  (frama-c (and (>= 26.0~) (< 27.0~)))
  )
  (depopts
    conf-swi-prolog  ; for the deduction features of MetAcsl

frama-c-metacsl.opam

@@ -11,7 +11,7 @@ tags: [
 depends: [
   "dune" {>= "3.2"}
   "ocaml" {>= "4.08.1"}
-  "frama-c" {>= "24.0" & < "25.0"}
+  "frama-c" {>= "26.0~" & < "27.0~"}
   "odoc" {with-doc}
 ]
 depopts: [
@@ -35,10 +35,10 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 name: "frama-c-metacsl"
-synopsis: "MetACSL plugin of Frama-C for writing pervasives properties"
-version: "0.3+dev"
+synopsis: "MetAcsl plugin of Frama-C for writing pervasives properties"
+version: "0.4"
 description:"""
-MetACSL let users write properties that need to be checked at particular
+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
 of functions). It will then generate all the corresponding ACSL
 annotations, leaving it to analysis plug-ins (e.g. WP) to prove the

frama-c-metacsl.opam.template

 name: "frama-c-metacsl"
-synopsis: "MetACSL plugin of Frama-C for writing pervasives properties"
-version: "0.3+dev"
+synopsis: "MetAcsl plugin of Frama-C for writing pervasives properties"
+version: "0.4"
 description:"""
-MetACSL let users write properties that need to be checked at particular
+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
 of functions). It will then generate all the corresponding ACSL
 annotations, leaving it to analysis plug-ins (e.g. WP) to prove the