diff --git a/dune-project b/dune-project index ea7a8a0ad687c7cdae67e517206fdc30736c44d9..552ba2100cf43c5b20af103e80292eb4da0f2819 100644 --- a/dune-project +++ b/dune-project @@ -29,8 +29,8 @@ (package (name frama-c-metacsl) (depends - (ocaml (>= 4.08.1)) - (frama-c (and (>= 26.0~) (< 27.0~))) + (ocaml (>= 4.11.1)) + (frama-c (and (>= 27.0~) (< 28.0~))) ) (depopts conf-swi-prolog ; for the deduction features of MetAcsl diff --git a/frama-c-metacsl.opam b/frama-c-metacsl.opam index 2433cc1efc6549836690c80c5d3374cd3c64b212..879384e68cfc6589d857a860a9cfe8ab8fef1902 100644 --- a/frama-c-metacsl.opam +++ b/frama-c-metacsl.opam @@ -10,8 +10,8 @@ tags: [ ] depends: [ "dune" {>= "3.2"} - "ocaml" {>= "4.08.1"} - "frama-c" {>= "26.0~" & < "27.0~"} + "ocaml" {>= "4.11.1"} + "frama-c" {>= "27.0~" & < "28.0~"} "odoc" {with-doc} ] depopts: [ @@ -36,7 +36,7 @@ build: [ ] name: "frama-c-metacsl" synopsis: "MetAcsl plugin of Frama-C for writing pervasives properties" -version: "0.4+dev" +version: "0.5~beta" 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 diff --git a/frama-c-metacsl.opam.template b/frama-c-metacsl.opam.template index 9436f72c84bed56573140f9a95de8037fa675022..aeed39fae90d19f554610c77b723cc90178c3f65 100644 --- a/frama-c-metacsl.opam.template +++ b/frama-c-metacsl.opam.template @@ -1,6 +1,6 @@ name: "frama-c-metacsl" synopsis: "MetAcsl plugin of Frama-C for writing pervasives properties" -version: "0.4+dev" +version: "0.5~beta" 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 diff --git a/tests/wp-cache/cache/02ec56fcf1c1a815b7db564e0b1f8eed.json b/tests/wp-cache/cache/02ec56fcf1c1a815b7db564e0b1f8eed.json new file mode 100644 index 0000000000000000000000000000000000000000..23b23de787fd95a231c0d08ed688b6e246061d79 --- /dev/null +++ b/tests/wp-cache/cache/02ec56fcf1c1a815b7db564e0b1f8eed.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.4.3", "verdict": "valid", "time": 0.0047, + "steps": 29 } diff --git a/tests/wp-cache/cache/243a414ad350253fcde34ef28d4b0805.json b/tests/wp-cache/cache/243a414ad350253fcde34ef28d4b0805.json new file mode 100644 index 0000000000000000000000000000000000000000..d00ca4f95414edc75334a392d0a2efbd67a2ecaa --- /dev/null +++ b/tests/wp-cache/cache/243a414ad350253fcde34ef28d4b0805.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.4.3", "verdict": "valid", "time": 0.0126, + "steps": 158 } diff --git a/tests/wp-cache/cache/29fae1b03ae769dd9d5227abcf97e182.json b/tests/wp-cache/cache/29fae1b03ae769dd9d5227abcf97e182.json new file mode 100644 index 0000000000000000000000000000000000000000..17f432df24ba72eabdc6c54c9f0e2192ecf4f40d --- /dev/null +++ b/tests/wp-cache/cache/29fae1b03ae769dd9d5227abcf97e182.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.4.3", "verdict": "valid", "time": 0.0124, + "steps": 47 } diff --git a/tests/wp-cache/cache/3cc18422e0c163603d7aff88afcb9de5.json b/tests/wp-cache/cache/3cc18422e0c163603d7aff88afcb9de5.json new file mode 100644 index 0000000000000000000000000000000000000000..3533675b4800e864c584f1a8b81c74e2db2f9b76 --- /dev/null +++ b/tests/wp-cache/cache/3cc18422e0c163603d7aff88afcb9de5.json @@ -0,0 +1 @@ +{ "prover": "Alt-Ergo:2.4.3", "verdict": "timeout", "time": 1. } diff --git a/tests/wp-cache/cache/60c47cb034783c49959264a81c38fb59.json b/tests/wp-cache/cache/60c47cb034783c49959264a81c38fb59.json new file mode 100644 index 0000000000000000000000000000000000000000..3533675b4800e864c584f1a8b81c74e2db2f9b76 --- /dev/null +++ b/tests/wp-cache/cache/60c47cb034783c49959264a81c38fb59.json @@ -0,0 +1 @@ +{ "prover": "Alt-Ergo:2.4.3", "verdict": "timeout", "time": 1. } diff --git a/tests/wp-cache/cache/662be506be96b93077371c9197816490.json b/tests/wp-cache/cache/662be506be96b93077371c9197816490.json new file mode 100644 index 0000000000000000000000000000000000000000..3533675b4800e864c584f1a8b81c74e2db2f9b76 --- /dev/null +++ b/tests/wp-cache/cache/662be506be96b93077371c9197816490.json @@ -0,0 +1 @@ +{ "prover": "Alt-Ergo:2.4.3", "verdict": "timeout", "time": 1. } diff --git a/tests/wp-cache/cache/704114ccfd125f30e51abb279169d8ab.json b/tests/wp-cache/cache/704114ccfd125f30e51abb279169d8ab.json new file mode 100644 index 0000000000000000000000000000000000000000..3533675b4800e864c584f1a8b81c74e2db2f9b76 --- /dev/null +++ b/tests/wp-cache/cache/704114ccfd125f30e51abb279169d8ab.json @@ -0,0 +1 @@ +{ "prover": "Alt-Ergo:2.4.3", "verdict": "timeout", "time": 1. } diff --git a/tests/wp-cache/cache/73c1837214ac1fd111f9e883fc89a9c2.json b/tests/wp-cache/cache/73c1837214ac1fd111f9e883fc89a9c2.json new file mode 100644 index 0000000000000000000000000000000000000000..4e879975b26bc75a8c61a98260b475b6078bd70b --- /dev/null +++ b/tests/wp-cache/cache/73c1837214ac1fd111f9e883fc89a9c2.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.4.3", "verdict": "valid", "time": 0.0125, + "steps": 157 } diff --git a/tests/wp-cache/cache/a8e6337cb512c10286c6e1b2f0b2513c.json b/tests/wp-cache/cache/a8e6337cb512c10286c6e1b2f0b2513c.json new file mode 100644 index 0000000000000000000000000000000000000000..649bae581ecc8d898cb18fc592a2f75387600d40 --- /dev/null +++ b/tests/wp-cache/cache/a8e6337cb512c10286c6e1b2f0b2513c.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.4.3", "verdict": "valid", "time": 0.0057, + "steps": 20 } diff --git a/tests/wp-cache/cache/c4706d26672432bc13ae0b4acac5a31b.json b/tests/wp-cache/cache/c4706d26672432bc13ae0b4acac5a31b.json new file mode 100644 index 0000000000000000000000000000000000000000..3533675b4800e864c584f1a8b81c74e2db2f9b76 --- /dev/null +++ b/tests/wp-cache/cache/c4706d26672432bc13ae0b4acac5a31b.json @@ -0,0 +1 @@ +{ "prover": "Alt-Ergo:2.4.3", "verdict": "timeout", "time": 1. } diff --git a/tests/wp-cache/cache/fb37747238b7860c303daac9b3d1f842.json b/tests/wp-cache/cache/fb37747238b7860c303daac9b3d1f842.json new file mode 100644 index 0000000000000000000000000000000000000000..c46f1247d68fe62cd1b57f30b7cb37150b3b61ad --- /dev/null +++ b/tests/wp-cache/cache/fb37747238b7860c303daac9b3d1f842.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.4.3", "verdict": "valid", "time": 0.0047, + "steps": 20 }