diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 96c52af374c82f1c0bc8524cda90c91437398ab7..0f54bad033530b3a48bbc86e9e541750c5ac9676 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,225 +1,248 @@
stages:
- - update_docker
- - lint
- - frama_c_and_plugins
+ - git-update
+ - build
+ - tests
- distrib_and_compatibility
-variables:
- OPAM_PACKAGES: ocamlfind zarith ocamlgraph ocp-indent
-
-# update the cache
-update_docker:
- stage: update_docker
- image: ocaml/opam:debian
- variables:
- GIT_STRATEGY: none
- before_script:
- - sudo apt-get install -y -qq rsync
- - mkdir -p .gitlab_oci_cache/.opam/
- - rsync -a .gitlab_oci_cache/.opam/ /home/opam/.opam/
- - opam list
- - opam depext -i $OPAM_PACKAGES
- after_script:
- - rsync -a --delete /home/opam/.opam/ .gitlab_oci_cache/.opam/
- cache:
- key: "frama-c"
- paths:
- - .gitlab_oci_cache/
- script:
- - exit 0
- tags:
- - docker
-
-#lint uses the cache but doesn't modify it
-lint:
- stage: lint
- image: ocaml/opam:debian
- before_script:
- - sudo apt-get install -y -qq rsync autoconf build-essential bc
- - mkdir -p .gitlab_oci_cache/.opam/
- - rsync -a .gitlab_oci_cache/.opam/ /home/opam/.opam/
- - opam list
- - opam depext -i $OPAM_PACKAGES
- cache:
- key: "frama-c"
- paths:
- - .gitlab_oci_cache/
- script:
- - autoconf
- - ./configure
- - make lint
- - make stats-lint
-# - make check-headers OPEN_SOURCE=yes STRICT_HEADERS=yes
- coverage: '/lint coverage: \d+\.\d+/'
- tags:
- - docker
-
-
-frama-c-external:
- stage: frama_c_and_plugins
+#avoid a nix error https://github.com/NixOS/nix/issues/2087
+git-update:
+ stage: git-update
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c-external --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh instantiate --eval -A frama-c.src.outPath
tags:
- except:
- - tags
- retry: 2
+ - nix
frama-c:
- stage: frama_c_and_plugins
+ stage: build
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A frama-c.installed
tags:
- except:
- - tags
- retry: 2
+ - nix
-frama-c-ocaml-4.03:
- stage: distrib_and_compatibility
+lint:
+ stage: build
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --ocaml 4.03 --camlp4 4.03 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A frama-c.lint
+ coverage: '/lint coverage: \d+\.\d+/'
tags:
- except:
- - tags
- retry: 2
+ - nix
-frama-c-ocaml-4.04:
- stage: distrib_and_compatibility
+tests:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --ocaml 4.04 --camlp4 4.04 --lablgtk 4bbd5cf1990aa8b775cf247fbfe5be321e13cc61 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A frama-c.tests
tags:
- except:
- - tags
- retry: 2
+ - nix
-frama-c-ocaml-4.05:
- stage: distrib_and_compatibility
+wp-qualif:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --ocaml 4.05 --camlp4 4.05 --lablgtk 4bbd5cf1990aa8b775cf247fbfe5be321e13cc61 --camomile 3f4d657d50c17213f3338ca75efb30d728704df3 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A frama-c.wp-qualif
tags:
- except:
- - tags
- retry: 2
+ - nix
allow_failure: true
-frama-c-internal:
- stage: distrib_and_compatibility
- script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c-internal --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
- tags:
- only:
- - master
- - stable/silicium
- except:
- - tags
- retry: 2
-
-frama-c-distrib:
- stage: distrib_and_compatibility
+genassigns:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c-distrib --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A genassigns.tests
tags:
- except:
- - tags
- retry: 2
+ - nix
-
-Genassigns:
- stage: frama_c_and_plugins
+counter-examples:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Genassigns --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A counter-examples.tests
tags:
- except:
- - tags
- retry: 2
+ - nix
-Mthread:
- stage: frama_c_and_plugins
+acsl-importer:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Mthread --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A acsl-importer.tests
tags:
- except:
- - tags
- retry: 2
+ - nix
-a3export:
- stage: frama_c_and_plugins
+volatile:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME a3export --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A volatile.tests
tags:
- except:
- - tags
- retry: 2
+ - nix
-PathCrawler:
- stage: frama_c_and_plugins
+E-ACSL:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME PathCrawler --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A e-acsl.tests
tags:
- except:
- - tags
- retry: 2
+ - nix
Security:
- stage: frama_c_and_plugins
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Security --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A security.tests
tags:
- except:
- - tags
- retry: 2
+ - nix
-E-ACSL:
- stage: frama_c_and_plugins
+CFP:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME E-ACSL --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A context-from-precondition.tests
tags:
- except:
- - tags
- allow_failure: true
- retry: 2
+ - nix
-context-from-precondition:
- stage: frama_c_and_plugins
+internal:
+ stage: distrib_and_compatibility
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME context-from-precondition --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A frama-c.internal
tags:
- except:
- - tags
- retry: 2
+ - nix
-open-source-case-studies:
- stage: frama_c_and_plugins
+.build_template: &frama-c-ocaml
+ stage: distrib_and_compatibility
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --url open-source-case-studies,git@git.frama-c.com:frama-c/open-source-case-studies.git --commit open-source-case-studies,master open-source-case-studies --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A frama-c.installed
tags:
- except:
- - tags
- when: manual
- retry: 2
+ - nix
+
+
+frama-c-ocaml-4.02:
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_02"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
+ <<: *frama-c-ocaml
-ACSL-importer:
- stage: frama_c_and_plugins
+frama-c-ocaml-4.03:
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_03"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
+ <<: *frama-c-ocaml
+
+frama-c-ocaml-4.04:
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_04"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
+ <<: *frama-c-ocaml
+
+frama-c-ocaml-4.06:
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_06"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
+ <<: *frama-c-ocaml
+
+frama-c-ocaml-4.07:
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_07"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
+ <<: *frama-c-ocaml
+
+caveat-importer:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME ACSL-importer --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A caveat-importer.tests
tags:
- except:
- - tags
- retry: 2
+ - nix
-Caveat-importer:
- stage: frama_c_and_plugins
+mthread:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Caveat-importer --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A mthread.tests
tags:
- except:
- - tags
- retry: 2
+ - nix
-Volatile:
- stage: frama_c_and_plugins
+pathcrawler:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "master"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Volatile --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A pathcrawler.tests
tags:
- except:
- - tags
- retry: 2
+ - nix
diff --git a/Makefile b/Makefile
index a578a6b1d9d259fd8c5a19ba1eb0df1b22f4d129..66c0425e779534241c469e900cd1b08a8a968e08 100644
--- a/Makefile
+++ b/Makefile
@@ -374,7 +374,7 @@ ifeq ("$(DEVELOPMENT)","yes")
all:: share/.gitignore
endif
-clean::
+clean_share_link:
if test -f share/.gitignore; then \
for link in $$(cat share/.gitignore); do \
if test -L share$$link; then \
@@ -386,6 +386,8 @@ clean::
rm share/.gitignore; \
fi
+clean:: clean_share_link
+
##############
# Ocamlgraph #
##############
@@ -1221,6 +1223,16 @@ bin/toplevel.opt$(EXE): $(ALL_BATCH_CMX) $(GEN_OPT_LIBS) \
$(PRINT_LINKING) $@
$(OCAMLOPT) $(OLINKFLAGS) -o $@ $(OPT_LIBS) $(ALL_BATCH_CMX)
+LIB_KERNEL_CMO= $(filter-out src/kernel_internals/runtime/gui_init.cmo, $(CMO))
+LIB_KERNEL_CMX= $(filter-out src/kernel_internals/runtime/gui_init.cmx, $(CMX))
+
+lib/fc/frama-c.cma: $(LIB_KERNEL_CMO) $(GEN_OPT_LIBS) $(LIB_KERNEL_CMX) lib/fc/META.frama-c
+ $(PRINT_LINKING) $@ and lib/fc/frama-c.cmxa
+ $(MKDIR) $(FRAMAC_LIB)
+ $(OCAMLMKLIB) -o lib/fc/frama-c $(OPT_LIBS) $(LIB_KERNEL_CMO) $(LIB_KERNEL_CMX)
+
+lib/fc/frama-c.cmxa: lib/fc/frama-c.cma
+
####################
# (Ocaml) Toplevel #
####################
@@ -1826,6 +1838,7 @@ install-lib: clean-install
$(PRINT_INSTALL) kernel API
$(MKDIR) $(FRAMAC_LIBDIR)
$(CP) $(LIB_BYTE_TO_INSTALL) $(LIB_OPT_TO_INSTALL) $(FRAMAC_LIBDIR)
+ $(CP) $(addprefix lib/fc/,dllframa-c.so libframa-c.a frama-c.cma frama-c.a frama-c.cmxa META.frama-c) $(FRAMAC_LIBDIR)
install-doc-code:
$(PRINT_INSTALL) API documentation
@@ -2398,15 +2411,15 @@ clean-distrib: dist-clean
create_lib_to_install_list = $(addprefix $(FRAMAC_LIB)/,$(call map,notdir,$(1)))
-byte:: bin/toplevel.byte$(EXE) share/Makefile.dynamic_config \
+byte:: bin/toplevel.byte$(EXE) lib/fc/frama-c.cma share/Makefile.dynamic_config \
$(call create_lib_to_install_list,$(LIB_BYTE_TO_INSTALL)) \
- $(PLUGIN_META_LIST)
+ $(PLUGIN_META_LIST) lib/fc/META.frama-c
-opt:: bin/toplevel.opt$(EXE) share/Makefile.dynamic_config \
+opt:: bin/toplevel.opt$(EXE) lib/fc/frama-c.cmxa share/Makefile.dynamic_config \
$(call create_lib_to_install_list,$(LIB_OPT_TO_INSTALL)) \
$(filter %.o %.cmi,\
$(call create_lib_to_install_list,$(LIB_BYTE_TO_INSTALL))) \
- $(PLUGIN_META_LIST)
+ $(PLUGIN_META_LIST) lib/fc/META.frama-c
top: bin/toplevel.top$(EXE) \
$(call create_lib_to_install_list,$(LIB_BYTE_TO_INSTALL)) \
diff --git a/Makefile.generating b/Makefile.generating
index f6fc54a95d179d6920d44dd3a9f75cd6bf3ab557..174a2b7bd4944525c884101148b7d1bf947bdb41 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -209,6 +209,12 @@ ifeq ("$(DEVELOPMENT)","yes")
all:: .merlin
endif
+lib/fc/META.frama-c: share/META.frama-c share/Makefile.config Makefile.generating
+ $(MKDIR) lib/fc/
+ $(SED) $< -e "s/@REQUIRES/$(LIBRARY_NAMES)/" > $@
+
+GENERATED += lib/fc/META.frama-c
+
# Local Variables:
# mode: makefile
diff --git a/default.nix b/default.nix
new file mode 100644
index 0000000000000000000000000000000000000000..e64150378a86d1a128776f31ba1f5912ea77af15
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,15 @@
+# standalone derivation, for nix-build, nix-shell, etc
+{ pkgs ? import <nixpkgs> {} }:
+let
+ src = builtins.fetchGit {
+ "url" = ./.git;
+ "name" = "frama-c";
+ "rev" = "ffa925f404779a3a0c4aacff5bd78b1c502def11";
+ "ref" = "test-nix-fetchGit";
+ };
+ in
+
+pkgs.callPackage ./nix/default.nix {
+ opam2nix = pkgs.callPackage ../Frama-CI/opam2nix-packages.nix {};
+ src = src;
+}
diff --git a/nix/default.nix b/nix/default.nix
new file mode 100644
index 0000000000000000000000000000000000000000..3bc25269109649cda4fcd4975e348e46a170e8e7
--- /dev/null
+++ b/nix/default.nix
@@ -0,0 +1,238 @@
+# paramaterised derivation with dependencies injected (callPackage style)
+{ pkgs, stdenv, src ? ../., opam2nix, ocaml_version ? "ocaml-ng.ocamlPackages_4_05.ocaml", plugins ? { } }:
+
+let mk_buildInputs = { opamPackages ? [] } :
+ [ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl] ++ opam2nix.build {
+ specs = opam2nix.toSpecs ([ "ocamlfind" "zarith" "ocamlgraph"
+ { name = "coq"; constraint = "=8.7.2"; }
+ ] ++ opamPackages ++
+ (if ocaml_version == "pkgs.ocaml-ng.ocamlPackages_4_02.ocaml"
+ then [ { name = "ocamlbuild" ; constraint = "=0"; } ] else [])
+ );
+ ocamlAttr = ocaml_version;
+ };
+
+in
+
+rec {
+ inherit src;
+ buildInputs = mk_buildInputs {};
+ installed = main.out;
+ main = stdenv.mkDerivation {
+ name = "frama-c";
+ inherit src buildInputs;
+ outputs = [ "out" "build_dir" ];
+ postPatch = ''
+ patchShebangs .
+ '';
+ configurePhase = ''
+ unset CC
+ autoconf
+ ./configure --prefix=$out
+ '';
+ buildPhase = ''
+ make -j 4
+ '';
+ installPhase = ''
+ make install
+ mkdir -p $build_dir
+ tar -cf $build_dir/dir.tar .
+ pwd > $build_dir/old_pwd
+ '';
+ setupHook = pkgs.writeText "setupHook.sh" ''
+ addFramaCPath () {
+ if test -d "''$1/lib/frama-c/plugins"; then
+ export FRAMAC_PLUGIN="''${FRAMAC_PLUGIN}''${FRAMAC_PLUGIN:+:}''$1/lib/frama-c/plugins"
+ export OCAMLPATH="''${OCAMLPATH}''${OCAMLPATH:+:}''$1/lib/frama-c/plugins"
+ fi
+
+ if test -d "''$1/lib/frama-c"; then
+ export OCAMLPATH="''${OCAMLPATH}''${OCAMLPATH:+:}''$1/lib/frama-c"
+ fi
+
+ if test -d "''$1/share/frama-c/"; then
+ export FRAMAC_EXTRA_SHARE="''${FRAMAC_EXTRA_SHARE}''${FRAMAC_EXTRA_SHARE:+:}''$1/share/frama-c"
+ fi
+
+ }
+
+ addEnvHooks "$targetOffset" addFramaCPath
+ '';
+ };
+
+ lint = stdenv.mkDerivation {
+ name = "frama-c-lint";
+ inherit src;
+ buildInputs = (mk_buildInputs {opamPackages = [ "ocp-indent" ];} ) ++ [ pkgs.bc plugins.headache.installed pkgs.file ];
+ outputs = [ "out" ];
+ postPatch = ''
+ patchShebangs .
+ '';
+ configurePhase = ''
+ unset CC
+ autoconf
+ ./configure --prefix=$out
+ '';
+ buildPhase = ''
+ make lint
+ make stats-lint
+ make check-headers
+ '';
+ installPhase = ''
+ true
+ '';
+ };
+
+ tests = stdenv.mkDerivation {
+ name = "frama-c-test";
+ inherit buildInputs;
+ build_dir = main.build_dir;
+ src = main.build_dir + "/dir.tar";
+ sourceRoot = ".";
+ postUnpack = ''
+ find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
+ '';
+ configurePhase = ''
+ true
+ '';
+ buildPhase = ''
+ make clean_share_link
+ make create_share_link
+ make tests -j4 PTESTS_OPTS="-error-code -j 4"
+ '';
+ installPhase = ''
+ true
+ '';
+ };
+
+ distrib = stdenv.mkDerivation {
+ name = "frama-c-distrib";
+ inherit src;
+ buildInputs = buildInputs ++ [ plugins.headache.installed ];
+ postPatch = ''
+ patchShebangs .
+ '';
+ configurePhase = ''
+ unset CC
+ autoconf
+ ./configure --prefix=$out
+ '';
+ buildPhase = ''
+ make DISTRIB="frama-c-archive" src-distrib
+ '';
+ installPhase = ''
+ tar -C $out --strip-components=1 -xf frama-c-archive.tar.gz
+ '';
+ };
+
+ tests-distrib = stdenv.mkDerivation {
+ name = "frama-c-tests-distrib";
+ inherit distrib buildInputs;
+ outputs = [ "out" "build_dir" ];
+ configurePhase = ''
+ unset CC
+ autoconf
+ ./configure --prefix=$out
+ '';
+ buildPhase = ''
+ make -j 4
+ make tests -j4 PTESTS_OPTS="-error-code -j 4"
+ '';
+ installPhase = ''
+ make install
+ '';
+ };
+
+ wp-qualif = stdenv.mkDerivation {
+ name = "frama-c-wp-qualif";
+ buildInputs = mk_buildInputs { opamPackages = [
+ { name = "alt-ergo"; constraint = "=2.0.0"; }
+ { name = "why3" ; constraint = "=0.88.3"; }
+ ]; };
+ build_dir = main.build_dir;
+ src = main.build_dir + "/dir.tar";
+ sourceRoot = ".";
+ postUnpack = ''
+ find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
+ '';
+ configurePhase = ''
+ true
+ '';
+ buildPhase = ''
+ make clean_share_link
+ make create_share_link
+ mkdir home
+ HOME=$(pwd)/home
+ why3 config
+ bin/ptests.opt -error-code -config qualif src/plugins/wp/tests
+ '';
+ installPhase = ''
+ true
+ '';
+ };
+
+ internal = stdenv.mkDerivation {
+ name = "frama-c-internal";
+ inherit src;
+ buildInputs = (mk_buildInputs { opamPackages = [ "xml-light" ];} ) ++
+ [ pkgs.getopt pkgs.which
+ pkgs.libxslt pkgs.libxml2 pkgs.file pkgs.autoPatchelfHook stdenv.cc.cc.lib
+ ];
+ counter_examples_src = plugins.counter-examples.src;
+ genassigns_src = plugins.genassigns.src;
+ pathcrawler_src = plugins.pathcrawler.src;
+ mthread_src = plugins.mthread.src;
+ caveat_importer_src = plugins.caveat-importer.src;
+ acsl_importer_src = plugins.acsl-importer.src;
+ volatile_src = plugins.volatile.src;
+ e_acsl_src = plugins.e-acsl.src;
+ security_src = plugins.security.src;
+ context_from_precondition_src = plugins.context-from-precondition.src;
+ postPatch = ''
+ patchShebangs .
+ '';
+ postUnpack = ''
+ cp -r --preserve=mode "$counter_examples_src" "$sourceRoot/src/plugins/counter-examples"
+ chmod -R u+w -- "$sourceRoot/src/plugins/counter-examples"
+ cp -r --preserve=mode "$genassigns_src" "$sourceRoot/src/plugins/genassigns"
+ chmod -R u+w -- "$sourceRoot/src/plugins/genassigns"
+ cp -r --preserve=mode "$pathcrawler_src" "$sourceRoot/src/plugins/pathcrawler"
+ chmod -R u+w -- "$sourceRoot/src/plugins/pathcrawler"
+ cp -r --preserve=mode "$mthread_src" "$sourceRoot/src/plugins/mthread"
+ chmod -R u+w -- "$sourceRoot/src/plugins/mthread"
+ cp -r --preserve=mode "$caveat_importer_src" "$sourceRoot/src/plugins/caveat-importer"
+ chmod -R u+w -- "$sourceRoot/src/plugins/caveat-importer"
+ cp -r --preserve=mode "$volatile_src" "$sourceRoot/src/plugins/volatile"
+ chmod -R u+w -- "$sourceRoot/src/plugins/volatile"
+ cp -r --preserve=mode "$acsl_importer_src" "$sourceRoot/src/plugins/acsl-importer"
+ chmod -R u+w -- "$sourceRoot/src/plugins/acsl-importer"
+ cp -r --preserve=mode "$e_acsl_src" "$sourceRoot/src/plugins/e-acsl"
+ chmod -R u+w -- "$sourceRoot/src/plugins/e-acsl"
+ echo IN_FRAMA_CI=yes > "$sourceRoot/in_frama_ci"
+ cp -r --preserve=mode "$context_from_precondition_src" "$sourceRoot/src/plugins/context-from-precondition"
+ chmod -R u+w -- "$sourceRoot/src/plugins/context-from-precondition"
+ cp -r --preserve=mode "$security_src" "$sourceRoot/src/plugins/security"
+ chmod -R u+w -- "$sourceRoot/src/plugins/security"
+ '';
+
+ configurePhase = ''
+ unset CC
+ autoconf
+ ./configure --prefix=$out
+ '';
+ buildPhase = ''
+ make unpack-eclipse
+ sed -i src/plugins/pathcrawler/extern/eclipseCLP/RUNME -e "s/chmod 2755/chmod 755/g"
+ rm src/plugins/pathcrawler/extern/eclipseCLP/lib/x86_64_linux/dbi_mysql.so
+ rm src/plugins/pathcrawler/extern/eclipseCLP/lib/x86_64_linux/ic.so
+ prefix="src/plugins/pathcrawler" autoPatchelf
+ make -j 4
+ ln -sr src/plugins/pathcrawler/share share/pc
+ make tests -j4 PTESTS_OPTS="-error-code -j 4"
+ '';
+ installPhase = ''
+ make install
+ '';
+ };
+
+}
diff --git a/nix/empty b/nix/empty
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/nix/frama-ci.nix b/nix/frama-ci.nix
new file mode 100644
index 0000000000000000000000000000000000000000..e26a55d0f058b25b43d59ddd40a3656c951ef440
--- /dev/null
+++ b/nix/frama-ci.nix
@@ -0,0 +1,15 @@
+#To copy in other repository
+{ pkgs ? import <nixpkgs> {}, password}:
+
+let
+ src = builtins.fetchGit {
+ "url" = "https://bobot:${password}@git.frama-c.com/frama-c/Frama-CI.git";
+ "name" = "Frama-CI";
+ "rev" = "70045f4252e668e0facad12d7db2c6ab83fc813b";
+ "ref" = "master";
+ };
+ in
+ {
+ src = src;
+ compiled = pkgs.callPackage "${src}/compile.nix" { inherit pkgs; };
+ }
diff --git a/nix/frama-ci.sh b/nix/frama-ci.sh
new file mode 100755
index 0000000000000000000000000000000000000000..b4a69f90154968218273a70d50be6173a2909841
--- /dev/null
+++ b/nix/frama-ci.sh
@@ -0,0 +1,12 @@
+#!/bin/sh -eu
+
+DIR=$(dirname $0)
+
+export FRAMA_CI_NIX=$DIR/frama-ci.nix
+
+export FRAMA_CI=$(nix-instantiate --eval -E "((import <nixpkgs> {}).callPackage $FRAMA_CI_NIX { password = \"$TOKEN_FOR_API\";}).src.outPath")
+
+FRAMA_CI=${FRAMA_CI#\"}
+FRAMA_CI=${FRAMA_CI%\"}
+
+$FRAMA_CI/compile.sh $@
diff --git a/share/META.frama-c b/share/META.frama-c
new file mode 100644
index 0000000000000000000000000000000000000000..be05739fdfee70b426d186932e71a06352db62e4
--- /dev/null
+++ b/share/META.frama-c
@@ -0,0 +1,16 @@
+description="frama-c"
+version=""
+requires=""
+
+package "kernel" (
+ description="The kernel library of frama-c"
+ version=""
+ requires="@REQUIRES"
+ archive(byte) = "frama-c.cma"
+ plugin(byte) = "frama-c.cma"
+ archive(native) = "frama-c.cmxa"
+ plugin(native) = "frama-c.cmxs"
+ directory=""
+)
+
+directory=""
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index 13eda479d2ab98e0c3fcbd8be80b5646da605d1e..9d321679ed94e0bd3c09e788c50172408cd44421 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -38,10 +38,10 @@ prefix ?=@prefix@
exec_prefix ?=@exec_prefix@
datarootdir ?=@datarootdir@
datadir ?=@datadir@
-BINDIR ?="$(DESTDIR)@bindir@"
-LIBDIR ?="$(DESTDIR)@libdir@"
-DATADIR ?="$(DESTDIR)@datarootdir@"
-MANDIR ?="$(DESTDIR)@mandir@"
+BINDIR ?=$(DESTDIR)@bindir@
+LIBDIR ?=$(DESTDIR)@libdir@
+DATADIR ?=$(DESTDIR)@datarootdir@
+MANDIR ?=$(DESTDIR)@mandir@
FRAMAC_LIBDIR ?=$(LIBDIR)/frama-c
FRAMAC_PLUGINDIR ?=$(FRAMAC_LIBDIR)/plugins
@@ -65,6 +65,8 @@ OCAMLDEP ?=@OCAMLDEP@ -slash
OCAMLLEX ?=@OCAMLLEX@
OCAMLYACC ?=@OCAMLYACC@
OCAMLMKTOP ?=@OCAMLMKTOP@
+OCAMLMKLIB ?=@OCAMLFIND@ ocamlmklib
+OCAMLFIND ?=@OCAMLFIND@
OCAMLDOC ?=@OCAMLDOC@
OCAMLCP ?=@OCAMLCP@
diff --git a/share/Makefile.dynamic b/share/Makefile.dynamic
index d67115ac9a983e357817f5254917ebb55a28acb3..4ebe6147bc6d2b7b10b77c5c0c9e035d93765a01 100644
--- a/share/Makefile.dynamic
+++ b/share/Makefile.dynamic
@@ -46,6 +46,7 @@ ifeq ($(FRAMAC_INTERNAL),yes)
PLUGIN_RESET :=yes
else
+
# The plugin is compiled from an installed frama-c
PLUGIN_RESET :=no
include $(MAKECONFIG_DIR)/Makefile.common
@@ -186,11 +187,11 @@ $(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
TARGETS := $(TARGET_META) $(TARGET_CMI)
TARGETS_TOP := $(TARGET_TOP_CMO) $(TARGET_TOP_CMX) \
- $(TARGET_TOP_CMA) $(TARGET_TOP_CMXS)
+ $(TARGET_TOP_CMA) $(TARGET_TOP_CMXS) $(TARGET_TOP_O)
TARGETS_GUI_BYTE := $(TARGET_GUI_CMI) $(TARGET_GUI_CMO)
-TARGETS_GUI := $(TARGETS_GUI_BYTE) $(TARGET_GUI_CMX) $(TARGET_GUI_CMXS)
+TARGETS_GUI := $(TARGETS_GUI_BYTE) $(TARGET_GUI_CMX) $(TARGET_GUI_CMXS) $(TARGET_GUI_O)
TARGETS_BYTE:= $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMO) $(TARGET_TOP_CMA)
-TARGETS_OPT:= $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMX) $(TARGET_TOP_CMXS)
+TARGETS_OPT:= $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMX) $(TARGET_TOP_CMXS) $(TARGET_TOP_O)
byte:: $(TARGETS_BYTE)
opt:: $(TARGETS_OPT)
diff --git a/share/Makefile.dynamic_config.external b/share/Makefile.dynamic_config.external
index 5cb3d96418aa16cf410ee7a9b372fe8e2ea8797e..e76a1aa89899864ff5f1c29830e04a997b0f855c 100644
--- a/share/Makefile.dynamic_config.external
+++ b/share/Makefile.dynamic_config.external
@@ -29,13 +29,16 @@ export FRAMAC_INCLUDES=-I "$(FRAMAC_LIBDIR)"
export PTESTS=$(BINDIR)/ptests.$(PTESTSBEST)$(EXE)
-export FRAMAC_LIB="$(FRAMAC_LIBDIR)"
+export FRAMAC_LIB=$(FRAMAC_LIBDIR)
export DOC_DIR=$(FRAMAC_SHARE)/doc/code
export PLUGIN_LIB_DIR=$(PLUGIN_DIR)
export FRAMAC_COMPILED_PLUGINDIR=$(FRAMAC_LIBDIR)/plugins
+export OCAMLPATH:=$(FRAMAC_LIB):$(FRAMAC_PLUGINDIR)$(if $(OCAMLPATH),:,)$(OCAMLPATH)
+export OCAMLFIND_IGNORE_DUPS_IN:=$(FRAMAC_LIB):$(FRAMAC_PLUGINDIR)$(if $(OCAMLFIND_IGNORE_DUPS_IN),:,)$(OCAMLFIND_IGNORE_DUPS_IN)
+
# fake target corresponding to the clean-install of Frama-C's Makefile
.PHONY: clean-install
clean-install: ;
diff --git a/share/Makefile.dynamic_config.internal b/share/Makefile.dynamic_config.internal
index 75a0df9fbfd0f890cceffc8c7eaef42d2b96b4e9..6c50e7bba80c9ccea20a91c6c08111c773703ba3 100644
--- a/share/Makefile.dynamic_config.internal
+++ b/share/Makefile.dynamic_config.internal
@@ -36,6 +36,9 @@ export PLUGIN_LIB_DIR=$(FRAMAC_ROOT_SRCDIR)/lib/plugins
export FRAMAC_COMPILED_PLUGINDIR=$(FRAMAC_ROOT_SRCDIR)/lib/plugins
+export OCAMLPATH:=$(FRAMAC_LIB):$(PLUGIN_LIB_DIR)$(if $(OCAMLPATH),:,)$(OCAMLPATH)
+export OCAMLFIND_IGNORE_DUPS_IN:=$(FRAMAC_LIB):$(PLUGIN_LIB_DIR)$(if $(OCAMLFIND_IGNORE_DUPS_IN),:,)$(OCAMLFIND_IGNORE_DUPS_IN)
+
##########################################################################
# Local Variables:
# mode: makefile
diff --git a/share/Makefile.plugin.template b/share/Makefile.plugin.template
index efc8670691bc9d1d79d7bb8caa8dd829d05f3620..7d699300c57861a82917dfa14ecfb1e52be630f4 100644
--- a/share/Makefile.plugin.template
+++ b/share/Makefile.plugin.template
@@ -183,18 +183,26 @@ PLUGIN_RESET?=yes # Set it to no in order to NOT reset plug-in variable.
#
###############################################################################
+
+DEPEND_PKG := $(addprefix frama-c-, $(shell echo $(PLUGIN_DEPENDENCIES) | tr '[:upper:]' '[:lower:]'))
+
# Where the other plug-ins to load are already installed
ifeq ($(FRAMAC_INTERNAL),yes)
INSTALLED_PLUGIN_DIR:=$(FRAMAC_ROOT_SRCDIR)/lib/plugins
# Also inform the main Makefile that there's another plug-in to be
# considered
PLUGIN_LIST+=$(PLUGIN_DIR)/@PLUGIN_NAME@
+PLUGIN_PACKAGES:=$(PLUGIN_REQUIRES)
+
else
INSTALLED_PLUGIN_DIR:=$(PLUGIN_INSTALL_DIR)
+PLUGIN_PACKAGES:=$(PLUGIN_REQUIRES) $(DEPEND_PKG)
endif
+PLUGIN_REQUIRES += $(DEPEND_PKG)
+
# The plugin types .cm* files
PLUGIN_TYPES_CMO:=$(addsuffix .cmo,$(PLUGIN_TYPES_CMO))
PLUGIN_TYPES_CMX:=$(PLUGIN_TYPES_CMO:.cmo=.cmx)
@@ -213,6 +221,8 @@ $(notdir $(patsubst %/,%,$(PLUGIN_DIR)))))
PLUGIN_DEPENDS:=$(PLUGIN_DEPENDS) $(PLUGIN_DEPENDENCIES)
+
+
################
# ml sources #
################
@@ -426,7 +436,7 @@ PLUGIN_EXTRA_DIRS_INC:=$(patsubst %,-I $(PLUGIN_DIR)/% ,$(PLUGIN_EXTRA_DIRS))
# Set the compilation flags for the plugin
INCLUDE_FLAGS:=-I $(PLUGIN_DIR) -I $(INSTALLED_PLUGIN_DIR) \
$(PLUGIN_EXTRA_DIRS_INC) \
- $(addprefix -package ,$(PLUGIN_REQUIRES) $(LIBRARY_NAMES))
+ $(addprefix -package ,$(PLUGIN_PACKAGES) $(LIBRARY_NAMES))
$(NAME_BFLAGS):=$(BFLAGS) $(INCLUDE_FLAGS) $(PLUGIN_BFLAGS)
$(NAME_OFLAGS):=$(OFLAGS) $(INCLUDE_FLAGS) $(PLUGIN_OFLAGS)
@@ -459,9 +469,8 @@ endif
# META file
PLUGIN_PKG :=$(shell echo frama-c-@PLUGIN_NAME@ | tr '[:upper:]' '[:lower:]')
-DEPEND_PKG :=$(shell echo $(PLUGIN_DEPENDENCIES) | tr '[:upper:]' '[:lower:]')
-PLUGIN_REQUIRES += $(addprefix frama-c-,$(DEPEND_PKG))
TARGET_META :=$(PLUGIN_LIB_DIR)/META.$(PLUGIN_PKG)
+PLUGIN_GENERATED+= $(TARGET_META)
ifneq ($(PLUGIN_HAS_META),yes)
# generated META
@@ -510,7 +519,7 @@ $(TARGET_META):
$(RM) $@
$(ECHO) "description = \"$($(notdir $@).DESCRIPTION)\"" >> $@
$(ECHO) "version = \"$($(notdir $@).VERSION)\"" >> $@
- $(ECHO) "requires = \"$($(notdir $@).REQUIRES)\"" >> $@
+ $(ECHO) "requires = \"frama-c.kernel $($(notdir $@).REQUIRES)\"" >> $@
$(ECHO) "archive(byte) = \"top/$($(notdir $@).BYTE)\"" >> $@
$(ECHO) "archive(native) = \"top/$($(notdir $@).NATIVE)\"" >> $@
$(ECHO) "plugin(native) = \"top/$($(notdir $@).PLUGIN)\"" >> $@
@@ -981,7 +990,7 @@ endif #EXTRA_BYTE
endif #HAS_GUI
PLUGIN_DYN_DEP_GUI_CMX_LIST += $(PLUGIN_GUI_CMX)
-PLUGIN_DYN_CMX_LIST += $(TARGET_TOP_CMXS) $(TARGET_TOP_CMX)
+PLUGIN_DYN_CMX_LIST += $(TARGET_TOP_CMXS) $(TARGET_TOP_CMX) $(TARGET_TOP_O)
# If P1 depends on P2, then dynamically link P1.cmxs requires to have
# compiled P1's sources wrt the P2's .cmx.
ifeq ($(HAS_GUI),yes)
diff --git a/src/kernel_internals/runtime/config.ml.in b/src/kernel_internals/runtime/config.ml.in
index 75a6064a73d0dfbea83c2f71659b94de53c11146..c0f5852814ae1f34681f122f7a672be1ee95ed92 100644
--- a/src/kernel_internals/runtime/config.ml.in
+++ b/src/kernel_internals/runtime/config.ml.in
@@ -36,28 +36,41 @@ let ocamlc = "@OCAMLC@"
let ocamlopt = "@OCAMLOPT@"
let ocaml_wflags = "@WARNINGS@"
+let getenv_list name =
+ let path = Sys.getenv name in
+ Str.split (Str.regexp ":") path
+
+let add_symbolic_dir_list name = function
+ | [d] -> Filepath.add_symbolic_dir name d
+ | ds ->
+ List.iteri
+ (fun i d ->
+ let path = Printf.sprintf "%s#%d" name (succ i) in
+ Filepath.add_symbolic_dir path d)
+ ds
+
+
let datadir = try Sys.getenv "FRAMAC_SHARE" with Not_found -> "@FRAMAC_DATADIR@"
+let framac_libc = datadir ^ "/libc"
+let extra_datadir = try getenv_list "FRAMAC_EXTRA_SHARE" with Not_found -> []
+let () = add_symbolic_dir_list "FRAMAC_EXTRA_SHARE" extra_datadir
+(** After so that it has the priority for pretty printing *)
let () = Filepath.add_symbolic_dir "FRAMAC_SHARE" datadir
+
+let datadirs = datadir::extra_datadir
+
let libdir = try Sys.getenv "FRAMAC_LIB" with Not_found -> "@FRAMAC_LIBDIR@"
let () = Filepath.add_symbolic_dir "FRAMAC_LIB" libdir
let plugin_dir =
try
- let path = Sys.getenv "FRAMAC_PLUGIN" in
- Str.split (Str.regexp ":") path
+ getenv_list "FRAMAC_PLUGIN"
with Not_found ->
try [ Sys.getenv "FRAMAC_LIB" ^ "/plugins" ]
with Not_found -> [ "@FRAMAC_PLUGINDIR@" ]
let plugin_path = String.concat ":" plugin_dir
-let () = match plugin_dir with
- | [d] -> Filepath.add_symbolic_dir "FRAMAC_PLUGIN" d
- | ds ->
- Array.iteri
- (fun i d ->
- let path = Printf.sprintf "FRAMAC_PLUGIN#%d" (succ i) in
- Filepath.add_symbolic_dir path d)
- (Array.of_list ds)
+let () = add_symbolic_dir_list "FRAMAC_PLUGIN" plugin_dir
let default_cpp = "@FRAMAC_DEFAULT_CPP@"
diff --git a/src/kernel_internals/runtime/config.mli b/src/kernel_internals/runtime/config.mli
index ecdad0fbd184ddd7db887189689a1f4d0bcbb9c6..d223daf3b963e3919f947abc024a05619d04c9f4 100644
--- a/src/kernel_internals/runtime/config.mli
+++ b/src/kernel_internals/runtime/config.mli
@@ -59,7 +59,17 @@ val ocaml_wflags: string
@since Chlorine-20180501 *)
val datadir: string
- (** Directory where architecture independent files are. *)
+ (** Directory where architecture independent files are.
+ Main directory, use {!datadirs} for the others *)
+
+val datadirs: string list
+ (** Directories where architecture independent files are in order of
+ priority.
+ @since Frama-C-trunk*)
+
+val framac_libc: string
+ (** Directory where Frama-C libc headers are.
+ @since Frama-C-trunk*)
val libdir: string
(** Directory where the Frama-C kernel library is.
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 0bdc611ed92bee320148dfab22327c22d55d1de1..984fef51c452bc6ffd8b2cab48b3e9c352650d11 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -315,7 +315,7 @@ let process_stdlib_pragma name args =
match args with
| [ ACons ("pop",_) ] -> pop_stdheader (); None
| [ ACons ("push",_); AStr s ] ->
- let base_name = Config.datadir ^ "/libc" in
+ let base_name = Config.framac_libc in
let relative_name = Filepath.relativize ~base_name s in
push_stdheader relative_name;
None
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 94b276dd1dea4ff0be79d7eb93166cdad8fce598..cc22eb64b92a5628a90b5cb3d00c82b73c678fbd 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -477,7 +477,7 @@ let parse_cabs = function
(* Hypothesis: the preprocessor is POSIX compliant,
hence understands -I and -D. *)
let include_args =
- if Kernel.FramaCStdLib.get () then [Config.datadir ^ "/libc"]
+ if Kernel.FramaCStdLib.get () then [Config.framac_libc]
else []
in
let define_args =
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 86c5091279c38e3f1fb11213df420506aff6acaa..5666e51558b4c86c74e925a73b5c5f36d71bb469 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -125,7 +125,7 @@ let is_object base =
let packages = Hashtbl.create 64
-let () = List.iter (fun p -> Hashtbl.add packages p ()) Config.library_names
+let () = List.iter (fun p -> Hashtbl.add packages p ()) ("frama-c.kernel"::Config.library_names)
let missing pkg = not (Hashtbl.mem packages pkg)
@@ -281,8 +281,9 @@ let set_module_load_path path =
Klog.debug ~dkey "plugin_dir: %s" (String.concat ":" Config.plugin_dir);
load_path :=
List.fold_right (add_dir ~user:true) path
- (List.fold_right (add_dir ~user:false) Config.plugin_dir []);
- let findlib_path = String.concat ":" !load_path in
+ (List.fold_right (add_dir ~user:false) (Config.libdir::Config.plugin_dir) []);
+ let env_ocamlpath = try Str.split (Str.regexp ":") (Sys.getenv "OCAMLPATH") with Not_found -> [] in
+ let findlib_path = String.concat ":" (!load_path@env_ocamlpath) in
Klog.debug ~dkey "setting findlib path to %s" findlib_path;
Findlib.init ~env_ocamlpath:findlib_path ()
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 0efe77903f6e9bf4a2a66eec578ac4e70f50eaf5..6048de1b0a82fa0d40d1a4205d38cd22201f09d9 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -277,10 +277,10 @@ struct
include Parameter_builder.Make
(struct
- let shortname = P.shortname
- module L = L
- let messages_group = messages
- let parameters = plugin.p_parameters
+ let shortname = P.shortname
+ module L = L
+ let messages_group = messages
+ let parameters = plugin.p_parameters
end)
let prefix =
@@ -297,7 +297,7 @@ struct
module Make_specific_dir
(O: Parameter_sig.Input_with_arg)
(D: sig
- val dir: unit -> string
+ val dirs: unit -> string list
val visible_ref: bool
val force_dir: bool
end)
@@ -325,44 +325,54 @@ struct
let mk_dir d =
try
- Unix.mkdir d 0o755;
- L.warning "creating %s directory `%s'" O.option_name d;
- d
+ Unix.mkdir d 0o755;
+ L.warning "creating %s directory `%s'" O.option_name d;
+ d
with Unix.Unix_error _ ->
- L.warning "cannot create %s directory `%s'" O.option_name d;
- raise No_dir
-
- let get_and_check_dir ?(error=true) d =
- (* DO NOT Filepath.normalize the argument, since it can transform an
- absolute path into a relative one, leading to issues if a chdir occurs
- at some point. *)
- if (try Sys.is_directory d with Sys_error _ -> false) then d
- else
- if error then
- L.abort "no %s directory `%s' for plug-in `%s'"
- O.option_name
- d
- P.name
- else begin
- if force_dir then begin
- (* create the parent, if it does not exist *)
- let p = Filename.dirname d in
- if not (try Sys.is_directory p with Sys_error _ -> false) then
- ignore (mk_dir p);
- mk_dir d
- end else
- raise No_dir
- end
+ L.warning "cannot create %s directory `%s'" O.option_name d;
+ raise No_dir
+
+ let rec get_and_check_dirs error = function
+ | [] ->
+ raise No_dir
+ | d::l ->
+ if (try Sys.is_directory d with Sys_error _ -> false) then d
+ else
+ get_and_check_dirs error l
+
+ let get_and_check_dirs ?(error=true) = function
+ | [] ->
+ if error then
+ L.abort "no %s directories to look into" O.option_name
+ else
+ raise No_dir
+ | (first::_) as l ->
+ try
+ get_and_check_dirs error l
+ with
+ | No_dir when error ->
+ L.abort "no %s directory for plug-in `%s' among %a"
+ O.option_name
+ P.name
+ Pretty_utils.(pp_list ~sep:",@ " Format.pp_print_string) l
+ | No_dir when force_dir ->
+ (* create the parent, if it does not exist *)
+ let p = Filename.dirname first in
+ if not (try Sys.is_directory p with Sys_error _ -> false) then
+ ignore (mk_dir p);
+ mk_dir first
let dir ?error () =
(* get the specified dir if any *)
let d = if is_visible then Dir_name.get () else empty_string in
if d = empty_string then
- (* no specified dir: look for the default one. *)
- if is_kernel then get_and_check_dir ?error (D.dir ())
- else get_and_check_dir ?error (D.dir () ^ "/" ^ plugin_subpath)
+ (* no specified dir: look for the default one. *)
+ if is_kernel then get_and_check_dirs ?error (D.dirs ())
+ else
+ let dirs = List.map (fun x -> x ^ "/" ^ plugin_subpath) (D.dirs ()) in
+ get_and_check_dirs ?error dirs
else
- get_and_check_dir ?error d
+ get_and_check_dirs ?error [d]
let file ?error f = dir ?error () ^ "/" ^ f
@@ -371,32 +381,32 @@ struct
module Share =
Make_specific_dir
(struct
- let option_name = "share"
- let arg_name = "dir"
- let help = "set the plug-in share directory to <dir> \
+ let option_name = "share"
+ let arg_name = "dir"
+ let help = "set the plug-in share directory to <dir> \
(may be used if the plug-in is not installed at the same place as Frama-C)"
end)
(struct
- let dir () = Config.datadir
- let visible_ref = !share_visible_ref
- let force_dir = false
+ let dirs () = Config.datadirs
+ let visible_ref = !share_visible_ref
+ let force_dir = false
end)
module Session =
Make_specific_dir
(struct
- let option_name = "session"
- let arg_name = "dir"
- let help = "set the plug-in session directory to <dir>"
+ let option_name = "session"
+ let arg_name = "dir"
+ let help = "set the plug-in session directory to <dir>"
end)
(struct
- let dir () =
- if !session_is_set_ref () then !session_ref ()
- else
- try Sys.getenv "FRAMAC_SESSION"
- with Not_found -> "./.frama-c"
- let visible_ref = !session_visible_ref
- let force_dir = true
+ let dirs () = [
+ if !session_is_set_ref () then !session_ref ()
+ else
+ try Sys.getenv "FRAMAC_SESSION"
+ with Not_found -> "./.frama-c"]
+ let visible_ref = !session_visible_ref
+ let force_dir = true
end)
let () =
if is_kernel () then Journal.get_session_file := Session.file ~error:false
@@ -404,29 +414,30 @@ struct
module Config =
Make_specific_dir
(struct
- let option_name = "config"
- let arg_name = "dir"
- let help = "set the plug-in config directory to <dir> \
+ let option_name = "config"
+ let arg_name = "dir"
+ let help = "set the plug-in config directory to <dir> \
(may be used on systems with no default user directory)"
end)
(struct
- let dir () =
- let d, vis =
- if !config_is_set_ref () then !config_ref (), false
- else
- try Sys.getenv "FRAMAC_CONFIG", false
- with Not_found ->
- try Sys.getenv "USERPROFILE", false (* Win32 *)
- with Not_found ->
- (* Unix like *)
- try Sys.getenv "XDG_CONFIG_HOME", true
- with Not_found ->
- try Sys.getenv "HOME" ^ "/.config", true
- with Not_found -> ".", false
- in
- d ^ if vis then "/frama-c" else "/.frama-c"
- let visible_ref = !config_visible_ref
- let force_dir = true
+ let dirs () = [
+ let d, vis =
+ if !config_is_set_ref () then !config_ref (), false
+ else
+ try Sys.getenv "FRAMAC_CONFIG", false
+ with Not_found ->
+ try Sys.getenv "USERPROFILE", false (* Win32 *)
+ with Not_found ->
+ (* Unix like *)
+ try Sys.getenv "XDG_CONFIG_HOME", true
+ with Not_found ->
+ try Sys.getenv "HOME" ^ "/.config", true
+ with Not_found -> ".", false
+ in
+ d ^ if vis then "/frama-c" else "/.frama-c"
+ ]
+ let visible_ref = !config_visible_ref
+ let force_dir = true
end)
let help = add_group "Getting Information"
@@ -588,10 +599,10 @@ struct
(* line order below matters *)
set_range ~min:0 ~max:max_int;
if is_kernel () then begin
- Cmdline.kernel_verbose_atleast_ref := (fun n -> get () >= n);
- match !Cmdline.Kernel_verbose_level.value_if_set with
- | None -> ()
- | Some n -> set n
+ Cmdline.kernel_verbose_atleast_ref := (fun n -> get () >= n);
+ match !Cmdline.Kernel_verbose_level.value_if_set with
+ | None -> ()
+ | Some n -> set n
end
end
@@ -614,15 +625,15 @@ struct
set_range ~min:0 ~max:max_int;
add_set_hook
(fun old n ->
- (* the level of verbose is at least the level of debug *)
- if n > Verbose.get () then Verbose.set n;
+ (* the level of verbose is at least the level of debug *)
+ if n > Verbose.get () then Verbose.set n;
if n = 0 then Pervasives.decr positive_debug_ref
else if old = 0 then Pervasives.incr positive_debug_ref);
if is_kernel () then begin
- Cmdline.kernel_debug_atleast_ref := (fun n -> get () >= n);
- match !Cmdline.Kernel_debug_level.value_if_set with
- | None -> ()
- | Some n -> set n
+ Cmdline.kernel_debug_atleast_ref := (fun n -> get () >= n);
+ match !Cmdline.Kernel_debug_level.value_if_set with
+ | None -> ()
+ | Some n -> set n
end
end
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.ml b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
index d5752c3f078f98802065bc3ec40bd501d4cf1415..416f4e48137c375177750486711f2ae6ee39506e 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
@@ -111,7 +111,8 @@ let run () =
Model.on_scope (Some kf) (fun () ->
let paths,start = Compiler.compute_kf kf in
let cfg, goals = paths.Compiler.paths_cfg, paths.Compiler.paths_goals in
- let cout = open_out (Format.sprintf "/tmp/cfg_pre_%s.dot" (Kernel_function.get_name kf)) in
+ let fname = Filename.temp_file "cfg_pre_" (Kernel_function.get_name kf) in
+ let cout = open_out fname in
Compiler.Cfg.output_dot cout ~checks:(Bag.map (fun g -> g.Compiler.goal_pred) goals) cfg;
close_out cout;
Format.printf "new way@.";