anil.recoil.org / opam-repository
this repo has no description
fork atom

[new release] memcad 1.1.0 (#19786)

* [new release] memcad 1.1.0

This PR provides a new release for memcad static analyzer.

- Modifications with an impact on the analysis precision, performance, and
domain of applications:

- Support for set parameters in inductive predicates:
MemCAD now supports inductive predicates with constraints over sets,
that can be passed as an argument to inductive predicates. This makes
it possible for the analysis to reason over the preservation of the
set of elements stored in a structure, or to reason over some shared
data-structures. Handling of set parameters relies on a novel set
abstract domain. MemCAD can use a wide range of set abstract domains.
By default, it uses the external library setr.

- Partial support for sequence parameters in inductive predicates:
MemCAD now supports inductive predicates with constraints over
sequences of elements. This makes it possible for the analysis to
reason over properties such as the preservation of the ordering of
the elements in a data-structure or their correct sorting. Handling
of constraints over sequence parameters relies on a novel sequence
abstract domain.

- Clean up of the sub-memory abstract domain:
MemCAD incorporates an abstract domain to reason over data-structures
stored inside other data-structures, such as a list the elements of
which live in a static array. The precision of this abstract domain
operations has been improved, which should make the verification of
larger families of programs possible.

- Novel abstract domain for specific patters of sub-memories:
A novel abstract domain has been added to MemCAD, so as to support
specific instances of nested data-structures, of more simple form
than the ones addressed by the sub-memory abstract domain mentioned
above. While its scope is restricted, it enables the verification
of some families of operating system code such as basic drivers or
memory allocators.

- Value abstract domain for optional values:
The above abstract domain needs to express properties about optional
values, in the sence of the option type in OCaml. A dedicated abstract
domain provides support for optional scalar values.

- Internal changes, that should not be observable when using the analysis,
but with an impact on code quality and maintenance:

- Refactoring of the data-type that describes symbolic variables.

- General management of the set and sequence symbolic variables under a
common umbrella referred to as "collection variables".

- Refactoring of all the printers used in the analysis, using the
formatter interface.

* Update version dependencies for clangml-transforms

* Remove light-uninstall

* Tighter constraint for clangml version

* Add explicit dependency to dune

* Remove obuild dependency

* memcad.1.1.0: Fix opam syntax

* Fix version constraints

* Fix version constraints for setr and apron

* Add version constraint for mlbdd

Co-authored-by: Kate <kit.ty.kate@disroot.org>

thierry-martinez ed5ed752 fbf79f05

options
unified split
Changed files
+46 -2
packages
clangml-transforms
clangml-transforms.0.26
opam
memcad
memcad.1.1.0
opam
+2 -2
packages/clangml-transforms/clangml-transforms.0.26/opam 
···

       
7

       
7

       
 

       
doc: "https://gitlab.inria.fr/memcad/clangml-transforms"


     

       
8

       
8

       
 

       
bug-reports: "https://gitlab.inria.fr/memcad/clangml-transforms/issues"


     

       
9

       
9

       
 

       
depends: [


     

       
10

       

       
-

       
  "ocaml" {>= "4.03.0" & < "4.12.0"}


     

       

       
10

       
+

       
  "ocaml" {>= "4.08.0"}


     

       
11

       
11

       
 

       
  "dune" {>= "1.11.0"}


     

       
12

       

       
-

       
  "clangml" {>= "4.2.0"}


     

       

       
12

       
+

       
  "clangml" {>= "4.4.0"}


     

       
13

       
13

       
 

       
  "dolog" {>= "4.0.0" & < "5.0.0"}


     

       
14

       
14

       
 

       
  "traverse" {>= "0.2.0"}


     

       
15

       
15

       
 

       
  "refl" {>= "0.2.1"}
+44
packages/memcad/memcad.1.1.0/opam 
···

       

       
1

       
+

       
opam-version: "2.0"


     

       

       
2

       
+

       
maintainer: "Xavier.Rival@ens.fr"


     

       

       
3

       
+

       
authors: "Xavier Rival et. al."


     

       

       
4

       
+

       
homepage: "https://www.di.ens.fr/~rival/memcad.html"


     

       

       
5

       
+

       
bug-reports: "https://gitlab.inria.fr/memcad/memcad/-/issues"


     

       

       
6

       
+

       
dev-repo: "git+https://gitlab.inria.fr/memcad/memcad.git"


     

       

       
7

       
+

       
license: "GPL-3.0-only"


     

       

       
8

       
+

       
build: [


     

       

       
9

       
+

       
  ["dune" "subst"] {dev}


     

       

       
10

       
+

       
  [


     

       

       
11

       
+

       
    "dune"


     

       

       
12

       
+

       
    "build"


     

       

       
13

       
+

       
    "-p"


     

       

       
14

       
+

       
    name


     

       

       
15

       
+

       
    "-j"


     

       

       
16

       
+

       
    jobs


     

       

       
17

       
+

       
    "@install"


     

       

       
18

       
+

       
    "@runtest" {with-test}


     

       

       
19

       
+

       
    "@doc" {with-doc}


     

       

       
20

       
+

       
  ]


     

       

       
21

       
+

       
]


     

       

       
22

       
+

       
depends: [


     

       

       
23

       
+

       
  "ocaml" {>= "4.08.0"}


     

       

       
24

       
+

       
  "apron" {>= "v0.9.12"}


     

       

       
25

       
+

       
  "base-unix"


     

       

       
26

       
+

       
  "bdd"


     

       

       
27

       
+

       
  "clangml" {>= "4.4.0"}


     

       

       
28

       
+

       
  "clangml-transforms" {>= "0.26"}


     

       

       
29

       
+

       
  "conf-graphviz"


     

       

       
30

       
+

       
  "dune" {>= "1.3"}


     

       

       
31

       
+

       
  "ounit"


     

       

       
32

       
+

       
  "parmap"


     

       

       
33

       
+

       
  "qtest"


     

       

       
34

       
+

       
  "mlbdd" {>= "0.5"}


     

       

       
35

       
+

       
  "setr" {>= "0.1.1"}


     

       

       
36

       
+

       
]


     

       

       
37

       
+

       
synopsis: "The MemCAD analyzer"


     

       

       
38

       
+

       
description: """


     

       

       
39

       
+

       
MemCAD is an abstract interpreter for shape analysis.


     

       

       
40

       
+

       
MemCAD can analyze C programs manipulating complex data structures."""


     

       

       
41

       
+

       
url {


     

       

       
42

       
+

       
  src: "https://gitlab.inria.fr/memcad/memcad/-/archive/v1.1.0/memcad-v1.1.0.tar.gz"


     

       

       
43

       
+

       
  checksum: "sha512=7e37933fb3c2b67d166906f1ac38855b6819d4ce8f015f84b98012a513cf254eea5081b5d37fe69689dead565f8a1973418a023c9cee76426a5bdb93815c681f"


     

       

       
44

       
+

       
}