Skip to content
Snippets Groups Projects
refinedc.opam 898 B
Newer Older
Michael Sammler's avatar
Michael Sammler committed
opam-version: "2.0"
name: "refinedc"
synopsis: "RefinedC verification framework"
description: """
RefinedC is a framework for verifying idiomatic, low-level C code using a
combination of refinement types and ownership types.
"""
Michael Sammler's avatar
Michael Sammler committed
license: "BSD"

maintainer: ["Michael Sammler <msammler@mpi-sws.org>"
             "Rodolphe Lepigre <lepigre@mpi-sws.org>"]
authors: ["Michael Sammler" "Rodolphe Lepigre" "Kayvan Memarian"]

homepage: "https://plv.mpi-sws.org/refinedc"
Michael Sammler's avatar
Michael Sammler committed
bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"

depends: [
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
  "coq" { (>= "8.12.0" & < "8.13~") }
Michael Sammler's avatar
Michael Sammler committed
  "coq-iris" { (= "dev.2021-02-16.2.075ce23b") | (= "dev") }
  "dune" {>= "2.7.0"}
  "cerberus" {= "~dev"}
  "cmdliner" {>= "1.0.4"}
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
  "earley" {= "3.0.0"}
build: [
  ["dune" "subst"] {pinned}
  ["dune" "build" "-p" name "-j" jobs]
]