diff --git a/.gitattributes b/.gitattributes
new file mode 100644
index 0000000000000000000000000000000000000000..6d5050fb3d0f15106cae3b59564ae20863992de8
--- /dev/null
+++ b/.gitattributes
@@ -0,0 +1,111 @@
+################
+# MERGE: union #
+################
+
+Changelog merge=union
+
+##################################################
+# BINARY/CHECK-SYNTAX/INDENT/EOL-EOF: set/-unset #
+##################################################
+
+# note: "binary" is a built-in macro that also
+# unsets the "text" and "diff" attributes
+
+# note: set "check-eoleof" and "check-utf8" by default to all files
+* check-eoleof check-utf8
+
+# note: unset "-check-eoleof" and "-check-utf8" for "binary"
+*.gz binary -check-eoleof -check-utf8
+*.svg binary -check-eoleof -check-utf8
+
+###########################################
+# CHECK-SYNTAX/INDENT/EOL-EOF: set/-unset #
+###########################################
+
+*.ml check-syntax check-indent -check-eoleof
+*.mli check-syntax check-indent -check-eoleof
+*.pl check-syntax -check-eoleof
+*.slog check-syntax -check-eoleof
+*.why check-syntax -check-eoleof
+
+#############################################
+# HEADER_SPEC: CEA_LGPL_OR_PROPRIETARY.META #
+#############################################
+
+dune-project header_spec=CEA_LGPL_OR_PROPRIETARY.META
+dune header_spec=CEA_LGPL_OR_PROPRIETARY.META
+
+Make* header_spec=CEA_LGPL_OR_PROPRIETARY.META
+
+*.ml header_spec=CEA_LGPL_OR_PROPRIETARY.META
+*.mli header_spec=CEA_LGPL_OR_PROPRIETARY.META
+
+*.txt header_spec=CEA_LGPL_OR_PROPRIETARY.META
+*.why header_spec=CEA_LGPL_OR_PROPRIETARY.META
+
+/share/run.pl header_spec=CEA_LGPL_OR_PROPRIETARY.META
+/share/model.slog header_spec=CEA_LGPL_OR_PROPRIETARY.META
+
+############################
+# HEADER_SPEC: SETLOG_LGPL #
+############################
+
+/share/setloglib.slog header_spec=SETLOG_LGPL
+/share/setlog_rules.pl header_spec=SETLOG_LGPL
+
+#####################################
+# HEADER_SPEC: SETLOG_LGPL_MODIFIED #
+#####################################
+
+/share/setlog.pl header_spec=SETLOG_LGPL_MODIFIED
+
+########################
+# HEADER_SPEC: .ignore #
+########################
+
+# Binaries
+
+*.gz header_spec=.ignore
+*.svg header_spec=.ignore
+
+# CI
+
+/.gitlab-ci.yml header_spec=.ignore
+/nix/ci.sh header_spec=.ignore
+*.nix header_spec=.ignore
+
+# Doc
+
+CHANGELOG.md header_spec=.ignore
+LICENSE header_spec=.ignore
+SETLOG_LICENSE header_spec=.ignore
+README* header_spec=.ignore
+TODO.md header_spec=.ignore
+VERSION header_spec=.ignore
+
+# Git
+
+.gitattributes header_spec=.ignore
+.gitignore header_spec=.ignore
+.git-blame-ignore-revs header_spec=.ignore
+
+# Headers
+
+/headers/open-source/* header_spec=.ignore
+/headers/close-source/* header_spec=.ignore
+
+# OCaml
+
+.merlin header_spec=.ignore
+.ocp-indent header_spec=.ignore
+*.opam* header_spec=.ignore
+
+# Proofs
+
+/proofs/meta_model/**/*.v header_spec=.ignore
+why3session.xml header_spec=.ignore
+
+# Tests
+
+/case_studies/**/* header_spec=.ignore
+/tests/**/* header_spec=.ignore
diff --git a/.gitignore b/.gitignore
index 89c53125b9f925b2ab8cd9b264ae8b7c6a725ef5..a0adaee8e411eebeb1eca0c408602ac4f3f23d75 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,21 +13,17 @@
*.o
.depend
/*.log
+_build
+.lint
# Configure-generated files
-/Makefile
/autom4te.cache
/config.status
/configure
# Test results and others
-/tests/ptests_config
-/tests/test_config
-/tests/meta/test_config
-/tests/*/result/
-/tests/*/*/result/
-/tests/*/result_*/
-/tests/*/*.opt
+/tests/*/result*/
+/tests/*/oracle*/dune
# Distribution artefacts
/frama-c-metacsl.tar.gz
@@ -77,3 +73,4 @@
/case_studies/wookey/loader/src/types.h
(??)
+/_build/
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 816109aa7bcebd83b8b7ddafe8f6216934ad5387..54914ba31ebb1ff81f28fd4891bc8f49228e93b6 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,10 +1,40 @@
-Tests:
+################################################################################
+### STAGES
+
+stages:
+ - tests
+
+################################################################################
+### DEFAULT JOB PARAMETERS
+
+default:
+ tags: [nix]
+
+################################################################################
+### VARIABLES
+
+variables:
+ DEFAULT: "feature/bobot/jbuilder"
+ OCAML: "4.11"
+
+################################################################################
+### TESTS
+
+build-and-test:
+ stage: tests
+ script:
+ - ./nix/ci.sh
+
+check-headers:
+ stage: tests
+ variables:
+ CI_MODE: "check-headers"
+ script:
+ - ./nix/ci.sh
+
+lint:
+ stage: tests
variables:
- CURRENT: $CI_COMMIT_REF_NAME
- DEFAULT: "master"
- OCAML: "4_08"
- FRAMA_CI_OPT: "--override meta:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
+ CI_MODE: "lint"
script:
- - nix/frama-ci.sh build -A meta.tests
- tags:
- - nix
+ - ./nix/ci.sh
diff --git a/configure.ac b/Makefile
similarity index 61%
rename from configure.ac
rename to Makefile
index e35b2fe1767559e2d918424ffecfe9e9057cae0c..697226722027499e46edf27b4f8b86e91119644e 100644
--- a/configure.ac
+++ b/Makefile
@@ -20,30 +20,45 @@
# #
##########################################################################
-m4_define([plugin_file],Makefile.in)
+.PHONY: all build clean
-m4_define(
- [FRAMAC_SHARE_ENV],
- [m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
+FRAMAC_SHARE:=$(shell frama-c -print-share-path)
-m4_define([FRAMAC_SHARE],
- [m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
- [m4_esyscmd(frama-c -print-path)])])
+##########################################################################
+# Build
+
+all: build frama-c-metacsl.opam
+
+frama-c-metacsl.opam: frama-c-metacsl.opam.template dune-project
+ rm -f $@
+ dune build $@
+
+build::
+ dune build @install
+
+clean:: purge-tests
+ dune clean
+ rm -rf _build .merlin
-m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
+##########################################################################
+# Tests
-check_plugin(metacsl,PLUGIN_RELATIVE_PATH(plugin_file),
- [support for HILARE annotations],yes)
+include ${FRAMAC_SHARE}/Makefile.testing
-configure_tool(SWIPROLOG,swipl,[swiprolog not found],no)
+##########################################################################
+# Install
-plugin_use_external(metacsl,swiprolog)
-plugin_use(metacsl,wp)
+include ${FRAMAC_SHARE}/Makefile.installation
-check_plugin_dependencies
+##########################################################################
+# Headers
-if test "$HAS_SWIPROLOG" = "no"; then
- AC_MSG_WARN([swi-prolog not found. Meta-deduction disabled]);
-fi
+HDRCK_EXTRA:= \
+ -headache-config-file ${FRAMAC_SHARE}/headache_config.txt \
+ -headache-config-file headers/header_config.txt
+include ${FRAMAC_SHARE}/Makefile.headers
+
+##########################################################################
+# Linting
-write_plugin_config(Makefile)
+include ${FRAMAC_SHARE}/Makefile.linting
diff --git a/Makefile.in b/Makefile.in
deleted file mode 100644
index fbb4537ca173ec3679fb2955fa5e32856a53453d..0000000000000000000000000000000000000000
--- a/Makefile.in
+++ /dev/null
@@ -1,135 +0,0 @@
-##########################################################################
-# #
-# This file is part of the Frama-C's MetACSL plug-in. #
-# #
-# Copyright (C) 2018-2022 #
-# CEA (Commissariat à l'énergie atomique et aux énergies #
-# alternatives) #
-# #
-# you can redistribute it and/or modify it under the terms of the GNU #
-# Lesser General Public License as published by the Free Software #
-# Foundation, version 2.1. #
-# #
-# It is distributed in the hope that it will be useful, #
-# but WITHOUT ANY WARRANTY; without even the implied warranty of #
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
-# GNU Lesser General Public License for more details. #
-# #
-# See the GNU Lesser General Public License version 2.1 #
-# for more details (enclosed in the file LICENSE) #
-# #
-##########################################################################
-
-ifneq ("$(FRAMAC_INTERNAL)","yes")
-FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
-else
-FRAMAC_SHARE := $(FRAMAC_ROOT_SRCDIR)/share
-endif
-
-HAS_SWIPROLOG=@HAS_SWIPROLOG@
-HAS_WP=@HAS_WP@
-
-PLUGIN_NAME = MetAcsl
-
-MetAcsl_DISTRIB_EXTERNAL:=Makefile.in configure configure.ac README.md \
- tests opam \
- $(addprefix share/, \
- model.slog run.pl setloglib.slog setlog.pl setlog_rules.pl)
-
-PLUGIN_DIR ?= .
-PLUGIN_CMO = meta_utils \
- meta_options \
- meta_bindings \
- meta_parse \
- meta_simplify \
- meta_deduce \
- meta_dispatch \
- meta_annotate \
- meta_run
-PLUGIN_TESTS_DIRS := meta
-ifneq ($(HAS_WP),no)
-PLUGIN_TESTS_DIRS += meta-wp
-ifneq ($(HAS_SWIPROLOG),no)
-PLUGIN_TESTS_DIRS += meta-deduce
-endif
-endif
-PLUGIN_DEPENDENCIES += Callgraph
-PLUGIN_REQUIRES += ocamlgraph
-PLUGIN_BFLAGS += -warn-error -20-26-27
-PLUGIN_OFLAGS += -warn-error -20-26-27
-PLUGIN_DISTRIB_EXTERNAL := $(MetAcsl_DISTRIB_EXTERNAL)
-
-include $(FRAMAC_SHARE)/Makefile.dynamic
-
-MetAcsl_DEFAULT_TESTS: $(MetAcsl_DIR)/tests/test_config
-
-ifeq ("$(FRAMAC_INTERNAL)","yes")
- WP_SHARE=-wp-share $(FRAMAC_ROOT_SRCDIR)/src/plugins/wp/share
-else
- WP_SHARE=
-endif
-
-$(MetAcsl_DIR)/tests/test_config: \
- $(MetAcsl_DIR)/tests/test_config.in $(MetAcsl_DIR)/Makefile
- $(RM) $@
- sed -e 's|@WP_SHARE@|$(WP_SHARE)|' $< > $@
- $(CHMOD_RO) $@
-
-METACSL_SHARE := $(FRAMAC_DATADIR)/meta
-
-p:
- make uninstall && make clean && make && make install
-
-install-sharedir:
- $(MKDIR) -p $(METACSL_SHARE)
-
-install:: install-sharedir
- $(PRINT_CP) $(METACSL_SHARE)
- $(CP) $(MetAcsl_DIR)/share/* $(METACSL_SHARE)
-
-ifneq ("$(FRAMAC_INTERNAL)","yes")
-
-VERSION=0.3+dev
-EXTRAVERSION?=
-OPEN_SOURCE?=yes
-
-configure: configure.ac
- autoconf -f
-
-Makefile: configure Makefile.in
- ./config.status --recheck
- ./config.status
-
-ifeq ("$(OPEN_SOURCE)","yes")
-HEADER_DIR=open-source
-else
-HEADER_DIR=close-source
-endif
-
-.PHONY: headers
-headers:
- while IFS=: read FILE LICENCE; do \
- LICENCE=$$(echo $$LICENCE | sed -e 's/^ *//'); \
- if test "$$LICENCE" != ".ignore"; then \
- headache \
- -c $(MetAcsl_DIR)/headers/header_config.txt \
- -h $(MetAcsl_DIR)/headers/$(HEADER_DIR)/$${LICENCE} \
- $${FILE}; \
- fi; \
- done \
- <headers/header_spec.txt
-
-ifeq ("$(EXTRAVERSION)","")
-FULLVERSION=$(VERSION)
-else
-FULLVERSION=$(VERSION)-$(EXTRAVERSION)
-endif
-DISTRIBDIR=frama-c-metacsl-$(FULLVERSION)
-distrib: configure
- $(RM) -r $(DISTRIBDIR)
- $(MKDIR) $(DISTRIBDIR)
- $(TAR) -cf - $(MetAcsl_SRC) $(MetAcsl_DISTRIB_EXTERNAL) | \
- tar -C $(DISTRIBDIR) -xf -
- $(RM) $(DISTRIBDIR).tar.gz
- $(TAR) czf $(DISTRIBDIR).tar.gz $(DISTRIBDIR)
-endif
diff --git a/MetAcsl.mli b/MetAcsl.ml
similarity index 98%
rename from MetAcsl.mli
rename to MetAcsl.ml
index c5a3a239c19083c69fc45fde6575c960866fdee8..cfb12a816ca1c8939fbae77eb0d6aef9f4f23b00 100644
--- a/MetAcsl.mli
+++ b/MetAcsl.ml
@@ -20,12 +20,12 @@
(* *)
(**************************************************************************)
-module Meta_utils : sig
- module StrSet : Set.S with type elt = string
-end
-
module Meta_run : sig
val translate : ?check_external:bool -> ?simpl:bool ->
?target_set:Meta_utils.StrSet.t -> ?number_assertions:bool ->
?prefix_meta:bool -> ?static_bindings:int -> unit -> Project.t
-end
+end = Meta_run
+
+module Meta_utils : sig
+ module StrSet : Set.S with type elt = string
+end = Meta_utils
diff --git a/dune b/dune
new file mode 100644
index 0000000000000000000000000000000000000000..b397dcf07b89389b3200191ad6d594f759694e7f
--- /dev/null
+++ b/dune
@@ -0,0 +1,73 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of the Frama-C's MetACSL plug-in. ;;
+;; ;;
+;; Copyright (C) 2018-2022 ;;
+;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
+;; alternatives) ;;
+;; ;;
+;; you can redistribute it and/or modify it under the terms of the GNU ;;
+;; Lesser General Public License as published by the Free Software ;;
+;; Foundation, version 2.1. ;;
+;; ;;
+;; It is distributed in the hope that it will be useful, ;;
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
+;; GNU Lesser General Public License for more details. ;;
+;; ;;
+;; See the GNU Lesser General Public License version 2.1 ;;
+;; for more details (enclosed in the file LICENSE) ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+( rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action ( progn
+ (echo "MetAcsl:" %{lib-available:frama-c-metacsl.core} "\n")
+ ;; requires Frama-C kernel
+ (echo " - Frama-C:" %{lib-available:frama-c.kernel} "\n")
+ ;; requires Wp.Ctypes
+ (echo " - CallGraph:" %{lib-available:frama-c-callgraph.core} "\n")
+ ;; optional dependencies:
+ (echo " - SWI-Prolog (tool for tests): ?\n")
+ )
+ )
+)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Build
+
+( library
+ (name MetAcsl)
+ (public_name frama-c-metacsl.core)
+ (flags -open Frama_c_kernel :standard -w -9 -warn-error -20-26-27)
+ (libraries frama-c.kernel frama-c-callgraph.core)
+)
+
+(plugin
+ (optional)
+ (name metacsl)
+ (libraries frama-c-metacsl.core)
+ (site
+ (frama-c plugins)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Install/Uninstall
+
+(install
+ (package frama-c-metacsl)
+ (section
+ (site
+ (frama-c share)))
+ (files
+ (share/model.slog as meta/model.slog)
+ (share/run.pl as meta/run.pl)
+ (share/setloglib.slog as meta/setloglib.slog)
+ (share/SETLOG_LICENSE as meta/SETLOG_LICENSE)
+ (share/setlog.pl as meta/setlog.pl)
+ (share/setlog_rules.pl as meta/setlog_rules.pl)
+ )
+)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..92cb929e47f61f5ecce80fa69ae0671ce21d6249
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,42 @@
+(lang dune 2.9)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of the Frama-C's MetACSL plug-in. ;;
+;; ;;
+;; Copyright (C) 2018-2022 ;;
+;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
+;; alternatives) ;;
+;; ;;
+;; you can redistribute it and/or modify it under the terms of the GNU ;;
+;; Lesser General Public License as published by the Free Software ;;
+;; Foundation, version 2.1. ;;
+;; ;;
+;; It is distributed in the hope that it will be useful, ;;
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
+;; GNU Lesser General Public License for more details. ;;
+;; ;;
+;; See the GNU Lesser General Public License version 2.1 ;;
+;; for more details (enclosed in the file LICENSE) ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(using dune_site 0.1)
+(generate_opam_files true)
+
+(name frama-c-metacsl)
+(maintainers "https://git.frama-c.com/pub/frama-c")
+
+(package (name frama-c-metacsl)
+ (depends
+ (ocaml (>= 4.08.1))
+ (frama-c (and (>= 24.0) (< 25.0)))
+ )
+ (depopts
+ conf-swi-prolog ; for the deduction features of MetAcsl
+ (why3 (>= 1.3.1)) ; for the validation of proofs/meta_model.why
+ )
+ ; (conflict ...)
+ (tags ("program verification" "formal specification" "C" "plugins" "ACSL"
+ "MetACSL"))
+)
diff --git a/frama-c-metacsl.opam b/frama-c-metacsl.opam
new file mode 100644
index 0000000000000000000000000000000000000000..0b424436c407887251470127dd29b6ffc5c242b2
--- /dev/null
+++ b/frama-c-metacsl.opam
@@ -0,0 +1,56 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+tags: [
+ "program verification"
+ "formal specification"
+ "C"
+ "plugins"
+ "ACSL"
+ "MetACSL"
+]
+depends: [
+ "dune" {>= "2.9"}
+ "ocaml" {>= "4.08.1"}
+ "frama-c" {>= "24.0" & < "25.0"}
+ "odoc" {with-doc}
+]
+depopts: [
+ "conf-swi-prolog"
+ "why3" {>= "1.3.1"}
+]
+build: [
+ ["dune" "subst"] {dev}
+ [
+ "dune"
+ "build"
+ "-p"
+ name
+ "-j"
+ jobs
+ "--promote-install-files=false"
+ "@install"
+ "@runtest" {with-test}
+ "@doc" {with-doc}
+ ]
+ ["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"
+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
+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.Prevosto@cea.fr"
+authors: [
+ "Virgile Robles"
+]
+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"
+
+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} ]
diff --git a/opam b/frama-c-metacsl.opam.template
similarity index 66%
rename from opam
rename to frama-c-metacsl.opam.template
index 47816db5a9491a179c4bac8022b909854356b72e..b74abebeffdf9b5c35152c2636475e751436571f 100644
--- a/opam
+++ b/frama-c-metacsl.opam.template
@@ -1,4 +1,3 @@
-opam-version: "2.0"
name: "frama-c-metacsl"
synopsis: "MetACSL plugin of Frama-C for writing pervasives properties"
version: "0.3+dev"
@@ -9,7 +8,7 @@ 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.prevosto@cea.fr"
+maintainer: "Virgile.Prevosto@cea.fr"
authors: [
"Virgile Robles"
]
@@ -17,30 +16,5 @@ 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: [
- "program verification"
- "formal specification"
- "ACSL"
- "MetACSL"
-]
-
-build: [
- ["autoconf"] {dev}
- ["./configure"]
- [make "-j%{jobs}%"]
-]
-
-install: [
- [make "install"]
-]
-
-depends: [
- "ocaml" { >= "4.08.1" }
- "frama-c" { >= "25.0" & < "26.0" }
- "why3" { >= "1.5.0" }
- "conf-autoconf" {dev}
-]
-
-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} ]
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
deleted file mode 100644
index 70d60358586f7d808f29e2d312353e1e3b1f5fb1..0000000000000000000000000000000000000000
--- a/headers/header_spec.txt
+++ /dev/null
@@ -1,32 +0,0 @@
-Makefile: .ignore
-Makefile.in: CEA_LGPL_OR_PROPRIETARY.META
-TODO.md: .ignore
-configure: .ignore
-configure.ac: CEA_LGPL_OR_PROPRIETARY.META
-MetAcsl.mli: CEA_LGPL_OR_PROPRIETARY.META
-meta_annotate.ml: CEA_LGPL_OR_PROPRIETARY.META
-meta_annotate.mli: CEA_LGPL_OR_PROPRIETARY.META
-meta_bindings.ml: CEA_LGPL_OR_PROPRIETARY.META
-meta_bindings.mli: CEA_LGPL_OR_PROPRIETARY.META
-meta_deduce.ml: CEA_LGPL_OR_PROPRIETARY.META
-meta_deduce.mli: CEA_LGPL_OR_PROPRIETARY.META
-meta_dispatch.ml: CEA_LGPL_OR_PROPRIETARY.META
-meta_dispatch.mli: CEA_LGPL_OR_PROPRIETARY.META
-meta_options.ml: CEA_LGPL_OR_PROPRIETARY.META
-meta_options.mli: CEA_LGPL_OR_PROPRIETARY.META
-meta_parse.ml: CEA_LGPL_OR_PROPRIETARY.META
-meta_parse.mli: CEA_LGPL_OR_PROPRIETARY.META
-meta_run.ml: CEA_LGPL_OR_PROPRIETARY.META
-meta_run.mli: CEA_LGPL_OR_PROPRIETARY.META
-meta_simplify.ml: CEA_LGPL_OR_PROPRIETARY.META
-meta_simplify.mli: CEA_LGPL_OR_PROPRIETARY.META
-meta_utils.ml: CEA_LGPL_OR_PROPRIETARY.META
-meta_utils.mli: CEA_LGPL_OR_PROPRIETARY.META
-README.md: .ignore
-tests: .ignore
-opam: .ignore
-share/setloglib.slog: SETLOG_LGPL
-share/setlog.pl: SETLOG_LGPL_MODIFIED
-share/setlog_rules.pl: SETLOG_LGPL
-share/run.pl: CEA_LGPL_OR_PROPRIETARY.META
-share/model.slog: CEA_LGPL_OR_PROPRIETARY.META
diff --git a/nix/ci.sh b/nix/ci.sh
new file mode 100755
index 0000000000000000000000000000000000000000..5bad402390811398889ffe9e1ee00b447fe57d75
--- /dev/null
+++ b/nix/ci.sh
@@ -0,0 +1,42 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+DEFAULT=${DEFAULT:-master}
+NIX_TARGET="meta"
+# <plugin> /nix /ci.sh
+PLUGIN_DIR="$(dirname "$(dirname "$(readlink -f "$0")")")"
+
+CURRENT_BRANCH="${CI_MERGE_REQUEST_SOURCE_BRANCH_NAME:-}"
+: "${CURRENT_BRANCH:="${CI_COMMIT_REF_NAME:-}"}"
+: "${CURRENT_BRANCH:="$(git branch --show-current)"}"
+
+# prints
+# - "$CURRENT_BRANCH" if it is a branch name in remote $1,
+# - else "$DEFAULT" if it is set and $DEFAULT is a branch name in remote $1,
+# - else master
+get_matching_branch () {
+ if git ls-remote --quiet --exit-code "$1" "$CURRENT_BRANCH" >/dev/null 2>/dev/null;
+ then echo "$CURRENT_BRANCH"
+ elif git ls-remote --quiet --exit-code "$1" "$DEFAULT" >/dev/null 2>/dev/null;
+ then echo "$DEFAULT"
+ else echo master
+ fi
+}
+
+TMP_DIR="$(mktemp -d)"
+
+cleanup () {
+ rm -rf $TMP_DIR
+}
+
+trap cleanup EXIT
+
+mkdir -p $TMP_DIR/frama-ci
+frama_ci_repo="$(readlink -f $TMP_DIR/frama-ci)"
+frama_ci_url="git@git.frama-c.com:frama-c/Frama-CI.git"
+frama_ci_branch="$(get_matching_branch "$frama_ci_url")"
+echo "using branch $frama_ci_branch of Frama-CI repo at $frama_ci_repo"
+git clone --depth=1 --branch="$frama_ci_branch" "$frama_ci_url" "$frama_ci_repo"
+
+source $frama_ci_repo/common-plugin-ci.sh
diff --git a/nix/default.nix b/nix/default.nix
deleted file mode 100644
index da1dfba417f576361afddbdd8965fee352a23bc4..0000000000000000000000000000000000000000
--- a/nix/default.nix
+++ /dev/null
@@ -1,18 +0,0 @@
-# paramaterised derivation with dependencies injected (callPackage style)
-{ pkgs, stdenv, opam2nix,
- src ? ../.,
- ocaml ? "ocamlPackages_latest.ocaml",
- plugins ? { },
- plugin_extend ? self: super: { }
-}:
-
-plugins.helpers.simple_plugin
- { inherit pkgs stdenv src opam2nix ocaml plugins plugin_extend;
- name = "meta";
- deps = [ pkgs.swiProlog ];
- preFramaCTests = ''
- echo CONFIGURING Why3 for Frama_Clang.
- export HOME=$(mktemp -d)
- why3 config detect
- '';
- }
diff --git a/nix/frama-ci.nix b/nix/frama-ci.nix
deleted file mode 100644
index eccc033949bb7b58902bedfcbf60a6d6555b59eb..0000000000000000000000000000000000000000
--- a/nix/frama-ci.nix
+++ /dev/null
@@ -1,16 +0,0 @@
-#To copy in other repository
-{ password}:
-
-let
- src = builtins.fetchGit {
- "url" = "https://bobot:${password}@git.frama-c.com/frama-c/Frama-CI.git";
- "name" = "Frama-CI";
- "rev" = "ceea8c97fc127db159bfd92919eae404e2e67f18";
- "ref" = "master";
- };
- pkgs = import "${src}/pkgs.nix" {};
- in
- {
- src = src;
- compiled = pkgs.callPackage "${src}/compile.nix" { inherit pkgs; };
- }
diff --git a/nix/frama-ci.sh b/nix/frama-ci.sh
deleted file mode 100755
index b4deee0abc1543e01c82d3c6c92d9b0045b26d77..0000000000000000000000000000000000000000
--- a/nix/frama-ci.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/sh -eu
-
-DIR=$(dirname $0)
-
-export FRAMA_CI_NIX=$DIR/frama-ci.nix
-export FRAMA_CI=$(nix-instantiate --eval -E "((import <nixos-20.03> {}).callPackage $FRAMA_CI_NIX { password = \"$TOKEN_FOR_API\";}).src.outPath")
-
-FRAMA_CI=${FRAMA_CI#\"}
-FRAMA_CI=${FRAMA_CI%\"}
-
-export NIX_PATH="nixpkgs=$(eval echo $(nix-instantiate --eval -E "with import $FRAMA_CI/pkgs-ref.nix; url"))"
-$FRAMA_CI/compile.sh $@
diff --git a/nix/meta.nix b/nix/meta.nix
new file mode 100644
index 0000000000000000000000000000000000000000..e8e6641083da72eef6d01c2f67478a9d23548ee5
--- /dev/null
+++ b/nix/meta.nix
@@ -0,0 +1,11 @@
+{ mk_plugin
+, gitignoreSource
+, swiProlog
+}:
+
+mk_plugin {
+ plugin-name = "metacsl" ;
+ plugin-src = gitignoreSource ./.. ;
+ additional-check-inputs = [ swiProlog ] ;
+ has-wp-proofs = true ;
+}
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
new file mode 100644
index 0000000000000000000000000000000000000000..b1f822442c8aa0715d8d923465d403277f6ef4b4
--- /dev/null
+++ b/nix/pkgs.nix
@@ -0,0 +1,16 @@
+{ frama-c-repo ? builtins.trace "meta: defaulting frama-c-repo to ${toString ../../frama-c}" ../../frama-c }:
+let
+ ocamlOverlay = oself: osuper: {
+ meta = oself.callPackage ./meta.nix {};
+ };
+ overlay = self: super: {
+ ocaml-ng = super.lib.mapAttrs (
+ name: value:
+ if builtins.hasAttr "overrideScope'" value
+ then value.overrideScope' ocamlOverlay
+ else value
+ ) super.ocaml-ng;
+ };
+ pkgs = (import (frama-c-repo + "/nix/pkgs.nix")).appendOverlays [ overlay ];
+in
+pkgs
diff --git a/tests/ptests_config b/tests/ptests_config
new file mode 100644
index 0000000000000000000000000000000000000000..678b7448bff05abcb33bec77dab78e7807bb77c5
--- /dev/null
+++ b/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES = meta meta-deduce meta-wp
diff --git a/tests/test_config b/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..213b04dd4df3abcec23faa64891f2a7406ad1e0f
--- /dev/null
+++ b/tests/test_config
@@ -0,0 +1,7 @@
+MACRO: META -meta
+MACRO: WP -then-last -wp -wp-timeout 1 -wp-par 1 -wp-msg-key shell -wp-cache update -wp-session @PTEST_SUITE_DIR@/../wp-cache
+MACRO: PRINT -then-last -print
+
+MACRO: EVA_PLUGINS eva,scope,inout variadic
+MACRO: WP_PLUGINS wp,rtegen
+PLUGIN: metacsl @WP_PLUGINS@ @EVA_PLUGINS@
diff --git a/tests/test_config.in b/tests/test_config.in
deleted file mode 100644
index 45ffa54deec4b146c5a86e5cd6487912b2ee3a4a..0000000000000000000000000000000000000000
--- a/tests/test_config.in
+++ /dev/null
@@ -1,9 +0,0 @@
-COMMENT: Generated file. Edit test_config.in
-
-MACRO: META -meta -meta-share @PTEST_SHARE_DIR@
-MACRO: WP -then-last -wp -wp-timeout 1 -wp-par 1 -wp-msg-key shell -wp-cache update -wp-session @PTEST_SUITE_DIR@/../wp-cache @WP_SHARE@
-MACRO: PRINT -then-last -print
-
-MACRO: EVA_PLUGINS eva,scope variadic
-MACRO: WP_PLUGINS wp,rtegen
-PLUGIN: metacsl @WP_PLUGINS@ @EVA_PLUGINS@