diff --git a/Makefile b/Makefile index bbb4b83aa2938cde51144a7218e0673caa3ae567..5e013647c0d0a9265fa04a0880831238192667bf 100644 --- a/Makefile +++ b/Makefile @@ -24,6 +24,8 @@ FRAMAC_SHARE:=$(shell frama-c-config -print-share-path) +include $(FRAMAC_SHARE)/Makefile.common + ########################################################################## # Build diff --git a/dune-project b/dune-project index 4fe093d66373cbe23a0fbf2722388e6e628546b0..d2233f118f3c6585ea02c0d94ada0cf91b8af1e8 100644 --- a/dune-project +++ b/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 diff --git a/frama-c-metacsl.opam b/frama-c-metacsl.opam index 43308fe22805a9441103d736f80076e88e7a7283..fe5a97fd154f24b01c03a9872ab2a32e87247239 100644 --- a/frama-c-metacsl.opam +++ b/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~beta" 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 diff --git a/frama-c-metacsl.opam.template b/frama-c-metacsl.opam.template index b74abebeffdf9b5c35152c2636475e751436571f..3e1d1c7c7f00ecaa52527f0aefc3f4dce4d6ac54 100644 --- a/frama-c-metacsl.opam.template +++ b/frama-c-metacsl.opam.template @@ -1,8 +1,8 @@ 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~beta" 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