diff --git a/share/analysis-scripts/README.md b/share/analysis-scripts/README.md index 54e904fbbfce03333424a16451549768d941bca4..3e95700bb8e313539399c114698008e7adca0f5d 100644 --- a/share/analysis-scripts/README.md +++ b/share/analysis-scripts/README.md @@ -58,14 +58,13 @@ By default, the scripts use the frama-c binaries located in your `$PATH` environment variable. You may want to specify different binaries, but, if you want to version your analysis, this path will depend on the computer it is run on. So, we recommend you use an unversioned file `frama-c-path.mk`. Add this -file to your `.gitignore` and define the `FRAMAC`, `FRAMAC_GUI` and -`FRAMAC_CONFIG` variables there. For instance: +file to your `.gitignore` and define the `FRAMAC` and `FRAMAC_GUI` +variables there. For instance: ```` FRAMAC_DIR=frama-c/bin FRAMAC=$(FRAMAC_DIR)/frama-c FRAMAC_GUI=$(FRAMAC_DIR)/frama-c-gui -FRAMAC_CONFIG=$(FRAMAC_DIR)/frama-c-config ```` And include this file before `frama-c.mk` in your Makefile. As this file @@ -78,12 +77,12 @@ files: ```` Then, to handle both cases when Frama-C is in the path, and when it is not, -use the following conditional definition of `FRAMAC_CONFIG` followed by the +use the following conditional definition of `FRAMAC` followed by the inclusion of `frama-c.mk`: ``` -FRAMAC_CONFIG ?= frama-c-config -include $(shell $(FRAMAC_CONFIG) -print-share-path)/analysis-scripts/frama-c.mk +FRAMAC ?= frama-c +include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk ``` @@ -164,8 +163,7 @@ Full example # optional include, in case frama-c-path.mk does not exist (frama-c in the PATH) -include frama-c-path.mk # frama-c-config is used to find the analysis scripts and frama-c.mk -FRAMAC_CONFIG ?= frama-c-config -include $(shell $(FRAMAC_CONFIG) -print-share-path)/analysis-scripts/frama-c.mk +include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk # Global parameters CPPFLAGS = -D__I586__ @@ -192,7 +190,6 @@ example.eva: EVAFLAGS += -slevel 500 FRAMAC_DIR=frama-c/bin FRAMAC=$(FRAMAC_DIR)/frama-c FRAMAC_GUI=$(FRAMAC_DIR)/frama-c-gui -FRAMAC_CONFIG=$(FRAMAC_DIR)/frama-c-config ```` ### `.gitignore` diff --git a/share/analysis-scripts/examples/example-multi.mk b/share/analysis-scripts/examples/example-multi.mk index 3c6758f68a6ae94ba0b860e882a0c143a1172855..fa25003a7127116c5195395fea4e4c1abe1e8880 100644 --- a/share/analysis-scripts/examples/example-multi.mk +++ b/share/analysis-scripts/examples/example-multi.mk @@ -1,6 +1,6 @@ -include frama-c-path.mk -FRAMAC_CONFIG ?= frama-c-config --include $(shell $(FRAMAC_CONFIG) -print-share-path)/analysis-scripts/frama-c.mk +FRAMAC ?= frama-c +-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk # Global parameters CPPFLAGS = -D__I586__ diff --git a/share/analysis-scripts/examples/example-slevel.mk b/share/analysis-scripts/examples/example-slevel.mk index 4d50809cfe520d7939476496a76a5be7a6dc70cc..d623a913abbe3b396cce5f4e2c7d02e115c96536 100644 --- a/share/analysis-scripts/examples/example-slevel.mk +++ b/share/analysis-scripts/examples/example-slevel.mk @@ -8,8 +8,8 @@ # 3. The all rule invoke the script -include frama-c-path.mk -FRAMAC_CONFIG ?= frama-c-config --include $(shell $(FRAMAC_CONFIG) -print-share-path)/analysis-scripts/frama-c.mk +FRAMAC ?= frama-c +-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk # Global parameters CPPFLAGS = -D__I586__ @@ -21,7 +21,7 @@ export FRAMA_C_MEMORY_FOOTPRINT = 8 # Default targets all: - $(shell $(FRAMAC_CONFIG) -print-share-path)/analysis-scripts/slevel-tweaker.sh -f example-slevel.mk example1 example2 + $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/slevel-tweaker.sh -f example-slevel.mk example1 example2 # Clean clean:: diff --git a/share/analysis-scripts/examples/example.mk b/share/analysis-scripts/examples/example.mk index 01854b37faf71ac2ad03849b6d90d69aab58226a..4a6130de5b3ea37c40629d1ea16052ffde4ee613 100644 --- a/share/analysis-scripts/examples/example.mk +++ b/share/analysis-scripts/examples/example.mk @@ -3,12 +3,12 @@ # frama-c binaries (e.g. FRAMAC and FRAMAC_GUI). # It is an optional include, unnecessary if frama-c is in the PATH -include frama-c-path.mk -# FRAMAC_CONFIG is defined in frama-c-path.mk when it is included, so the +# FRAMAC is defined in frama-c-path.mk when it is included, so the # line below will be safely ignored if this is the case -FRAMAC_CONFIG ?= frama-c-config +FRAMAC ?= frama-c # frama-c.mk should be included at the top of your Makefile, right below # the inclusion of frama-c-path.mk --include $(shell $(FRAMAC_CONFIG) -print-share-path)/analysis-scripts/frama-c.mk +-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk # Define global parameters CPPFLAGS += -D__I586__ -D__FRAMAC__ diff --git a/share/analysis-scripts/summary.py b/share/analysis-scripts/summary.py index 46c777f84204ff6f78e951f0d82cea62cfdfd580..a23c34e73ac9d5960d75d0140ee09f355e6f3d8d 100755 --- a/share/analysis-scripts/summary.py +++ b/share/analysis-scripts/summary.py @@ -72,8 +72,7 @@ def run_make(framac, benchmark_tag=None): bindir = framac + '/build/bin' args += [ 'FRAMAC_DIR=' + bindir, - 'FRAMAC=' + bindir + '/frama-c', - 'FRAMAC_CONFIG=' + bindir + '/frama-c-config'] + 'FRAMAC=' + bindir + '/frama-c'] if benchmark_tag is None: args += ['-j', '8'] else: diff --git a/share/analysis-scripts/template.mk b/share/analysis-scripts/template.mk index 232ab45e946235be03e4c8f5c6cfab9ac9730582..7cf5bcb29e186a6a7b80a0a261094e0915c77bb4 100644 --- a/share/analysis-scripts/template.mk +++ b/share/analysis-scripts/template.mk @@ -12,12 +12,12 @@ export FRAMA_C_MEMORY_FOOTPRINT = 8 # It is an optional include, unnecessary if frama-c is in the PATH -include frama-c-path.mk # -# FRAMAC_CONFIG is defined in frama-c-path.mk when it is included, so the +# FRAMAC is defined in frama-c-path.mk when it is included, so the # line below will be safely ignored if this is the case -FRAMAC_CONFIG ?= frama-c-config +FRAMAC ?= frama-c # # frama-c.mk contains the main rules and targets --include $(shell $(FRAMAC_CONFIG) -print-share-path)/analysis-scripts/frama-c.mk +-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk # ############################################################################### diff --git a/tests/fc_script/oracle/GNUmakefile b/tests/fc_script/oracle/GNUmakefile index c7f456e4db883cb2d9e1609c8a84a0e9767d0a2e..44f773a61a3c01b2d46d6407f2cda92926b65d7d 100644 --- a/tests/fc_script/oracle/GNUmakefile +++ b/tests/fc_script/oracle/GNUmakefile @@ -12,12 +12,12 @@ export FRAMA_C_MEMORY_FOOTPRINT = 8 # It is an optional include, unnecessary if frama-c is in the PATH -include frama-c-path.mk # -# FRAMAC_CONFIG is defined in frama-c-path.mk when it is included, so the +# FRAMAC is defined in frama-c-path.mk when it is included, so the # line below will be safely ignored if this is the case -FRAMAC_CONFIG ?= frama-c-config +FRAMAC ?= frama-c # # frama-c.mk contains the main rules and targets --include $(shell $(FRAMAC_CONFIG) -print-share-path)/analysis-scripts/frama-c.mk +-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk # ###############################################################################