Skip to content
Snippets Groups Projects
Commit 8b823cc0 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'feature/bobot/jbuilder' into 'master' 

Use Dune for building MetAcsl

See merge request frama-c/meta!59
parents 41189bee 608159a3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 441 additions and 279 deletions
.gitattributes 0 → 100644
+ 111
− 0
View file @ 8b823cc0
################
# 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
.gitignore
+ 5
− 8
View file @ 8b823cc0
......@@ -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/
.gitlab-ci.yml
+ 38
− 8
View file @ 8b823cc0
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
configure.ac → Makefile
+ 33
− 18
View file @ 8b823cc0
......@@ -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
Makefile.in deleted 100644 → 0
+ 0
− 135
View file @ 41189bee
##########################################################################
# #
# 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
MetAcsl.mli → MetAcsl.ml
+ 5
− 5
View file @ 8b823cc0
......@@ -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
dune 0 → 100644
+ 73
− 0
View file @ 8b823cc0
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 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)
)
)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
dune-project 0 → 100644
+ 42
− 0
View file @ 8b823cc0
(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"))
)
frama-c-metacsl.opam 0 → 100644
+ 56
− 0
View file @ 8b823cc0
# 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} ]
opam → frama-c-metacsl.opam.template
+ 1
− 27
View file @ 8b823cc0
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} ]
headers/header_spec.txt deleted 100644 → 0
+ 0
− 32
View file @ 41189bee
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
nix/ci.sh 0 → 100755
+ 42
− 0
View file @ 8b823cc0
#!/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
nix/default.nix deleted 100644 → 0
+ 0
− 18
View file @ 41189bee
# 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
'';
}
nix/frama-ci.nix deleted 100644 → 0
+ 0
− 16
View file @ 41189bee
#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; };
}
nix/frama-ci.sh deleted 100755 → 0
+ 0
− 12
View file @ 41189bee
#!/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 $@
nix/meta.nix 0 → 100644
+ 11
− 0
View file @ 8b823cc0
{ mk_plugin
, gitignoreSource
, swiProlog
}:
mk_plugin {
plugin-name = "metacsl" ;
plugin-src = gitignoreSource ./.. ;
additional-check-inputs = [ swiProlog ] ;
has-wp-proofs = true ;
}
nix/pkgs.nix 0 → 100644
+ 16
− 0
View file @ 8b823cc0
{ 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
tests/ptests_config 0 → 100644
+ 1
− 0
View file @ 8b823cc0
DEFAULT_SUITES = meta meta-deduce meta-wp
tests/test_config.in → tests/test_config
+ 7
− 0
View file @ 8b823cc0
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: 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 variadic
MACRO: EVA_PLUGINS eva,scope,inout variadic
MACRO: WP_PLUGINS wp,rtegen
PLUGIN: metacsl @WP_PLUGINS@ @EVA_PLUGINS@
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment