diff --git a/src/plugins/e-acsl/.gitlab-ci.yml b/src/plugins/e-acsl/.gitlab-ci.yml index ea239e1cfc81d3f9ebd346f100d7c2bd7ad5649e..9a5ad8890c1a3f64aaabd2c3a6c14699e0a68ce7 100644 --- a/src/plugins/e-acsl/.gitlab-ci.yml +++ b/src/plugins/e-acsl/.gitlab-ci.yml @@ -1,6 +1,6 @@ Tests: script: - - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c master --E-ACSL $(git rev-parse HEAD) E-ACSL + - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --E-ACSL $CI_BUILD_REF --branch $CI_BUILD_REF_NAME E-ACSL tags: except: - tags diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index 6de472d98619f231a4d3d8be9fbc8573e811de32..fd737c8e32f796ab2639153fae21501126ae0ee3 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -112,11 +112,16 @@ $(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in VERSION ifeq (@MAY_RUN_TESTS@,yes) -$(PLUGIN_DIR)/tests/print.cmxs: OFLAGS=-I $(FRAMAC_LIB) -$(PLUGIN_DIR)/tests/print.cmo: BFLAGS=-I $(FRAMAC_LIB) +$(PLUGIN_DIR)/tests/print.cmxs: OFLAGS=-I $(FRAMAC_LIB) -I tests +$(PLUGIN_DIR)/tests/print.cmo: BFLAGS=-I $(FRAMAC_LIB) -I tests +$(PLUGIN_DIR)/tests/print.cmx: OFLAGS=-I $(FRAMAC_LIB) -I tests PLUGIN_TESTS_DIRS := reject runtime bts gmp no-main -E_ACSL_TESTS: $(PLUGIN_DIR)/tests/test_config \ +PLUGIN_TESTS_LIB:=tests/print.ml + +E_ACSL_TESTS: $(PLUGIN_DIR)/tests/test_config + +$(PLUGIN_DIR)/tests/ptests_config: \ $(PLUGIN_DIR)/tests/print.cmxs \ $(PLUGIN_DIR)/tests/print.cmo diff --git a/src/plugins/e-acsl/tests/print.ml b/src/plugins/e-acsl/tests/print.ml index 04a0d201831af165ee6c71956bc32efbbbe239da..1d084da5be994e1816fa9b02a9b0222a3f2f83c2 100644 --- a/src/plugins/e-acsl/tests/print.ml +++ b/src/plugins/e-acsl/tests/print.ml @@ -3,7 +3,7 @@ module Printer_extension(X:Printer.PrinterClass) = struct class printer = object inherit Printer.extensible_printer () as super - method global fmt g = + method! global fmt g = let loc, _ = Cil_datatype.Global.loc g in let file = loc.Lexing.pos_fname in if file = "" || List.exists