diff --git a/Makefile.in b/Makefile.in index 7c7badc4debe8619a15e87af5dd350a93aa2bae7..fa61c90f0e2cf3365f9db3a007b6875cee1f9845 100644 --- a/Makefile.in +++ b/Makefile.in @@ -89,7 +89,7 @@ install:: install-sharedir ifneq ("$(FRAMAC_INTERNAL)","yes") -VERSION=0.0 +VERSION=0.2 EXTRAVERSION?= OPEN_SOURCE?=yes diff --git a/opam b/opam index 0353330bcff1358843e7f5d7c3fdec0867b96cd4..febc487498190428f6d22122e03d14adfb87498a 100644 --- a/opam +++ b/opam @@ -1,7 +1,7 @@ opam-version: "2.0" name: "frama-c-metacsl" synopsis: "MetACSL plugin of Frama-C for writing pervasives properties" -version: "0.0" +version: "0.2" 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 @@ -9,12 +9,12 @@ of functions). It will then generate all the corresponding ACSL annotations, leaving it to analysis plug-ins (e.g. WP) to prove the resulting clauses. """ -maintainer: "virgile.robles@cea.fr" +maintainer: "virgile.prevosto@cea.fr" authors: [ "Virgile Robles" ] -homepage: "http://frama-c.com/" -license: "LGPLv2.1" +homepage: "https://frama-c.com/" +license: "LGPL-2.1-only" dev-repo: "git+https://git.frama-c.com/pub/meta.git" bug-reports: "https://git.frama-c.com/pub/meta/-/issues" tags: [ @@ -25,7 +25,7 @@ tags: [ ] build: [ - ["autoconf"] {pinned} + ["autoconf"] {dev} ["./configure"] [make "-j%{jobs}%"] ] @@ -35,7 +35,11 @@ install: [ ] depends: [ - "ocaml" { >= "4.05.0" & ( < "4.08.0~" | >= "4.08.1" ) } - "frama-c" { >= "22.0+dev" } - "why3" { >= "1.4.0" } + "ocaml" { >= "4.08.1" } + "frama-c" { >= "24.0" & < "25.0" } + "why3" { >= "1.3.1" } ] + +depopts: [ "conf-swi-prolog" ] + +messages: [ "Note that if you wish to use the deduction features of MetAcsl, you must install the conf-swi-prolog package (and swi-prolog itself)" {!conf-swi-prolog:installed} ]