diff --git a/.gitignore b/.gitignore index c4204e5ff6e7981f0a1fa70898438580dd785939..7343b6eb873ae129de4a268773e8aac76a18c1ab 100644 --- a/.gitignore +++ b/.gitignore @@ -213,6 +213,12 @@ Makefile.plugin.generated /doc/developer/hello.tar.gz hello-*.tar.gz +# Dune conversion +.merlin +_build +*.install +/config.sed + ####################### # should remain empty # ####################### diff --git a/Makefile b/Makefile index 7f7d6c9d99545f4713c0c6040965cdfd3daed406..339672ee03a082413e90dd55a2b34768ec5b40dc 100644 --- a/Makefile +++ b/Makefile @@ -24,9 +24,8 @@ FRAMAC_SRC=. MAKECONFIG_DIR=share -PLUGIN_TESTS_LIST:= + include share/Makefile.common -include share/Makefile.dynamic_config.internal #Check share/Makefile.config available ifndef FRAMAC_ROOT_SRCDIR @@ -41,1311 +40,10 @@ endif VERSION:=$(shell $(CAT) VERSION) VERSION_CODENAME:=$(shell $(CAT) VERSION_CODENAME) -########################### -# Global plugin variables # -########################### - -# the directory where compiled plugin non-GUI files are stored -PLUGIN_TOP_LIB_DIR= $(PLUGIN_LIB_DIR)/top - -# the directory where compiled plugin GUI files are stored -PLUGIN_GUI_LIB_DIR= $(PLUGIN_LIB_DIR)/gui - -# the directory where the other Makefiles are -FRAMAC_SHARE = share - -# Shared lists between Makefile.plugin and Makefile : -# initialized them as "simply extended variables" (with :=) -# for a correct behavior of += (see section 6.6 of GNU Make manual) -PLUGIN_LIST := -PLUGIN_GENERATED_LIST:= -PLUGIN_CMO_LIST := -PLUGIN_CMX_LIST := -PLUGIN_META_LIST := -PLUGIN_DYN_CMI_LIST := -PLUGIN_DYN_CMO_LIST := -PLUGIN_DYN_CMX_LIST := -PLUGIN_INTERNAL_CMO_LIST:= -PLUGIN_INTERNAL_CMX_LIST:= -PLUGIN_GUI_CMO_LIST:= -PLUGIN_GUI_CMX_LIST:= -PLUGIN_DYN_DEP_GUI_CMO_LIST:= -PLUGIN_DYN_DEP_GUI_CMX_LIST:= -PLUGIN_DYN_GUI_CMO_LIST := -PLUGIN_DYN_GUI_CMX_LIST := -PLUGIN_TYPES_CMO_LIST := -PLUGIN_TYPES_CMX_LIST := -PLUGIN_DEP_LIST:= -PLUGIN_DOC_LIST := -PLUGIN_DOC_DIRS := -PLUGIN_DISTRIBUTED_LIST:= -PLUGIN_DIST_TARGET_LIST:= -PLUGIN_DIST_DOC_LIST:= -PLUGIN_BIN_DOC_LIST:= -PLUGIN_DIST_EXTERNAL_LIST:= -PLUGIN_DIST_TESTS_LIST:= -PLUGIN_DISTRIBUTED_NAME_LIST:= -MERLIN_PACKAGES:= - -PLUGIN_HEADER_SPEC_LIST := -PLUGIN_HEADER_DIRS_LIST := -PLUGIN_HEADER_EXCEPTIONS_LIST := -PLUGIN_CEA_PROPRIETARY_HEADERS_LIST := -PLUGIN_CEA_PROPRIETARY_FILES_LIST := - -# default value used for HEADER_SPEC and PLUGIN_HEADER_SPEC -DEFAULT_HEADER_SPEC := headers/header_spec.txt -# default value used for HEADER_DIRS and PLUGIN_HEADER_DIRS -DEFAULT_HEADER_DIRS := headers -# default value used for HEADER_EXCEPTIONS and PLUGIN_HEADER_EXCEPTIONS -DEFAULT_HEADER_EXCEPTIONS := configure -# default value used for CEA_PROPRIETARY_FILES and PLUGIN_CEA_PROPRIETARY_FILES -DEFAULT_CEA_PROPRIETARY_FILES := tests/non-free/% -# default value used for CEA_PROPRIETARY_HEADERS -# and PLUGIN_CEA_PROPRIETARY_HEADERS -DEFAULT_CEA_PROPRIETARY_HEADERS := CEA_PROPRIETARY - -MERLIN_PACKAGES:= - -############################### -# Additional global variables # -############################### - -# Directories containing some source code -SRC_DIRS= ptests $(PLUGIN_LIB_DIR) $(FRAMAC_SRC_DIRS) - -# Directory containing source code documentation -DOC_DIR = doc/code - -# Source files to document -MODULES_TODOC= - -# Directories to include when compiling -INCLUDES=$(addprefix -I ,$(FRAMAC_SRC_DIRS)) -I $(PLUGIN_LIB_DIR) -ifneq ($(ENABLE_GUI),no) -GUI_INCLUDES = $(addprefix -package ,$(LIBRARY_NAMES_GUI)) -else -GUI_INCLUDES = -endif - -# Files for which dependencies must be computed. -# Other files are added later in this Makefile. -FILES_FOR_OCAMLDEP+=$(PLUGIN_LIB_DIR)/*.mli - -BFLAGS = $(PACKAGES) $(FLAGS) $(DEBUG) $(INCLUDES) \ - $(FRAMAC_USER_BFLAGS) -OFLAGS = $(PACKAGES) $(FLAGS) $(DEBUG) $(INCLUDES) -compact \ - $(FRAMAC_USER_OFLAGS) - -BLINKFLAGS += -linkpkg $(BFLAGS) -linkall -custom -OLINKFLAGS += -linkpkg $(OFLAGS) -linkall - -DOC_FLAGS= -charset utf8 -colorize-code -stars -m A $(PACKAGES) $(INCLUDES) $(GUI_INCLUDES) - -ifneq ($(VERBOSEMAKE),yes) -DOC_FLAGS+= -hide-warnings -endif - -# Files that depend on external libraries -namely Zarith- whose interface -# has not been explicitely declared -opaque, hence would trigger warning 58. -# This can't be solved by Frama-C itself, we can only wait for an update of -# said library. - -NON_OPAQUE_DEPS:= - -# Libraries generated by Frama-C -GEN_BYTE_LIBS= -GEN_OPT_LIBS= - -# Libraries used in Frama-C -EXTRA_OPT_LIBS:= -PACKAGES = $(addprefix -package ,$(LIBRARY_NAMES)) -BYTE_LIBS = $(GEN_BYTE_LIBS) -OPT_LIBS = $(EXTRA_OPT_LIBS) - -OPT_LIBS+= $(GEN_OPT_LIBS) - -ICONS:= $(addprefix share/,\ - frama-c.ico frama-c.png unmark.png \ - switch-on.png switch-off.png) - -THEME_ICON_NAMES:= \ - never_tried.png \ - unknown.png \ - surely_valid.png \ - surely_invalid.png \ - considered_valid.png \ - valid_under_hyp.png \ - invalid_under_hyp.png \ - invalid_but_dead.png \ - unknown_but_dead.png \ - valid_but_dead.png \ - inconsistent.png \ - fold.png unfold.png - -THEME_ICONS_DEFAULT:= \ - $(addprefix share/theme/default/,$(THEME_ICON_NAMES)) -THEME_ICONS_COLORBLIND:= \ - $(addprefix share/theme/colorblind/,$(THEME_ICON_NAMES)) -THEME_ICONS_FLAT:= \ - $(addprefix share/theme/flat/,$(THEME_ICON_NAMES)) - -ROOT_LIBC_DIR:= share/libc -LIBC_SUBDIRS:= sys netinet net arpa -LIBC_DIR:= $(ROOT_LIBC_DIR) $(addprefix $(ROOT_LIBC_DIR)/,$(LIBC_SUBDIRS)) -LIBC_FILES:= \ - $(wildcard share/*.h share/*.c) \ - $(wildcard $(addsuffix /*.h,$(LIBC_DIR))) \ - $(wildcard $(addsuffix /*.c,$(LIBC_DIR))) - -# Checks that all .h can be included multiple times. -ALL_LIBC_HEADERS:=$(wildcard share/*.h $(addsuffix /*.h,$(LIBC_DIR))) - -check-libc: bin/toplevel.$(OCAMLBEST)$(EXE) - @echo "checking libc..."; \ - EXIT_VALUE=0; \ - for file in $(filter-out share/builtin.h,$(ALL_LIBC_HEADERS)); do \ - echo "#include \"$$file\"" > check-libc.c; \ - echo "#include \"$$file\"" >> check-libc.c; \ - FRAMAC_SHARE=share bin/toplevel.$(OCAMLBEST)$(EXE) \ - -cpp-extra-args="-Ishare/libc -nostdinc" check-libc.c \ - > $$(basename $$file .h).log 2>&1; \ - if test $$? -ne 0; then \ - if grep -q -e '#error "Frama-C:' $$file; then : ; \ - else \ - echo "$$file cannot be included twice. \ -Output is in $$(basename $$file .h).log"; \ - EXIT_VALUE=1; \ - fi; \ - else \ - rm $$(basename $$file .h).log; \ - fi; \ - done; \ - rm check-libc.c; \ - exit $$EXIT_VALUE - -clean-check-libc: - $(RM) *.log - -# Kernel files to be included in the distribution. -# Plug-ins should use PLUGIN_DISTRIB_EXTERNAL if they export something else -# than *.ml* files in their directory. -# NB: configure for the distribution is generated in the distrib directory -# itself, rather than copied: otherwise, it could include references to -# non-distributed plug-ins. -DISTRIB_FILES:=\ - $(wildcard bin/migration_scripts/*2*.sh) bin/local_export.sh \ - bin/frama-c bin/frama-c.byte bin/frama-c-gui bin/frama-c-gui.byte \ - bin/frama-c-config bin/frama-c-script \ - share/frama-c.WIN32.rc share/frama-c.Unix.rc \ - $(ICONS) $(THEME_ICONS_DEFAULT) $(THEME_ICONS_COLORBLIND) \ - $(THEME_ICONS_FLAT) \ - man/frama-c.1 doc/README \ - doc/code/docgen.ml \ - doc/code/*.css doc/code/intro_plugin.txt \ - doc/code/intro_plugin_D_and_S.txt \ - doc/code/intro_plugin_default.txt \ - doc/code/intro_kernel_plugin.txt \ - doc/code/toc_head.htm \ - doc/code/toc_tail.htm \ - doc/Makefile \ - $(filter-out ptests/ptests_config.ml,$(wildcard ptests/*.ml*)) \ - configure.in Makefile Makefile.generating \ - Changelog config.h.in \ - VERSION VERSION_CODENAME $(wildcard licenses/*) \ - $(LIBC_FILES) \ - share/analysis-scripts/analysis.mk \ - share/analysis-scripts/benchmark_database.py \ - share/analysis-scripts/cmd-dep.sh \ - share/analysis-scripts/concat-csv.sh \ - share/analysis-scripts/clone.sh \ - share/analysis-scripts/creduce.sh \ - share/analysis-scripts/epilogue.mk \ - share/analysis-scripts/fc_stubs.c \ - share/analysis-scripts/find_fun.py \ - share/analysis-scripts/flamegraph.pl \ - share/analysis-scripts/frama_c_results.py \ - share/analysis-scripts/function_finder.py \ - share/analysis-scripts/git_utils.py \ - share/analysis-scripts/list_files.py \ - share/analysis-scripts/make_template.py \ - share/analysis-scripts/make_wrapper.py \ - share/analysis-scripts/parse-coverage.sh \ - share/analysis-scripts/prologue.mk \ - share/analysis-scripts/README.md \ - share/analysis-scripts/results_display.py \ - share/analysis-scripts/summary.py \ - share/analysis-scripts/template.mk \ - $(wildcard share/emacs/*.el) share/autocomplete_frama-c \ - share/_frama-c \ - share/compliance/c11_functions.json \ - share/compliance/glibc_functions.json \ - share/compliance/nonstandard_identifiers.json \ - share/compliance/posix_identifiers.json \ - share/configure.ac \ - share/Makefile.config.in share/Makefile.common \ - share/Makefile.generic \ - share/Makefile.plugin.template share/Makefile.dynamic \ - share/Makefile.dynamic_config.external \ - share/Makefile.dynamic_config.internal \ - share/META.frama-c \ - $(filter-out src/kernel_internals/runtime/fc_config.ml, \ - $(wildcard src/kernel_internals/runtime/*.ml*)) \ - $(wildcard src/kernel_services/abstract_interp/*.ml*) \ - $(wildcard src/plugins/gui/*.ml*) \ - $(wildcard src/libraries/stdlib/*.ml*) \ - $(wildcard src/libraries/utils/*.ml*) \ - $(wildcard src/libraries/utils/*.c) \ - $(wildcard src/libraries/project/*.ml*) \ - $(filter-out src/kernel_internals/parsing/check_logic_parser.ml, \ - $(wildcard src/kernel_internals/parsing/*.ml*)) \ - $(wildcard src/kernel_internals/typing/*.ml*) \ - $(wildcard src/kernel_services/ast_data/*.ml*) \ - $(wildcard src/kernel_services/ast_queries/*.ml*) \ - $(wildcard src/kernel_services/ast_printing/*.ml*) \ - $(wildcard src/kernel_services/cmdline_parameters/*.ml*) \ - $(wildcard src/kernel_services/analysis/*.ml*) \ - $(wildcard src/kernel_services/ast_transformations/*.ml*) \ - $(wildcard src/kernel_services/plugin_entry_points/*.ml*) \ - $(wildcard src/kernel_services/visitors/*.ml*) \ - $(wildcard src/kernel_services/parsetree/*.ml*) \ - $(wildcard src/libraries/datatype/*.ml*) \ - bin/sed_get_make_major bin/sed_get_make_minor \ - INSTALL.md README.md .make-clean \ - .make-clean-stamp .force-reconfigure \ - opam/opam \ - -# Test files to be included in the distribution (without header checking). -# Plug-ins should use PLUGIN_DISTRIB_TESTS to export their test files. -DISTRIB_TESTS=$(shell git ls-files \ - tests \ - src/plugins/aorai/tests \ - src/plugins/report/tests \ - src/plugins/wp/tests | $(SED) 's/ /@/g') - - -# files that are needed to compile API documentation of external plugins -DOC_GEN_FILES:=$(addprefix doc/code/,\ - *.css intro_plugin.txt intro_kernel_plugin.txt \ - intro_plugin_default.txt intro_plugin_D_and_S \ - kernel-doc.ocamldoc \ - docgen.ml docgen.cm* *.htm) - -################ -# Main targets # -################ - -# additional compilation targets for 'make all'. -# cannot be delayed after 'make all' -EXTRAS = ptests bin/fc-config$(EXE) - -ifneq ($(ENABLE_GUI),no) -ifeq ($(HAS_LABLGTK),yes) -EXTRAS += gui -endif -endif - -all:: byte $(OCAMLBEST) $(EXTRAS) plugins_ptests_config - -.PHONY: top opt byte dist bdist rebuild rebuild-branch - -dist: clean - $(QUIET_MAKE) all - -clean-rebuild: clean - $(QUIET_MAKE) all - -rebuild: config.status - $(MAKE) smartclean - $(MAKE) depend $(FRAMAC_PARALLEL) - $(MAKE) all $(FRAMAC_PARALLEL) || \ - (touch .force-reconfigure; \ - $(MAKE) config.status && \ - $(MAKE) depend $(FRAMAC_PARALLEL) && \ - $(MAKE) all $(FRAMAC_PARALLEL)) - -sinclude .Makefile.user -# Should define FRAMAC_PARALLEL, FRAMAC_USER_FLAGS, FRAMAC_USER_MERLIN_FLAGS - -#Create link in share for local execution if -.PHONY:create_share_link -create_share_link: share/.gitignore - -# note: when using opam pin path in a cloned Frama-C git, the symbolic links -# become directories, so a different command is necessary for each situation - -share/.gitignore: share/Makefile.config - if test -f $@; then \ - for link in $$(cat $@); do \ - if test -L share$$link; then \ - rm -f share$$link \ - else \ - rm -rf share$$link; \ - fi; \ - done; \ - fi - $(RM) $@.tmp - touch $@.tmp - $(foreach dir,$(EXTERNAL_PLUGINS),\ - if test -d $(dir)/share; then \ - echo "Sharing $(dir)/link"; \ - ln -s $(realpath $(dir)/share) share/$(notdir $(dir)); \ - echo /$(notdir $(dir)) >> $@.tmp; \ - fi; ) - mv $@.tmp $@ - -ifeq ("$(DEVELOPMENT)","yes") -all:: share/.gitignore -endif - -clean_share_link: - if test -f share/.gitignore; then \ - for link in $$(cat share/.gitignore); do \ - if test -L share$$link; then \ - rm -f share$$link \ - else \ - rm -rf share$$link; \ - fi; \ - done; \ - rm share/.gitignore; \ - fi - -clean:: clean_share_link - -############## -# Ocamlgraph # -############## - -# dgraph (included in ocamlgraph) -#[LC] Cf https://github.com/backtracking/ocamlgraph/pull/32 -ifeq ($(HAS_GNOMECANVAS),yes) -ifneq ($(ENABLE_GUI),no) -GRAPH_GUICMO= dgraph.cmo -GRAPH_GUICMX= dgraph.cmx -GRAPH_GUIO= dgraph.o -HAS_DGRAPH=yes -else # enable_gui is no: disable dgraph -HAS_DGRAPH=no -endif -else # gnome_canvas is not yes: disable dgraph -HAS_DGRAPH=no -endif - -################## -# Frama-C Kernel # -################## - -# Libraries which could be compiled fully independently -####################################################### - -VERY_FIRST_CMO = src/kernel_internals/runtime/frama_c_init.cmo -CMO += $(VERY_FIRST_CMO) - -LIB_CMO =\ - src/libraries/stdlib/transitioning \ - src/libraries/stdlib/FCHashtbl \ - src/libraries/stdlib/extlib \ - src/libraries/datatype/unmarshal \ - src/libraries/datatype/unmarshal_z \ - src/libraries/datatype/structural_descr \ - src/libraries/datatype/type \ - src/libraries/datatype/descr \ - src/libraries/utils/filepath \ - src/libraries/utils/sanitizer \ - src/libraries/utils/pretty_utils \ - src/libraries/utils/hook \ - src/libraries/utils/bag \ - src/libraries/utils/wto \ - src/libraries/utils/vector \ - src/libraries/utils/indexer \ - src/libraries/utils/rgmap \ - src/libraries/utils/bitvector \ - src/libraries/utils/qstack \ - src/libraries/stdlib/integer \ - src/libraries/utils/json \ - src/libraries/utils/markdown \ - src/libraries/utils/rich_text \ - src/libraries/utils/dotgraph - -NON_OPAQUE_DEPS+=\ - src/libraries/datatype/unmarshal_z \ - src/libraries/stdlib/integer - -LIB_CMO:= $(addsuffix .cmo,$(LIB_CMO)) -CMO += $(LIB_CMO) - -# Very first files to be linked (most modules use them) -############################### - -FIRST_CMO= src/kernel_internals/runtime/fc_config \ - src/kernel_internals/runtime/gui_init \ - src/kernel_services/plugin_entry_points/log \ - src/kernel_services/cmdline_parameters/cmdline \ - src/libraries/project/project_skeleton \ - src/libraries/datatype/datatype \ - src/kernel_services/plugin_entry_points/journal - -# project_skeleton requires log -# datatype requires project_skeleton -# rangemap requires datatype - -FIRST_CMO:= $(addsuffix .cmo,$(FIRST_CMO)) -CMO += $(FIRST_CMO) - -#Project (Project_skeleton must be linked before Journal) -PROJECT_CMO= \ - state \ - state_dependency_graph \ - state_topological \ - state_selection \ - project \ - state_builder -PROJECT_CMO:= $(patsubst %,src/libraries/project/%.cmo,$(PROJECT_CMO)) -CMO += $(PROJECT_CMO) - -# kernel -######## - -KERNEL_CMO=\ - src/libraries/utils/utf8_logic.cmo \ - src/libraries/utils/binary_cache.cmo \ - src/libraries/utils/hptmap.cmo \ - src/libraries/utils/hptset.cmo \ - src/libraries/utils/escape.cmo \ - src/kernel_services/ast_queries/cil_datatype.cmo \ - src/kernel_services/cmdline_parameters/typed_parameter.cmo \ - src/kernel_services/plugin_entry_points/dynamic.cmo \ - src/kernel_services/cmdline_parameters/parameter_category.cmo \ - src/kernel_services/cmdline_parameters/parameter_customize.cmo \ - src/kernel_services/cmdline_parameters/parameter_state.cmo \ - src/kernel_services/cmdline_parameters/parameter_builder.cmo \ - src/kernel_services/plugin_entry_points/plugin.cmo \ - src/kernel_services/plugin_entry_points/kernel.cmo \ - src/libraries/utils/unicode.cmo \ - src/kernel_services/plugin_entry_points/emitter.cmo \ - src/libraries/utils/floating_point.cmo \ - src/libraries/utils/rangemap.cmo \ - src/kernel_services/ast_printing/cil_types_debug.cmo \ - src/kernel_services/ast_printing/printer_builder.cmo \ - src/libraries/utils/cilconfig.cmo \ - src/kernel_internals/typing/alpha.cmo \ - src/kernel_services/ast_queries/cil_state_builder.cmo \ - src/kernel_internals/runtime/machdeps.cmo \ - src/kernel_services/ast_queries/cil_const.cmo \ - src/kernel_services/ast_queries/logic_env.cmo \ - src/kernel_services/ast_queries/logic_const.cmo \ - src/kernel_services/visitors/visitor_behavior.cmo \ - src/kernel_services/ast_queries/cil.cmo \ - src/kernel_internals/parsing/errorloc.cmo \ - src/kernel_services/ast_printing/cil_printer.cmo \ - src/kernel_services/ast_printing/cil_descriptive_printer.cmo \ - src/kernel_services/parsetree/cabs.cmo \ - src/kernel_services/parsetree/cabshelper.cmo \ - src/kernel_services/ast_printing/logic_print.cmo \ - src/kernel_services/ast_queries/logic_utils.cmo \ - src/kernel_internals/parsing/logic_parser.cmo \ - src/kernel_internals/parsing/logic_lexer.cmo \ - src/kernel_services/ast_queries/logic_typing.cmo \ - src/kernel_services/ast_queries/acsl_extension.cmo \ - src/kernel_services/ast_queries/ast_info.cmo \ - src/kernel_services/ast_data/ast.cmo \ - src/kernel_services/ast_printing/cprint.cmo \ - src/kernel_services/visitors/cabsvisit.cmo \ - src/kernel_internals/typing/cabs2cil.cmo \ - src/kernel_services/ast_data/globals.cmo \ - src/kernel_internals/typing/cfg.cmo \ - src/kernel_services/ast_data/kernel_function.cmo \ - src/kernel_services/ast_data/property.cmo \ - src/kernel_services/ast_data/property_status.cmo \ - src/kernel_services/ast_data/annotations.cmo \ - src/kernel_services/ast_printing/printer.cmo \ - src/kernel_internals/typing/logic_builtin.cmo \ - src/kernel_services/ast_printing/cabs_debug.cmo \ - src/kernel_internals/parsing/lexerhack.cmo \ - src/kernel_internals/parsing/clexer.cmo \ - src/kernel_internals/parsing/cparser.cmo \ - src/kernel_internals/parsing/logic_preprocess.cmo \ - src/kernel_internals/typing/mergecil.cmo \ - src/kernel_internals/typing/rmtmps.cmo \ - src/kernel_internals/typing/oneret.cmo \ - src/kernel_internals/typing/frontc.cmo \ - src/kernel_internals/typing/substitute_const_globals.cmo \ - src/kernel_services/analysis/ordered_stmt.cmo \ - src/kernel_services/analysis/wto_statement.cmo \ - src/kernel_services/analysis/dataflows.cmo \ - src/kernel_services/analysis/dataflow2.cmo \ - src/kernel_services/analysis/stmts_graph.cmo \ - src/kernel_services/analysis/dominators.cmo \ - src/kernel_services/analysis/service_graph.cmo \ - src/kernel_services/analysis/undefined_sequence.cmo \ - src/kernel_services/analysis/interpreted_automata.cmo \ - src/kernel_services/ast_data/alarms.cmo \ - src/kernel_services/ast_printing/description.cmo \ - src/kernel_services/abstract_interp/lattice_messages.cmo \ - src/kernel_services/abstract_interp/abstract_interp.cmo \ - src/kernel_services/abstract_interp/bottom.cmo \ - src/kernel_services/abstract_interp/int_Base.cmo \ - src/kernel_services/analysis/bit_utils.cmo \ - src/kernel_services/abstract_interp/fc_float.cmo \ - src/kernel_services/abstract_interp/float_interval.cmo \ - src/kernel_services/abstract_interp/fval.cmo \ - src/kernel_services/abstract_interp/int_interval.cmo \ - src/kernel_services/abstract_interp/int_set.cmo \ - src/kernel_services/abstract_interp/int_val.cmo \ - src/kernel_services/abstract_interp/ival.cmo \ - src/kernel_services/abstract_interp/base.cmo \ - src/kernel_services/abstract_interp/origin.cmo \ - src/kernel_services/abstract_interp/map_lattice.cmo \ - src/kernel_services/abstract_interp/tr_offset.cmo \ - src/kernel_services/abstract_interp/offsetmap.cmo \ - src/kernel_services/abstract_interp/int_Intervals.cmo \ - src/kernel_services/abstract_interp/locations.cmo \ - src/kernel_services/abstract_interp/lmap.cmo \ - src/kernel_services/abstract_interp/lmap_bitwise.cmo \ - src/kernel_services/visitors/visitor.cmo \ - src/kernel_services/ast_data/statuses_by_call.cmo \ - src/kernel_services/ast_printing/printer_tag.cmo \ - $(PLUGIN_TYPES_CMO_LIST) \ - src/kernel_services/plugin_entry_points/db.cmo \ - src/libraries/utils/command.cmo \ - src/libraries/utils/task.cmo \ - src/kernel_services/ast_queries/filecheck.cmo \ - src/kernel_services/ast_queries/json_compilation_database.cmo \ - src/kernel_services/ast_queries/file.cmo \ - src/kernel_internals/typing/translate_lightweight.cmo \ - src/kernel_internals/typing/ghost_cfg.cmo \ - src/kernel_internals/typing/ghost_accesses.cmo \ - src/kernel_internals/typing/allocates.cmo \ - src/kernel_internals/typing/unroll_loops.cmo \ - src/kernel_internals/typing/asm_contracts.cmo \ - src/kernel_services/analysis/loop.cmo \ - src/kernel_services/analysis/exn_flow.cmo \ - src/kernel_services/analysis/destructors.cmo \ - src/kernel_services/analysis/logic_interp.cmo \ - src/kernel_internals/typing/infer_annotations.cmo \ - src/kernel_services/ast_transformations/clone.cmo \ - src/kernel_services/ast_transformations/filter.cmo \ - src/kernel_services/ast_transformations/inline.cmo \ - src/kernel_internals/runtime/special_hooks.cmo \ - src/kernel_internals/runtime/messages.cmo - -CMO += $(KERNEL_CMO) - -MLI_ONLY+=\ - src/libraries/utils/hptmap_sig.mli \ - src/kernel_services/cmdline_parameters/parameter_sig.mli \ - src/kernel_services/ast_data/cil_types.mli \ - src/kernel_services/parsetree/logic_ptree.mli \ - src/kernel_services/ast_printing/printer_api.mli \ - src/kernel_services/abstract_interp/float_sig.mli \ - src/kernel_services/abstract_interp/float_interval_sig.mli \ - src/kernel_services/abstract_interp/lattice_type.mli \ - src/kernel_services/abstract_interp/eva_lattice_type.mli \ - src/kernel_services/abstract_interp/int_Intervals_sig.mli \ - src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli \ - src/kernel_services/abstract_interp/offsetmap_sig.mli \ - src/kernel_services/abstract_interp/lmap_sig.mli \ - src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli - -NO_MLI+= src/kernel_services/parsetree/cabs.mli \ - src/kernel_internals/runtime/machdep_ppc_32.mli \ - src/kernel_internals/runtime/machdep_x86_16.mli \ - src/kernel_internals/runtime/machdep_x86_32.mli \ - src/kernel_internals/runtime/machdep_x86_64.mli \ - src/kernel_services/ast_printing/cabs_debug.mli \ - src/kernel_internals/parsing/logic_lexer.mli \ - src/kernel_internals/parsing/lexerhack.mli \ - -MODULES_NODOC+= src/kernel_internals/runtime/machdep_ppc_32.ml \ - src/kernel_internals/runtime/machdep_x86_16.ml \ - src/kernel_internals/runtime/machdep_x86_32.ml \ - src/kernel_internals/runtime/machdep_x86_64.ml \ - external/unmarshal_z.mli - - -GENERATED += $(addprefix src/kernel_internals/parsing/,\ - clexer.ml cparser.ml cparser.mli \ - logic_lexer.ml logic_parser.ml \ - logic_parser.mli logic_preprocess.ml) - - -.PHONY: check-logic-parser-wildcard -check-logic-parser-wildcard: - cd src/kernel_internals/parsing && ocaml check_logic_parser.ml - -NON_OPAQUE_DEPS+= src/kernel_services/plugin_entry_points/dynamic - -# C Bindings -############ - -GEN_C_BINDINGS=src/libraries/utils/c_bindings.o -GEN_C_BINDINGS_FLAGS= -fPIC -GEN_BYTE_LIBS+= $(GEN_C_BINDINGS) -GEN_OPT_LIBS+= $(GEN_C_BINDINGS) - -src/libraries/utils/c_bindings.o: src/libraries/utils/c_bindings.c - $(PRINT_CC) $@ - $(CC) $(GEN_C_BINDINGS_FLAGS) -c -I$(call winpath,$(OCAMLLIB)) -O3 -Wall -o $@ $< - -# Common startup module -# All link command should add it as last linked module and depend on it. -######################################################################## - -STARTUP_CMO=src/kernel_internals/runtime/boot.cmo -STARTUP_CMX=$(STARTUP_CMO:.cmo=.cmx) - -# GUI modules -# See below for GUI compilation -############################################################################## - -WTOOLKIT= \ - wutil widget wbox wfile wpane wpalette wtext wtable - -ifeq ("$(LABLGTK_VERSION)","3") - -src/plugins/gui/GSourceView.ml: src/plugins/gui/GSourceView3.ml.in - $(CP) $< $@ - $(CHMOD_RO) $@ - -src/plugins/gui/GSourceView.mli: src/plugins/gui/GSourceView3.mli.in - $(CP) $< $@ - $(CHMOD_RO) $@ - -else -src/plugins/gui/GSourceView.ml: src/plugins/gui/GSourceView2.ml.in - $(CP) $< $@ - $(CHMOD_RO) $@ - -src/plugins/gui/GSourceView.mli: src/plugins/gui/GSourceView2.mli.in - $(CP) $< $@ - $(CHMOD_RO) $@ - -endif - -SOURCEVIEWCOMPAT:=GSourceView -GENERATED+=src/plugins/gui/GSourceView.ml src/plugins/gui/GSourceView.mli \ - src/plugins/gui/dgraph_helper.ml src/plugins/gui/gtk_compat.ml - -ifeq ($(LABLGTK),lablgtk3) -src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.3.ml - $(CP) $< $@ - $(CHMOD_RO) $@ -else -src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.2.ml - $(CP) $< $@ - $(CHMOD_RO) $@ -endif -GENERATED+=src/plugins/gui/gtk_compat.ml - -ifeq ($(HAS_DGRAPH),yes) - DGRAPHFILES:=debug_manager - src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.yes.ml - $(CP) $< $@ - $(CHMOD_RO) $@ -else - DGRAPHFILES:= - src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.no.ml - $(CP) $< $@ - $(CHMOD_RO) $@ -endif - -SINGLE_GUI_CMO:= \ - wutil_once \ - gtk_compat \ - $(WTOOLKIT) \ - $(SOURCEVIEWCOMPAT) \ - gui_parameters \ - gtk_helper \ - dgraph_helper \ - gtk_form \ - source_viewer pretty_source source_manager book_manager \ - warning_manager \ - filetree \ - launcher \ - menu_manager \ - history \ - gui_printers \ - design \ - analyses_manager file_manager project_manager \ - help_manager \ - $(DGRAPHFILES) \ - property_navigator \ - -SINGLE_GUI_CMO:= $(patsubst %,src/plugins/gui/%.cmo,$(SINGLE_GUI_CMO)) - -############################################################################### -# # -#################### # -# Plug-in sections # # -#################### # -# # -# For 'internal' developers: # -# you can add your own plug-in here, # -# but it is better to have your own separated Makefile # -############################################################################### - -########### -# Metrics # -########### - -PLUGIN_ENABLE:=$(ENABLE_METRICS) -PLUGIN_NAME:=Metrics -PLUGIN_DISTRIBUTED:=yes -PLUGIN_DIR:=src/plugins/metrics -PLUGIN_CMO:= metrics_parameters css_html metrics_base metrics_acsl \ - metrics_cabs metrics_cilast metrics_coverage \ - register -PLUGIN_GUI_CMO:= metrics_gui register_gui -PLUGIN_DEPENDENCIES:=Eva -PLUGIN_INTERNAL_TEST:=yes -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -############# -# Callgraph # -############# - -PLUGIN_ENABLE:=$(ENABLE_CALLGRAPH) -PLUGIN_NAME:=Callgraph -PLUGIN_DISTRIBUTED:=yes -PLUGIN_DIR:=src/plugins/callgraph -PLUGIN_CMO:= options journalize subgraph cg services uses register -ifeq ($(HAS_DGRAPH),yes) -PLUGIN_GUI_CMO:=cg_viewer -else -PLUGIN_GUI_CMO:= -PLUGIN_DISTRIB_EXTERNAL:=cg_viewer.ml -endif -PLUGIN_CMI:= callgraph_api -PLUGIN_INTERNAL_TEST:=yes -PLUGIN_TESTS_DIRS:=callgraph -PLUGIN_TESTS_LIB:=tests/callgraph/function_pointer.ml -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - - -################## -# Evolved Value Analysis # -################## - -PLUGIN_ENABLE:=$(ENABLE_EVA) -PLUGIN_NAME:=Eva -PLUGIN_DIR:=src/plugins/value -PLUGIN_EXTRA_DIRS:=engine values domains api domains/cvalue domains/apron \ - domains/gauges domains/equality legacy partitioning utils gui_files \ - api values/numerors domains/numerors -PLUGIN_TESTS_DIRS+=value/traces - -# Files for the binding to Apron domains. Only available if Apron is available. -ifeq ($(HAS_APRON),yes) -PLUGIN_REQUIRES+= apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron gmp -APRON_CMO:= domains/apron/apron_domain -else -APRON_CMO:= -PLUGIN_DISTRIB_EXTERNAL+= \ - domains/apron/apron_domain.ml domains/apron/apron_domain.mli -endif - -# Files for the numerors domain. Only available is MPFR is available. -NUMERORS_FILES:= \ - values/numerors/numerors_utils values/numerors/numerors_float \ - values/numerors/numerors_interval values/numerors/numerors_arithmetics \ - values/numerors/numerors_value domains/numerors/numerors_domain - -ifeq ($(HAS_MPFR),yes) -PLUGIN_REQUIRES+= gmp -PLUGIN_TESTS_DIRS+=value/numerors -NUMERORS_CMO:= $(NUMERORS_FILES) -else -# Do not compile numerors files, but include them in the distributed files. -NUMERORS_CMO:= -PLUGIN_DISTRIB_EXTERNAL+= $(addsuffix .ml,$(NUMERORS_FILES)) -PLUGIN_DISTRIB_EXTERNAL+= $(addsuffix .mli,$(NUMERORS_FILES)) -endif - -# General rules for ordering files within PLUGIN_CMO: -# - try to keep the legacy Value before Eva -PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \ - utils/value_perf utils/eva_annotations \ - utils/value_util utils/red_statuses \ - utils/mark_noresults \ - utils/widen_hints_ext utils/widen \ - partitioning/split_return \ - partitioning/per_stmt_slevel \ - utils/library_functions \ - utils/eval_typ utils/backward_formals \ - alarmset eval utils/structure utils/abstract \ - values/value_product values/location_lift \ - values/cvalue_forward values/cvalue_backward \ - values/main_values values/main_locations \ - values/offsm_value values/sign_value \ - legacy/eval_op legacy/function_args \ - domains/domain_store domains/domain_builder \ - domains/domain_product domains/domain_lift domains/unit_domain \ - domains/printer_domain \ - domains/traces_domain \ - domains/simple_memory \ - domains/octagons \ - domains/gauges/gauges_domain \ - domains/hcexprs \ - domains/equality/equality domains/equality/equality_domain \ - domains/offsm_domain \ - domains/symbolic_locs \ - domains/sign_domain \ - domains/cvalue/warn domains/cvalue/locals_scoping \ - domains/cvalue/cvalue_offsetmap \ - utils/value_results \ - domains/cvalue/builtins domains/cvalue/builtins_malloc \ - domains/cvalue/builtins_string domains/cvalue/builtins_misc \ - domains/cvalue/builtins_memory domains/cvalue/builtins_print_c \ - domains/cvalue/builtins_watchpoint \ - domains/cvalue/builtins_float domains/cvalue/builtins_split \ - domains/inout_domain \ - utils/state_import \ - legacy/eval_terms legacy/eval_annots \ - domains/powerset engine/transfer_logic \ - domains/cvalue/cvalue_transfer domains/cvalue/cvalue_init \ - domains/cvalue/cvalue_specification \ - domains/cvalue/cvalue_domain \ - engine/subdivided_evaluation engine/evaluation engine/abstractions \ - engine/recursion engine/transfer_stmt engine/transfer_specification \ - partitioning/auto_loop_unroll \ - partitioning/partition partitioning/partitioning_parameters \ - partitioning/partitioning_index partitioning/trace_partitioning \ - engine/mem_exec engine/iterator engine/initialization \ - engine/compute_functions engine/analysis register \ - api/general_requests \ - utils/unit_tests \ - api/values_request \ - $(APRON_CMO) $(NUMERORS_CMO) -PLUGIN_CMI:= values/abstract_value values/abstract_location \ - domains/abstract_domain domains/simpler_domains -PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen Server - -# These files are used by the GUI, but do not depend on Lablgtk -VALUE_GUI_AUX:=gui_files/gui_types gui_files/gui_eval \ - gui_files/gui_callstacks_filters -PLUGIN_GUI_CMO:=$(VALUE_GUI_AUX) gui_files/gui_callstacks_manager \ - gui_files/gui_red gui_files/register_gui - -PLUGIN_INTERNAL_TEST:= yes -PLUGIN_TESTS_LIB=tests/float/fval_test.ml -PLUGIN_DISTRIBUTED:=yes -VALUE_TYPES:=$(addprefix src/plugins/value_types/,\ - cilE cvalue precise_locs value_types widen_type) -PLUGIN_TYPES_CMO:=$(VALUE_TYPES) -PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(VALUE_TYPES)) - -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -################## -# Occurrence # -################## - -PLUGIN_ENABLE:=$(ENABLE_OCCURRENCE) -PLUGIN_NAME:=Occurrence -PLUGIN_DISTRIBUTED:=yes -PLUGIN_DIR:=src/plugins/occurrence -PLUGIN_CMO:= options register -PLUGIN_GUI_CMO:=register_gui -PLUGIN_INTRO:=doc/code/intro_occurrence.txt -PLUGIN_INTERNAL_TEST:=yes -PLUGIN_DEPENDENCIES:=Eva -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -################################################ -# Runtime Error Annotation Generation analysis # -################################################ - -PLUGIN_ENABLE:=$(ENABLE_RTEGEN) -PLUGIN_NAME:=RteGen -PLUGIN_DIR:=src/plugins/rte -PLUGIN_CMO:= options generator rte flags visit register -PLUGIN_DISTRIBUTED:=yes -PLUGIN_INTERNAL_TEST:=yes -PLUGIN_TESTS_DIRS:=rte rte_manual -PLUGIN_TESTS_LIB:=\ - tests/rte/my_annotation/my_annotation.ml \ - tests/rte/rte_api/rte_get_annot.ml \ - tests/rte/compute_annot/compute_annot.ml \ - tests/rte/my_annot_proxy/my_annot_proxy.ml -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -################# -# From analysis # -################# - -PLUGIN_ENABLE:=$(ENABLE_FROM_ANALYSIS) -PLUGIN_NAME:=From -PLUGIN_DIR:=src/plugins/from -PLUGIN_CMO:= from_parameters from_compute \ - functionwise callwise from_register -PLUGIN_GUI_CMO:=from_register_gui -PLUGIN_TESTS_DIRS:=idct test float -PLUGIN_DISTRIBUTED:=yes -PLUGIN_INTERNAL_TEST:=yes -FROM_TYPES:=src/plugins/value_types/function_Froms -PLUGIN_TYPES_CMO:=$(FROM_TYPES) -PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(FROM_TYPES)) -PLUGIN_DEPENDENCIES:=Callgraph Eva Postdominators - -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -################## -# Users analysis # -################## - -PLUGIN_ENABLE:=$(ENABLE_USERS) -PLUGIN_NAME:=Users -PLUGIN_DIR:=src/plugins/users -PLUGIN_CMO:= users_register -PLUGIN_NO_TEST:=yes -PLUGIN_DISTRIBUTED:=yes -PLUGIN_INTERNAL_TEST:=yes -PLUGIN_DEPENDENCIES:=Callgraph Eva - -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -######################## -# Constant propagation # -######################## - -PLUGIN_ENABLE:=$(ENABLE_CONSTANT_PROPAGATION) -PLUGIN_NAME:=Constant_Propagation -PLUGIN_DIR:=src/plugins/constant_propagation -PLUGIN_TESTS_LIB:=tests/constant_propagation/introduction_of_non_explicit_cast.ml -PLUGIN_CMO:= propagationParameters \ - api -PLUGIN_DISTRIBUTED:=yes -PLUGIN_INTERNAL_TEST:=yes -PLUGIN_DEPENDENCIES:=Eva - -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -################### -# Post-dominators # -################### - -PLUGIN_ENABLE:=$(ENABLE_POSTDOMINATORS) -PLUGIN_NAME:=Postdominators -PLUGIN_DIR:=src/plugins/postdominators -PLUGIN_CMO:= postdominators_parameters print compute -PLUGIN_NO_TEST:=yes -PLUGIN_DISTRIBUTED:=yes -PLUGIN_INTERNAL_TEST:=yes -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -######### -# inout # -######### - -PLUGIN_ENABLE:=$(ENABLE_INOUT) -PLUGIN_NAME:=Inout -PLUGIN_DIR:=src/plugins/inout -PLUGIN_CMO:= inout_parameters cumulative_analysis \ - operational_inputs outputs inputs derefs register -PLUGIN_NO_TEST:=yes -PLUGIN_DISTRIBUTED:=yes -PLUGIN_INTERNAL_TEST:=yes -INOUT_TYPES:=src/plugins/value_types/inout_type -PLUGIN_TYPES_CMO:=$(INOUT_TYPES) -PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(INOUT_TYPES)) -PLUGIN_DEPENDENCIES:=Callgraph Eva From - -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -################### -# Impact analysis # -################### - -PLUGIN_ENABLE:=$(ENABLE_IMPACT) -PLUGIN_NAME:=Impact -PLUGIN_DIR:=src/plugins/impact -PLUGIN_CMO:= options pdg_aux reason_graph compute_impact register -PLUGIN_GUI_CMO:= register_gui -PLUGIN_DISTRIBUTED:=yes -PLUGIN_INTERNAL_TEST:=yes -PLUGIN_DEPENDENCIES:=Inout Eva Pdg Slicing - -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -################################## -# PDG : program dependence graph # -################################## - -PLUGIN_ENABLE:=$(ENABLE_PDG) -PLUGIN_NAME:=Pdg -PLUGIN_DIR:=src/plugins/pdg -PLUGIN_TESTS_LIB:=tests/pdg/dyn_dpds.ml \ - tests/pdg/sets.ml -PLUGIN_TESTS_DIRS:=pdg -PLUGIN_CMO:= pdg_parameters \ - ctrlDpds \ - pdg_state \ - build \ - sets \ - annot \ - marks \ - register - -PDG_TYPES:=pdgIndex pdgTypes pdgMarks -PDG_TYPES:=$(addprefix src/plugins/pdg_types/,$(PDG_TYPES)) -PLUGIN_TYPES_CMO:=$(PDG_TYPES) - -PLUGIN_INTRO:=doc/code/intro_pdg.txt -PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(PDG_TYPES)) -PLUGIN_DEPENDENCIES:=Callgraph Eva From -PLUGIN_DISTRIBUTED:=yes -PLUGIN_INTERNAL_TEST:=yes - -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -################################################ -# Scope : show different kinds of dependencies # -################################################ - -PLUGIN_ENABLE:=$(ENABLE_SCOPE) -PLUGIN_NAME:=Scope -PLUGIN_DIR:=src/plugins/scope -PLUGIN_TESTS_LIB:=tests/scope/bts971.ml \ - tests/scope/zones.ml -PLUGIN_CMO:= datascope zones defs -PLUGIN_GUI_CMO:=dpds_gui -PLUGIN_DEPENDENCIES:=Eva Inout -PLUGIN_INTRO:=doc/code/intro_scope.txt -PLUGIN_DISTRIBUTED:=yes -PLUGIN_INTERNAL_TEST:=yes -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -##################################### -# Sparecode : unused code detection # -##################################### - -PLUGIN_ENABLE:=$(ENABLE_SPARECODE) -PLUGIN_NAME:=Sparecode -PLUGIN_DIR:=src/plugins/sparecode -PLUGIN_CMO:= sparecode_params globs spare_marks transform register -PLUGIN_INTRO:=doc/code/intro_sparecode.txt -PLUGIN_DISTRIBUTED:=yes -PLUGIN_INTERNAL_TEST:=yes -PLUGIN_DEPENDENCIES:=Pdg Eva Users - -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -########### -# Slicing # -########### - -PLUGIN_ENABLE:=$(ENABLE_SLICING) -PLUGIN_NAME:=Slicing -PLUGIN_DIR:=src/plugins/slicing -PLUGIN_CMO:= slicingInternals \ - slicingTypes \ - slicingParameters \ - slicingState \ - slicingMacros \ - slicingMarks \ - slicingActions \ - fct_slice \ - printSlice \ - slicingProject \ - slicingTransform \ - slicingSelect \ - slicingCmds \ - api \ - register - -PLUGIN_GUI_CMO:=register_gui - -PLUGIN_INTRO:=doc/code/intro_slicing.txt -PLUGIN_UNDOC:=register.ml # slicing_gui.ml - -PLUGIN_TESTS_DIRS:= slicing -PLUGIN_TESTS_LIB:= tests/slicing/libSelect.ml tests/slicing/libAnim.ml \ - tests/slicing/simple_intra_slice.ml tests/slicing/combine.ml \ - tests/slicing/ex_spec_interproc.ml tests/slicing/horwitz.ml \ - tests/slicing/mark_all_slices.ml tests/slicing/merge.ml \ - tests/slicing/min_call.ml tests/slicing/select_by_annot.ml \ - tests/slicing/select_simple.ml tests/slicing/simple_intra_slice.ml \ - tests/slicing/slice_no_body.ml tests/slicing/switch.ml \ - tests/slicing/adpcm.ml -PLUGIN_DISTRIBUTED:=yes -PLUGIN_INTERNAL_TEST:=yes -PLUGIN_DEPENDENCIES:=Pdg Callgraph Eva Sparecode - -$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) - -##################### -# External plug-ins # -##################### - -define INCLUDE_PLUGIN -FRAMAC_SHARE:=$(FRAMAC_ROOT_SRCDIR)/share -FRAMAC_PLUGIN:=$(FRAMAC_ROOT_SRCDIR)/lib/plugins -FRAMAC_PLUGIN_GUI:=$(FRAMAC_ROOT_SRCDIR)/lib/plugins/gui -PLUGIN_DIR:=$(1) -include $(1)/Makefile -endef - -$(foreach p,$(EXTERNAL_PLUGINS),$(eval $(call INCLUDE_PLUGIN,$p))) - -############################################################################### -# # -########################### # -# End of plug-in sections # # -########################### # -# # -############################################################################### - -##################### -# Generic variables # -##################### - -CMX = $(CMO:.cmo=.cmx) -CMI = $(CMO:.cmo=.cmi) - -ALL_CMO = $(CMO) $(PLUGIN_CMO_LIST) $(STARTUP_CMO) -ALL_CMX = $(CMX) $(PLUGIN_CMX_LIST) $(STARTUP_CMX) - -FILES_FOR_OCAMLDEP+= $(addsuffix /*.mli,$(FRAMAC_SRC_DIRS)) \ - $(addsuffix /*.ml,$(FRAMAC_SRC_DIRS)) - -MODULES_TODOC+=$(filter-out $(MODULES_NODOC),\ - $(MLI_ONLY) $(NO_MLI:.mli=.ml) \ - $(filter-out $(NO_MLI),\ - $(filter-out $(PLUGIN_TYPES_CMO_LIST:.cmo=.mli),$(CMO:.cmo=.mli)))) - -################################ -# toplevel.{byte,opt} binaries # -################################ - -ALL_BATCH_CMO= $(filter-out src/kernel_internals/runtime/gui_init.cmo,\ - $(ALL_CMO)) -ALL_BATCH_CMX= $(filter-out src/kernel_internals/runtime/gui_init.cmx,\ - $(ALL_CMX)) - -bin/toplevel.byte$(EXE): $(ALL_BATCH_CMO) $(GEN_BYTE_LIBS) \ - $(PLUGIN_DYN_CMO_LIST) - $(PRINT_LINKING) $@ - $(OCAMLC) $(BLINKFLAGS) -o $@ $(BYTE_LIBS) $(ALL_BATCH_CMO) - -#Profiling version of toplevel.byte using ocamlprof -bin/toplevel.prof$(EXE): $(ALL_BATCH_CMO) $(GEN_BYTE_LIBS) \ - $(PLUGIN_DYN_CMO_LIST) - $(PRINT_OCAMLCP) $@ - $(OCAMLCP) $(BLINKFLAGS) -o $@ $(BYTE_LIBS) $(ALL_BATCH_CMO) - -bin/toplevel.opt$(EXE): $(ALL_BATCH_CMX) $(GEN_OPT_LIBS) \ - $(PLUGIN_DYN_CMX_LIST) - $(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_BYTE_LIBS) lib/fc/META.frama-c - $(PRINT_LINKING) $@ - $(MKDIR) $(FRAMAC_LIB) - $(OCAMLMKLIB) -o lib/fc/frama-c $(BYTE_LIBS) $(LIB_KERNEL_CMO) - -lib/fc/frama-c.cmxa: lib/fc/frama-c.cma $(GEN_OPT_LIBS) $(LIB_KERNEL_CMX) - $(MKDIR) $(FRAMAC_LIB) - $(PRINT_LINKING) $@ - $(OCAMLMKLIB) -o lib/fc/frama-c $(OPT_LIBS) $(LIB_KERNEL_CMX) - -#################### -# (Ocaml) Toplevel # -#################### - -bin/toplevel.top$(EXE): $(filter-out src/kernel_internals/runtime/boot.ml,$(ALL_BATCH_CMO)) \ - src/kernel_internals/runtime/toplevel_config.cmo \ - $(GEN_BYTE_LIBS) $(PLUGIN_DYN_CMO_LIST) - $(PRINT_OCAMLMKTOP) $@ - $(OCAMLMKTOP) $(BFLAGS) -warn-error -31 -custom -o $@ \ - -linkpkg $(BYTE_LIBS) $(ALL_BATCH_CMO) \ - src/kernel_internals/runtime/toplevel_config.cmo - -####### -# GUI # -####### - -ifneq ($(ENABLE_GUI),no) - -SINGLE_GUI_CMI = $(SINGLE_GUI_CMO:.cmo=.cmi) -SINGLE_GUI_CMX = $(SINGLE_GUI_CMO:.cmo=.cmx) - -GUICMO += $(SINGLE_GUI_CMO) $(PLUGIN_GUI_CMO_LIST) - -MODULES_TODOC+= $(filter-out src/plugins/gui/book_manager.mli,\ - $(SINGLE_GUI_CMO:.cmo=.mli)) - -GUICMI = $(GUICMO:.cmo=.cmi) -GUICMX = $(SINGLE_GUI_CMX) $(PLUGIN_GUI_CMX_LIST) - -$(GUICMI) $(GUICMO) bin/viewer.byte$(EXE): BFLAGS+= $(GUI_INCLUDES) -$(GUICMX) bin/viewer.opt$(EXE): OFLAGS+= $(GUI_INCLUDES) - -$(PLUGIN_DYN_DEP_GUI_CMO_LIST): BFLAGS+= $(GUI_INCLUDES) -$(PLUGIN_DYN_DEP_GUI_CMX_LIST): OFLAGS+= $(GUI_INCLUDES) - -.PHONY:gui - -gui-byte:: bin/viewer.byte$(EXE) share/Makefile.dynamic_config \ - $(PLUGIN_META_LIST) - -gui-opt:: gui-byte bin/viewer.opt$(EXE) - -gui: gui-$(OCAMLBEST) - -ALL_GUI_CMO= $(ALL_CMO) $(GRAPH_GUICMO) $(GUICMO) -ALL_GUI_CMX= $(patsubst %.cma,%.cmxa,$(ALL_GUI_CMO:.cmo=.cmx)) - -bin/viewer.byte$(EXE): BYTE_LIBS+= $(GRAPH_GUICMO) -bin/viewer.byte$(EXE): $(filter-out $(GRAPH_GUICMO),$(ALL_GUI_CMO)) \ - $(GEN_BYTE_LIBS) \ - $(PLUGIN_DYN_CMO_LIST) $(PLUGIN_DYN_GUI_CMO_LIST) - $(PRINT_LINKING) $@ - $(OCAMLC) $(BLINKFLAGS) $(THREAD) -o $@ $(BYTE_LIBS) \ - $(CMO) \ - $(filter-out \ - $(patsubst $(PLUGIN_GUI_LIB_DIR)/%,$(PLUGIN_LIB_DIR)/%,\ - $(PLUGIN_GUI_CMO_LIST)),\ - $(PLUGIN_CMO_LIST)) \ - $(GUICMO) $(STARTUP_CMO) - -bin/viewer.opt$(EXE): OPT_LIBS+= $(GRAPH_GUICMX) -bin/viewer.opt$(EXE): $(filter-out $(GRAPH_GUICMX),$(ALL_GUI_CMX)) \ - $(GEN_OPT_LIBS) \ - $(PLUGIN_DYN_CMX_LIST) $(PLUGIN_DYN_GUI_CMX_LIST) \ - $(PLUGIN_CMX_LIST) $(PLUGIN_GUI_CMX_LIST) - $(PRINT_LINKING) $@ - $(OCAMLOPT) $(OLINKFLAGS) $(THREAD) -o $@ $(OPT_LIBS) \ - $(CMX) \ - $(filter-out \ - $(patsubst $(PLUGIN_GUI_LIB_DIR)/%,$(PLUGIN_LIB_DIR)/%,\ - $(PLUGIN_GUI_CMX_LIST)),\ - $(PLUGIN_CMX_LIST)) \ - $(GUICMX) $(STARTUP_CMX) -endif - -##################### -# Config Ocaml File # -##################### +.PHONY: all -CONFIG_DIR=src/kernel_internals/runtime -CONFIG_FILE=$(CONFIG_DIR)/fc_config.ml -CONFIG_CMO=$(CONFIG_DIR)/fc_config.cmo -GENERATED +=$(CONFIG_FILE) -#Generated in Makefile.generating - -empty:= -space:=$(empty) $(empty) - -ifeq ($(ENABLE_GUI),no) -CONFIG_CMO=$(ALL_CMO) -CONFIG_PLUGIN_CMO=$(PLUGIN_CMO_LIST) -else -CONFIG_CMO=$(ALL_GUI_CMO) -CONFIG_PLUGIN_CMO=$(PLUGIN_GUI_CMO_LIST) -endif +all: config.sed + dune build ifeq ($(HAS_DOT),yes) OPTDOT=Some \"$(DOT)\" @@ -1353,826 +51,93 @@ else OPTDOT=None endif -COMPILATION_UNITS=\ - $(foreach p,$(CONFIG_CMO),\"$(notdir $(patsubst %.cmo,%,$p))\"; ) - -################### -# Generating part # -################### -# It is in another file in order to have a dependency only on Makefile.generating. -# It must be before `.depend` definition because it modifies $GENERATED. - -include Makefile.generating - -######### -# Tests # -######### - -ifeq ($(OCAMLBEST),opt) -PTESTS_FILES=ptests_config.cmi ptests_config.cmx ptests_config.o -else -PTESTS_FILES=ptests_config.cmi ptests_config.cmo -endif - -.PHONY: tests oracles btests tests_dist libc_tests plugins_ptests_config external_tests \ - update_external_tests - -tests:: byte opt ptests - $(PRINT_EXEC) ptests - time -p $(PTESTS) $(PTESTS_OPTS) $(FRAMAC_PARALLEL) \ - -make "$(MAKE)" $(PLUGIN_TESTS_LIST) - -external_tests: byte opt ptests -tests:: external_tests - -update_external_tests: PTESTS_OPTS="-update" -update_external_tests: external_tests - -oracles: byte opt ptests - $(PRINT_MAKING) oracles - ./bin/ptests.$(OCAMLBEST)$(EXE) -make "$(MAKE)" $(PLUGIN_TESTS_LIST) \ - > /dev/null 2>&1 - ./bin/ptests.$(OCAMLBEST)$(EXE) -make "$(MAKE)" -update \ - $(PLUGIN_TESTS_LIST) - -btests: byte ./bin/ptests.byte$(EXE) - $(PRINT_EXEC) ptests -byte - time -p ./bin/ptests.byte$(EXE) -make "$(MAKE)" -byte \ - $(PLUGIN_TESTS_LIST) - -tests_dist: dist ptests - $(PRINT_EXEC) ptests - time -p ./bin/ptests.$(OCAMLBEST)$(EXE) -make "$(MAKE)" \ - $(PLUGIN_TESTS_LIST) - -# test only one test suite : make suite_tests -%_tests: opt ptests - $(PRINT_EXEC) ptests - ./bin/ptests.$(OCAMLBEST)$(EXE) -make "$(MAKE)" $($*_TESTS_OPTS) $* - -# full test suite -wp_TESTS_OPTS=-j 1 -fulltests: tests wp_tests - -acsl_tests: byte - $(PRINT_EXEC) acsl_tests - find doc/speclang -name \*.c -exec ./bin/toplevel.byte$(EXE) {} \; > /dev/null - -LONELY_TESTS_DIR:=$(wildcard $(TEST_DIRS_AS_PLUGIN:%=tests/%)) -ifeq ($(strip $(LONELY_TESTS_DIR)),) - LONELY_TESTS_ML_FILES:= -else - LONELY_TESTS_ML_FILES:=\ - $(sort $(shell find $(TEST_DIRS_AS_PLUGIN:%=tests/%) -not -path '*/\.*' -name '*.ml')) -endif -$(foreach file,$(LONELY_TESTS_ML_FILES),\ - $(eval $(file:%.ml=%.cmo): BFLAGS+=-I $(dir $(file)))) -$(foreach file,$(LONELY_TESTS_ML_FILES),\ - $(eval $(file:%.ml=%.cmx): OFLAGS+=-I $(dir $(file)))) -$(foreach file,$(LONELY_TESTS_ML_FILES),\ - $(eval $(file:%.ml=%.cmxs): OFLAGS+=-I $(dir $(file)))) -.PRECIOUS: $(LONELY_TESTS_ML_FILES:%.ml=%.cmx) \ - $(LONELY_TESTS_ML_FILES:%.ml=%.cmxs) \ - $(LONELY_TESTS_ML_FILES:%.ml=%.cmo) \ - $(LONELY_TESTS_ML_FILES:%.ml=%.cmi) - -bin/ocamldep_transitive_closure: devel_tools/ocamldep_transitive_closure.ml - $(OCAMLOPT) -package ocamlgraph -package str -linkpkg -o $@ $< - -tests/crowbar/.%.depend: tests/crowbar/%.ml - $(OCAMLDEP) $(INCLUDES) $< > $@ - -tests/crowbar/%: tests/crowbar/%.ml tests/crowbar/.%.depend .depend \ - bin/ocamldep_transitive_closure bin/toplevel.opt - $(OCAMLOPT) $(OLINKFLAGS) -w -42 -package crowbar -o $@ \ - $(GEN_C_BINDINGS) \ - $$(bin/ocamldep_transitive_closure -root tests/crowbar/$*.cmx \ - -deps tests/crowbar/.$*.depend -deps .depend) \ - $< - -tests/crowbar/full-link-%: tests/crowbar/%.ml lib/fc/frama-c.cmxa - $(OCAMLOPT) $(OLINKFLAGS) -ccopt "-Llib/fc" -w -42 -package crowbar -o $@ \ - lib/fc/frama-c.cmxa $< - -crowbar-%: tests/crowbar/% - $< - -crowbar-afl-%: tests/crowbar/% - $(MKDIR) tests/crowbar/output-$* - afl-fuzz $(AFL_OPTS) -i tests/crowbar/input -o tests/crowbar/output-$* $< @@ - -crowbar-afl-check-%: tests/crowbar/% - $(foreach file,$(wildcard tests/crowbar/output-$*/crashes/id*), \ - $< $(file) >/dev/null 2>&1 || \ - echo "$(file) leads to a real test failure";) - -############## -# Emacs tags # -############## - -.PHONY: tags -# otags gives a better tagging of ocaml files than etags -ifdef OTAGS -tags: - $(OTAGS) -r src lib -vtags: - $(OTAGS) -vi -r src lib -else -tags: - find . -name "*.ml[ily]" -o -name "*.ml" | sort -r | xargs \ - etags "--regex=/[ \t]*let[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/[ \t]*let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/[ \t]*and[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/[ \t]*type[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/[ \t]*exception[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/[ \t]*val[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/[ \t]*module[ \t]+\([^ \t]+\)/\1/" -endif - -################# -# Documentation # -################# - -.PHONY: doc doc-distrib - -# private targets, useful for recompiling the doc without dependencies -# (too long!) -.PHONY: doc-kernel doc-index plugins-doc doc-update doc-tgz - -DOC_DEPEND=$(MODULES_TODOC) byte $(DOC_PLUGIN) -ifneq ($(ENABLE_GUI),no) -DOC_DEPEND+=bin/viewer.byte$(EXE) -endif - -$(DOC_DIR)/docgen.cmo: $(DOC_DIR)/docgen.ml - $(PRINT_OCAMLC) $@ - $(OCAMLC) -c -I +ocamldoc -I +compiler-libs -I $(CONFIG_DIR) $(DOC_DIR)/docgen.ml - -$(DOC_DIR)/docgen.cmxs: $(DOC_DIR)/docgen.ml - $(PRINT_PACKING) $@ - $(OCAMLOPT) -o $@ -shared -I +ocamldoc -I +compiler-libs -I $(CONFIG_DIR) \ - $(DOC_DIR)/docgen.ml - -clean-doc:: - $(PRINT_RM) "documentation generator" - $(RM) $(DOC_DIR)/docgen.cm* - -DOC_NOT_FOR_DISTRIB=yes -plugins-doc: - $(QUIET_MAKE) \ - $(if $(DOC_NOT_FOR_DISTRIB),$(PLUGIN_DOC_LIST),\ - $(filter \ - $(addsuffix _DOC,$(PLUGIN_DISTRIBUTED_NAME_LIST)),\ - $(PLUGIN_DOC_LIST))) - -.PHONY: server-doc-md server-doc-html server-doc - -server-doc-md: byte - $(PRINT) 'Generating Markdown server documentation' - @rm -fr doc/server - @mkdir -p doc/server - ./bin/frama-c.byte -server-doc doc/server - -server-doc-html: server-doc-md - $(PRINT) 'Generating HTML server documentation' - @find doc/server -name "*.md" -print -exec pandoc \ - --standalone --toc --toc-depth=2 --to html \ - --template doc/pandoc/template.html \ - --metadata-file {}.json \ - --lua-filter doc/pandoc/href.lua \ - {} -o {}.html \; - @cp -f doc/pandoc/style.css doc/server/ - $(PRINT) 'HTML server documentation ready:' - $(PRINT) ' open doc/server/readme.md.html' - -server-doc: server-doc-html - -# to make the documentation for one plugin only, -# the name of the plugin should begin with a capital letter : -# Example for the pdg doc : make Pdg_DOC -# While working on the documentation of a plugin, it can also be useful -# to use : make -o doc/code/kernel-doc.ocamldoc Plugin_DOC -# to avoid redoing the global documentation each time. - -STDLIB_FILES:=\ - array \ - buffer \ - bytes \ - char \ - format \ - hashtbl \ - int64 \ - list \ - map \ - marshal \ - obj \ - parsing \ - printf \ - queue \ - scanf \ - set \ - stack \ - string \ - sys \ - weak \ - ephemeron - -STDLIB_FILES:=$(patsubst %,$(OCAMLLIB)/%.mli,$(STDLIB_FILES)) - -.PHONY: doc-kernel -doc-kernel: $(DOC_DIR)/kernel-doc.ocamldoc - -$(DOC_DIR)/kernel-doc.ocamldoc: $(DOC_DEPEND) - $(PRINT_DOC) Kernel Documentation - $(MKDIR) $(DOC_DIR)/html - $(RM) $(DOC_DIR)/html/*.html - $(OCAMLDOC) $(DOC_FLAGS) \ - $(addprefix -passopt -stdlib ,$(STDLIB_FILES)) \ - -t "Frama-C Kernel" \ - -sort -css-style ../style.css \ - -g $(DOC_PLUGIN) \ - -d $(DOC_DIR)/html -dump $@ \ - $(MODULES_TODOC); \ - RES=$$?; \ - if test $$RES -ne 0; then \ - $(RM) $@; \ - exit $$RES; \ - fi - -DYN_MLI_DIR := src/plugins/print_api - -.PHONY: doc-dynamic -doc-dynamic: doc-kernel - $(RM) $(DYN_MLI_DIR)/dynamic_plugins.mli - ./bin/frama-c.byte \ - -print_api $(call winpath,$(FRAMAC_ROOT_SRCDIR)/$(DYN_MLI_DIR)) - $(PRINT_DOC) Dynamically registered plugins Documentation - $(MKDIR) $(DOC_DIR)/dynamic_plugins - $(RM) $(DOC_DIR)/dynamic_plugins/*.html - $(OCAMLDOC) $(DOC_FLAGS) -I $(FRAMAC_LIB) -I $(OCAMLLIB) \ - -passopt -docpath $(DOC_DIR)/html \ - -sort -css-style ../style.css \ - -load $(DOC_DIR)/kernel-doc.ocamldoc \ - -t " Dynamically registered plugins" \ - -g $(DOC_PLUGIN) \ - -d $(DOC_DIR)/dynamic_plugins \ - $(DYN_MLI_DIR)/dynamic_plugins.mli - $(ECHO) '<li><a href="dynamic_plugins/Dynamic_plugins.html">Dynamically registered plugins</a </li>' > $(DOC_DIR)/dynamic_plugins.toc - -doc-index: doc-kernel doc-dynamic plugins-doc - $(PRINT_MAKING) doc/code/index.html - $(CAT) $(DOC_DIR)/toc_head.htm $(DOC_DIR)/*.toc \ - $(DOC_DIR)/toc_tail.htm > $(DOC_DIR)/index.html - -doc-update: doc-kernel doc-dynamic plugins-doc doc-index - -doc:: doc-kernel doc-dynamic plugins-doc doc-index - -doc-kernel doc-dynamic plugins-doc doc-index: $(DOC_DEPEND) - -doc-tgz: - $(PRINT_MAKING) frama-c-api.tar.gz - cd $(DOC_DIR); \ - $(TAR) zcf tmp.tgz index.html *.txt \ - $(notdir $(wildcard $(DOC_DIR)/*.css $(DOC_DIR)/*.png \ - $(DOC_DIR)/dynamic_plugins*)) \ - html \ - $(foreach p,$(PLUGIN_DISTRIBUTED_NAME_LIST),\ - $(notdir $($(p)_DOC_DIR))) - $(MKDIR) frama-c-api - $(RM) -r frama-c-api/* - cd frama-c-api; $(TAR) zxf ../$(DOC_DIR)/tmp.tgz - $(TAR) zcf frama-c-api.tar.gz frama-c-api - $(RM) -r frama-c-api $(DOC_DIR)/tmp.tgz - -doc-distrib: - $(QUIET_MAKE) clean-doc - $(QUIET_MAKE) doc DOC_NOT_FOR_DISTRIB= - $(QUIET_MAKE) doc-tgz - -#find src -name "*.ml[i]" -o -name "*.ml" -maxdepth 3 | sort -r | xargs -dots: $(ALL_CMO) - $(PRINT_DOC) callgraph - $(OCAMLDOC) $(DOC_FLAGS) $(INCLUDES) -o doc/call_graph.dot \ - -dot -dot-include-all -dot-reduce $(MODULES_TODOC) - $(QUIET_MAKE) doc/call_graph.svg - $(QUIET_MAKE) doc/call_graph.ps - -# pandoc is required to regenerate the manpage -man/frama-c.1: man/frama-c.1.header man/frama-c.1.md - $(PRINT) 'generating $@' - $(RM) $@ - pandoc -s -t man -H $^ | tail -n +5 > man/frama-c.1 - $(CHMOD_RO) $@ - -# Checking consistency with the current implementation -###################################################### - -DOC_DEV_DIR = doc/developer -CHECK_API_DIR=$(DOC_DEV_DIR)/check_api - -$(CHECK_API_DIR)/check_code.cmo: $(CHECK_API_DIR)/check_code.ml - $(PRINT_OCAMLC) $@ - $(OCAMLC) -c -I +ocamldoc str.cma $(CHECK_API_DIR)/check_code.ml - -$(CHECK_API_DIR)/check_code.cmxs: $(CHECK_API_DIR)/check_code.ml - $(PRINT_PACKING) $@ - $(OCAMLOPT) -o $@ -shared -I +ocamldoc \ - str.cmxa $(CHECK_API_DIR)/check_code.ml - -CHECK_CODE=$(CHECK_API_DIR)/check_code.cmxs - -.PHONY: check-devguide -check-devguide: $(CHECK_CODE) $(DOC_DEPEND) $(DOC_DIR)/kernel-doc.ocamldoc - $(PRINT) 'Checking developer guide consistency' - $(MKDIR) $(CHECK_API_DIR)/html - $(OCAMLDOC) $(DOC_FLAGS) -I $(OCAMLLIB) \ - -g $(CHECK_CODE) \ - -passopt -docdevpath -passopt "`pwd`/$(CHECK_API_DIR)" \ - -load $(DOC_DIR)/kernel-doc.ocamldoc \ - -d $(CHECK_API_DIR)/html - $(RM) -r $(CHECK_API_DIR)/html - $(MAKE) --silent -C $(CHECK_API_DIR) main.idx - $(MAKE) --silent -C $(CHECK_API_DIR) >$(CHECK_API_DIR)/summary.txt - $(ECHO) see all the information displayed here \ - in $(CHECK_API_DIR)/summary.txt - $(RM) code_file -################################ -# Code prettyfication and lint # -################################ - -# We're interested by any .ml[i]? file in src, except for scripts in test -# directories, and generated files (in particular lexers and parsers) -# Note: the find command below is *very* ugly, but it should be POSIX-compliant. - -ALL_ML_FILES:=$(shell find src -name '*.ml' -print -o -name '*.mli' -print -o -path '*/tests' -prune '!' -name '*') -ALL_ML_FILES+=ptests/ptests.ml -MANUAL_ML_FILES:=$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST), $(ALL_ML_FILES)) - -# Allow control of files to be linted/fixed by external sources -# (e.g. pre-commit hook that will concentrate on files which have changed) - -sinclude .Makefile.lint - -HAS_GIT_FILE:=$(wildcard .git/HEAD) - -ifeq ("$(HAS_GIT_FILE)","") -LINT_OTHER_SOURCES:= -else -LINT_OTHER_SOURCES:=\ - $(filter-out \ - $(shell git ls-tree --name-only HEAD src/plugins/*), \ - $(wildcard src/plugins/*)) -endif - -$(foreach dir,$(LINT_OTHER_SOURCES),$(eval sinclude $(dir)/.Makefile.lint)) - -ML_LINT_MISSING:=$(filter-out $(MANUAL_ML_FILES), $(ML_LINT_KO)) - -# By default, also checks files with unknown status: -# this requires new files to pass lint checker from the beginning - -ML_LINT_CHECK?=$(filter-out $(ML_LINT_KO), $(MANUAL_ML_FILES)) - -# this NEWLINE variable containing a literal newline character is used to avoid -# the error "argument list too long", in some instances of "foreach". -# For details, see https://stackoverflow.com/questions/7039811 -define NEWLINE - - -endef - -# pre-requisite intentionally left blank: this target should only be used -# if the file is not present to generate it once and forall, -# and be edited manually afterwards -# double colon here tells make not to attempt updating the .Makefile.lint -# if it does not exist, but just to ignore it. -.Makefile.lint:: - echo "ML_LINT_KO:=" >> $@ - $(foreach file,$(sort $(MANUAL_ML_FILES)), \ - if ! $(MAKE) ML_LINT_CHECK=$(file) lint; \ - then echo "ML_LINT_KO+=$(file)" >> $@; fi;$(NEWLINE) ) - -$(foreach dir,$(LINT_OTHER_SOURCES),\ - $(eval $(dir)/.Makefile.lint:: ; \ - $(foreach file, $(sort $(filter $(dir)/%, $(MANUAL_ML_FILES))), \ - if ! $$(MAKE) ML_LINT_CHECK=$(file) lint; \ - then echo "ML_LINT_KO+=$(file)" >> $$@; fi; ))) - -.PHONY: stats-lint -stats-lint: - echo \ - "scale = 2; bad = $(words $(ML_LINT_MISSING)); \ - all = $(words $(sort $(MANUAL_ML_FILES))); \ - fail = $(words $(ML_LINT_KO)); \ - \"lint coverage: \"; \ - ((all - fail) * 100) / all; " | bc - echo "number of files supposed to pass lint: $(words $(ML_LINT_CHECK))" - echo "number of files supposed to fail lint: $(words $(ML_LINT_KO))" -ifneq ($(strip $(ML_LINT_MISSING)),) - echo "number of files missing from src/ : $(words $(ML_LINT_MISSING))" - $(foreach file, $(ML_LINT_MISSING), echo $(file);) - exit 1 -endif - -INDENT_TARGET= $(patsubst %,%.indent,$(ML_LINT_CHECK)) - -LINT_TARGET= $(patsubst %,%.lint,$(ML_LINT_CHECK)) - -FIX_SYNTAX_TARGET=$(patsubst %,%.fix-syntax,$(ML_LINT_CHECK)) - -.PHONY: $(INDENT_TARGET) $(LINT_TARGET) $(FIX_SYNTAX_TARGET) \ - indent lint fix-syntax - -indent: $(INDENT_TARGET) - -lint: $(LINT_TARGET) - -check-ocp-indent-version: - if command -v ocp-indent >/dev/null; then \ - if [ -z "$(shell ocp-indent --version)" ]; then echo "warning: ocp-indent returned an empty string, assuming it is the correct version"; \ - else \ - $(eval ocp_version_major := $(shell ocp-indent --version | $(SED) -E "s/^([0-9]+)\.[0-9]+\..*/\1/")) \ - $(eval ocp_version_minor := $(shell ocp-indent --version | $(SED) -E "s/^[0-9]+\.([0-9]+)\..*/\1/")) \ - if [ "$(ocp_version_major)" -lt 1 -o "$(ocp_version_minor)" -lt 7 ]; then \ - echo "error: ocp-indent 1.7.0 required for linting (got $(ocp_version_major).$(ocp_version_minor))"; \ - exit 1; \ - fi; \ - fi; \ - else \ - exit 1; \ - fi; - -fix-syntax: $(FIX_SYNTAX_TARGET) - -$(INDENT_TARGET): %.indent: % check-ocp-indent-version - ocp-indent -i $< - -$(LINT_TARGET): %.lint: % check-ocp-indent-version - # See SO 1825552 on mixing grep and \t (and cry) - # For OK_NL, we have three cases: - # - for empty files, the computation boils down to 0 - 0 == 0 - # - for non-empty files with a proper \n at the end, to 1 - 1 == 0 - # - for empty files without \n, to 1 - 0 == 1 that will be catched - OK_TAB=$$(grep -c -e "$$(printf '^ *\t')" $<) ; \ - OK_SPACE=$$(grep -c -e '[[:blank:]]$$' $<) ; \ - OK_NL=$$(($$(tail -c -1 $< | wc -c) - $$(tail -n -1 $< | wc -l))) ; \ - OK_EMPTY=$$(tail -n -1 $< | grep -c -e '^[[:blank:]]*$$') ; \ - ERROR=$$(($$OK_TAB + $$OK_SPACE + $$OK_NL + $$OK_EMPTY)) ; \ - if test $$ERROR -gt 0; then \ - echo "File $< does not pass syntactic checks:"; \ - echo "$$OK_TAB lines indented with tabulation instead of spaces"; \ - echo "$$OK_SPACE lines with spaces at end of line"; \ - test $$OK_NL -eq 0 || echo "No newline at end of file"; \ - test $$OK_EMPTY -eq 0 || echo "Empty line(s) at end of file"; \ - echo "Please run make ML_LINT_CHECK=$< fix-syntax"; \ - exit 1 ; \ - fi - ocp-indent $< > $<.tmp; - if cmp -s $< $<.tmp; \ - then rm -f $<.tmp; \ - else \ - echo "File $< is not indented correctly."; \ - echo "Please run make ML_LINT_CHECK=$< indent";\ - rm $<.tmp; \ - exit 1; \ - fi - -$(FIX_SYNTAX_TARGET): %.fix-syntax: % - $(ISED) -e 's/^ *\t\+/ /' $< - $(ISED) -e 's/\(.*[^[:blank:]]\)[[:blank:]]\+$$/\1/' $< - $(ISED) -e 's/^[ \t]\+$$//' $< - if test \( $$(tail -n -1 $< | wc -l) -eq 0 \) -a \( $$(wc -c $< | cut -d " " -f 1) -gt 0 \) ; then \ - echo "" >> $<; \ - else \ - while tail -n -1 $< | grep -l -e '^[ \t]*$$'; do \ - head -n -1 $< > $<.tmp; \ - mv $<.tmp $<; \ - done; \ - fi - -# Avoid a UTF-8 locale at all cost: in such setting, sed does not work -# reliably if you happen to have latin-1 encoding somewhere, -# which is still unfortunately the case in some dark corners of the platform -%.fix-syntax: LC_ALL = C - -################ -# Installation # -################ - -# line below does not work if INCLUDES contains twice the same directory -# Do not attempt to copy gui interfaces if gui is disabled -#Byte -ALL_BATCH_CMO_FIXED=$(filter-out src/kernel_internals/runtime/gui_init.cmo,$(CMO) $(STARTUP_CMO)) -LIB_BYTE_TO_INSTALL=\ - $(MLI_ONLY:.mli=.cmi) \ - $(ALL_BATCH_CMO_FIXED:.cmo=.cmi) \ - $(ALL_BATCH_CMO_FIXED) \ - $(filter-out %.o,$(GEN_BYTE_LIBS:.cmo=.cmi)) \ - $(GEN_BYTE_LIBS) - -#Byte GUI -ifneq ("$(ENABLE_GUI)","no") -LIB_BYTE_TO_INSTALL+=$(SINGLE_GUI_CMI) $(SINGLE_GUI_CMO) -endif - -#Opt -ifeq ("$(OCAMLBEST)","opt") -ALL_BATCH_CMX_FIXED= $(filter-out src/kernel_internals/runtime/gui_init.cmx,\ - $(CMX) $(STARTUP_CMX)) -LIB_OPT_TO_INSTALL +=\ - $(ALL_BATCH_CMX) \ - $(filter %.a,$(ALL_BATCH_CMX_FIXED:.cmxa=.a)) \ - $(filter %.o,$(ALL_BATCH_CMX_FIXED:.cmx=.o)) \ - $(filter-out %.o,$(GEN_OPT_LIBS)) \ - $(filter-out $(GEN_BYTE_LIBS),$(filter %.o,$(GEN_OPT_LIBS:.cmx=.o))) - -#Opt GUI -ifneq ("$(ENABLE_GUI)","no") -LIB_OPT_TO_INSTALL += $(SINGLE_GUI_CMX) $(SINGLE_GUI_CMX:.cmx=.o) -endif - -endif - -clean-install: - $(PRINT_RM) "Installation directory" - $(RM) -r $(FRAMAC_LIBDIR) - -install-lib-byte: clean-install - $(PRINT_INSTALL) kernel API - $(MKDIR) $(FRAMAC_LIBDIR) - $(CP) $(LIB_BYTE_TO_INSTALL) $(FRAMAC_LIBDIR) - $(CP) $(addprefix lib/fc/,dllframa-c$(DLLEXT) libframa-c.a frama-c.cma META.frama-c) $(FRAMAC_LIBDIR) - -install-lib-opt: install-lib-byte - $(CP) $(LIB_OPT_TO_INSTALL) $(FRAMAC_LIBDIR) - $(CP) $(addprefix lib/fc/,frama-c.a frama-c.cmxa) $(FRAMAC_LIBDIR) - -install-doc-code: - $(PRINT_INSTALL) API documentation - $(MKDIR) $(FRAMAC_DATADIR)/doc/code - (cd doc ; tar cf - --exclude='.svn' --exclude='*.toc' \ - --exclude='*.htm' --exclude='*.txt' \ - --exclude='*.ml' \ - code \ - | (cd $(FRAMAC_DATADIR)/doc ; tar xf -)) - -.PHONY: install -install:: install-lib-$(OCAMLBEST) - $(PRINT_MAKING) destination directories - $(MKDIR) $(BINDIR) - $(MKDIR) $(MANDIR)/man1 - $(MKDIR) $(FRAMAC_PLUGINDIR)/top - $(MKDIR) $(FRAMAC_PLUGINDIR)/gui - $(MKDIR) $(FRAMAC_DATADIR)/theme/default - $(MKDIR) $(FRAMAC_DATADIR)/theme/colorblind - $(MKDIR) $(FRAMAC_DATADIR)/theme/flat - $(MKDIR) $(FRAMAC_DATADIR)/libc/sys - $(MKDIR) $(FRAMAC_DATADIR)/libc/netinet - $(MKDIR) $(FRAMAC_DATADIR)/libc/net - $(MKDIR) $(FRAMAC_DATADIR)/libc/arpa - $(PRINT_INSTALL) shared files - $(CP) \ - $(wildcard share/*.c share/*.h) \ - share/Makefile.dynamic share/Makefile.plugin.template \ - share/Makefile.config share/Makefile.common share/Makefile.generic \ - share/configure.ac share/autocomplete_frama-c share/_frama-c \ - $(FRAMAC_DATADIR) - $(MKDIR) $(FRAMAC_DATADIR)/analysis-scripts - $(CP) \ - share/analysis-scripts/analysis.mk \ - share/analysis-scripts/benchmark_database.py \ - share/analysis-scripts/cmd-dep.sh \ - share/analysis-scripts/concat-csv.sh \ - share/analysis-scripts/clone.sh \ - share/analysis-scripts/creduce.sh \ - share/analysis-scripts/epilogue.mk \ - share/analysis-scripts/fc_stubs.c \ - share/analysis-scripts/find_fun.py \ - share/analysis-scripts/flamegraph.pl \ - share/analysis-scripts/frama_c_results.py \ - share/analysis-scripts/function_finder.py \ - share/analysis-scripts/git_utils.py \ - share/analysis-scripts/list_files.py \ - share/analysis-scripts/make_template.py \ - share/analysis-scripts/make_wrapper.py \ - share/analysis-scripts/parse-coverage.sh \ - share/analysis-scripts/prologue.mk \ - share/analysis-scripts/README.md \ - share/analysis-scripts/results_display.py \ - share/analysis-scripts/summary.py \ - share/analysis-scripts/template.mk \ - $(FRAMAC_DATADIR)/analysis-scripts - $(MKDIR) $(FRAMAC_DATADIR)/compliance - $(CP) share/compliance/c11_functions.json \ - share/compliance/glibc_functions.json \ - share/compliance/nonstandard_identifiers.json \ - share/compliance/posix_identifiers.json \ - $(FRAMAC_DATADIR)/compliance - $(MKDIR) $(FRAMAC_DATADIR)/emacs - $(CP) $(wildcard share/emacs/*.el) $(FRAMAC_DATADIR)/emacs - $(CP) share/frama-c.rc $(ICONS) $(FRAMAC_DATADIR) - $(CP) $(THEME_ICONS_DEFAULT) $(FRAMAC_DATADIR)/theme/default - $(CP) $(THEME_ICONS_COLORBLIND) $(FRAMAC_DATADIR)/theme/colorblind - $(CP) $(THEME_ICONS_FLAT) $(FRAMAC_DATADIR)/theme/flat - if [ -d $(EMACS_DATADIR) ]; then \ - $(CP) $(wildcard share/emacs/*.el) $(EMACS_DATADIR); \ - fi - $(CP) share/Makefile.dynamic_config.external \ - $(FRAMAC_DATADIR)/Makefile.dynamic_config - $(PRINT_INSTALL) C standard library - $(CP) $(wildcard share/libc/*.c share/libc/*.i share/libc/*.h) \ - $(FRAMAC_DATADIR)/libc - $(CP) share/libc/sys/*.[ch] $(FRAMAC_DATADIR)/libc/sys - $(CP) share/libc/arpa/*.[ch] $(FRAMAC_DATADIR)/libc/arpa - $(CP) share/libc/net/*.[ch] $(FRAMAC_DATADIR)/libc/net - $(CP) share/libc/netinet/*.[ch] $(FRAMAC_DATADIR)/libc/netinet - $(PRINT_INSTALL) binaries - $(CP) bin/toplevel.$(OCAMLBEST) $(BINDIR)/frama-c$(EXE) - $(CP) bin/toplevel.byte$(EXE) $(BINDIR)/frama-c.byte$(EXE) - if [ -x bin/toplevel.top ] ; then \ - $(CP) bin/toplevel.top $(BINDIR)/frama-c.toplevel$(EXE); \ - fi - if [ -x bin/viewer.$(OCAMLBEST) ] ; then \ - $(CP) bin/viewer.$(OCAMLBEST) $(BINDIR)/frama-c-gui$(EXE);\ - fi - if [ -x bin/viewer.byte$(EXE) ] ; then \ - $(CP) bin/viewer.byte$(EXE) $(BINDIR)/frama-c-gui.byte$(EXE); \ - fi - $(CP) bin/ptests.$(OCAMLBEST)$(EXE) \ - $(BINDIR)/ptests.$(OCAMLBEST)$(EXE) - if [ -x bin/fc-config$(EXE) ] ; then \ - $(CP) bin/fc-config$(EXE) $(BINDIR)/frama-c-config$(EXE); \ - fi - if [ -x bin/frama-c-script ] ; then \ - $(CP) bin/frama-c-script $(BINDIR)/frama-c-script; \ - fi - $(PRINT_INSTALL) config files - $(CP) $(addprefix ptests/,$(PTESTS_FILES)) $(FRAMAC_LIBDIR) - $(PRINT_INSTALL) API documentation - $(MKDIR) $(FRAMAC_DATADIR)/doc/code - $(CP) $(wildcard $(DOC_GEN_FILES)) $(FRAMAC_DATADIR)/doc/code - $(PRINT_INSTALL) plug-ins - if [ -d "$(FRAMAC_PLUGIN)" ]; then \ - $(CP) $(PLUGIN_DYN_CMI_LIST) $(PLUGIN_META_LIST) \ - $(FRAMAC_PLUGINDIR); \ - $(CP) $(PLUGIN_DYN_CMO_LIST) $(FRAMAC_PLUGINDIR)/top; \ - if [ "$(OCAMLBEST)" = "opt" ]; then \ - $(CP) $(PLUGIN_DYN_CMX_LIST) $(FRAMAC_PLUGINDIR)/top; \ - fi; \ - fi - $(PRINT_INSTALL) gui plug-ins - if [ -d "$(FRAMAC_PLUGIN_GUI)" -a "$(PLUGIN_DYN_GUI_EXISTS)" = "yes" ]; \ - then \ - $(CP) $(patsubst %.cma,%.cmi,$(PLUGIN_DYN_GUI_CMO_LIST:.cmo=.cmi)) \ - $(PLUGIN_DYN_GUI_CMO_LIST) $(FRAMAC_PLUGINDIR)/gui; \ - if [ "$(OCAMLBEST)" = "opt" ]; then \ - $(CP) $(PLUGIN_DYN_GUI_CMX_LIST) $(FRAMAC_PLUGINDIR)/gui; \ - fi; \ - fi - $(PRINT_INSTALL) man pages - $(CP) man/frama-c.1 $(MANDIR)/man1/frama-c.1 - $(CP) man/frama-c.1 $(MANDIR)/man1/frama-c-gui.1 - -.PHONY: uninstall -uninstall:: - $(PRINT_RM) installed binaries - $(RM) $(BINDIR)/frama-c* $(BINDIR)/ptests.$(OCAMLBEST)$(EXE) - $(PRINT_RM) installed shared files - $(RM) -R $(FRAMAC_DATADIR) - $(PRINT_RM) installed libraries - $(RM) -R $(FRAMAC_LIBDIR) $(FRAMAC_PLUGINDIR) - $(PRINT_RM) installed man files - $(RM) $(MANDIR)/man1/frama-c.1 $(MANDIR)/man1/frama-c-gui.1 - -################################ -# File headers: license policy # -################################ - - -# Generating headers -#################### - -# Default header specification files -HEADER_SPEC := $(DEFAULT_HEADER_SPEC) -# The list can be extended by external plugins using PLUGIN_HEADER_SPEC variable -HEADER_SPEC += $(PLUGIN_HEADER_SPEC_LIST) -# Default list of header specification files can be overloaded. -HEADER_SPEC_FILE?=$(HEADER_SPEC) - -# Default directory (containing subdirectories open-source and close-source) -HEADER_DIRS := $(DEFAULT_HEADER_DIRS) -# The list can be extended by external plugins using PLUGIN_HEADER_DIRS variable -HEADER_DIRS += $(PLUGIN_HEADER_DIRS_LIST) -# Takes into account the kind of distribution (open-souce/close-source) -DISTRIB_HEADER_DIRS?=$(addsuffix /$(DISTRIB_HEADERS),$(HEADER_DIRS)) - -# List of distributed files allowed to have no entry into the HEADER_SPEC_FILE -HEADER_EXCEPTIONS := $(DEFAULT_HEADER_EXCEPTIONS) -HEADER_EXCEPTIONS += opam/files $(wildcard $(PLUGIN_HEADER_EXCEPTIONS_LIST)) - -# List of headers that cannot be part of an open-source distribution -CEA_PROPRIETARY_HEADERS := $(DEFAULT_CEA_PROPRIETARY_HEADERS) -CEA_PROPRIETARY_HEADERS += $(PLUGIN_CEA_PROPRIETARY_HEADERS_LIST) - -# List of files that cannot be part of an open-source distribution -CEA_PROPRIETARY_FILES := $(DEFAULT_CEA_PROPRIETARY_FILES) -CEA_PROPRIETARY_FILES += $(PLUGIN_CEA_PROPRIETARY_FILES_LIST) - -HDRCK=./headers/hdrck$(EXE) - -HDRCK_EXTRA?=$(STRICT_HEADERS) -# Can be set to "-exit-on-warning" -ifeq ($(HDRCK_EXTRA),no) -HDRCK_EXTRA:="" -else -ifeq ($(HDRCK_EXTRA),yes) -HDRCK_EXTRA:="-exit-on-warning" -endif -endif - -.PHONY: headers - -# OPEN_SOURCE: set it to 'no' if you want to apply close source headers. -# STRICT_HEADERS: set it to 'yes' if you want to consider warnings as errors -headers:: $(HDRCK) - $(PRINT) "|$(OPEN_SOURCE)|$(SPECIFIED_OPEN_SOURCE)|" - $(PRINT) "Applying $(HDRCK_DISTRIB_HEADERS) headers (OPEN_SOURCE=$(HDRCK_OPEN_SOURCE))..." - $(PRINT) "- HEADER_SPEC_FILE=$(HEADER_SPEC_FILE)" - $(PRINT) "- DISTRIB_HEADER_DIRS=$(HDRCK_DISTRIB_HEADER_DIRS)" - $(HDRCK) \ - $(HDRCK_EXTRA) \ - -update -C . \ - $(addprefix -header-dirs ,$(HDRCK_DISTRIB_HEADER_DIRS)) \ - -headache-config-file ./headers/headache_config.txt \ - $(HEADER_SPEC_FILE) - -hdrck: $(HDRCK) - -$(HDRCK): headers/hdrck.ml - $(PRINT_MAKING) $@ -ifeq ($(OCAMLBEST),opt) - $(OCAMLOPT) str.cmxa unix.cmxa $< -o $@ -else - $(OCAMLC) str.cma unix.cma $< -o $@ -endif - -hdrck-clean: - $(RM) headers/hdrck headers/hdrck.o - $(RM) headers/hdrck.cmx headers/hdrck.cmi headers/hdrck.cmp - -clean:: hdrck-clean - -CURRENT_HEADERS?=open-source -CURRENT_HEADER_DIRS?=$(addsuffix /$(CURRENT_HEADERS),$(HEADER_DIRS)) - -# OPEN_SOURCE: set it to 'yes' if you want to check open source headers -# STRICT_HEADERS: set it to 'yes' if you want to consider warnings as errors -# The target check-headers does the following checks: -# 1. Checks entries of HEADER_SPEC_FILE -# 2. Checks that every DISTRIB_FILES (except HEADER_EXCEPTIONS) have an entry -# inside HEADER_SPEC_FILE -# 3. Checks that all these files are not under DISTRIB_PROPRIETARY_HEADERS -# licences -# Also check that distributed files are not encoded in ISO-8859. Do this first, -# because identical headers but with different encodings are not exactly -# easy to distinguish -.PHONY: check-headers -check-headers: $(HDRCK) - $(PRINT) "Checking $(DISTRIB_HEADERS) headers (OPEN_SOURCE=$(OPEN_SOURCE), CURRENT_HEADERS=$(CURRENT_HEADERS))..." - $(PRINT) "- HEADER_SPEC_FILE=$(HEADER_SPEC_FILE)" - $(PRINT) "- CURRENT_HEADER_DIRS=$(CURRENT_HEADER_DIRS)" - $(PRINT) "- FORBIDDEN_HEADERS=$(DISTRIB_PROPRIETARY_HEADERS)" - # Workaround to avoid "argument list too long" in make 3.82+ without - # using 'file' built-in, only available on make 4.0+ - # for make 4.0+, using the 'file' function could be a better solution, - # although it seems to segfault in 4.0 (but not in 4.1) - $(RM) file_list_to_check.tmp file_list_exceptions.tmp - @$(foreach file,$(DISTRIB_FILES),\ - echo $(file) >> file_list_to_check.tmp$(NEWLINE)) - @$(foreach file,$(HEADER_EXCEPTIONS),\ - echo $(file) >> file_list_exceptions.tmp$(NEWLINE)) - - @if command -v file >/dev/null 2>/dev/null; then \ - echo "Checking that distributed files do not use iso-8859..."; \ - file --mime-encoding -f file_list_to_check.tmp | \ - grep "iso-8859" \ - | $(SED) "s/^/error: invalid encoding in /" \ - | ( ! grep "error: invalid encoding" ); \ - else echo "command 'file' not found, skipping encoding checks"; \ - fi - $(HDRCK) \ - $(HDRCK_EXTRA) \ - $(addprefix -header-dirs ,$(CURRENT_HEADER_DIRS)) \ - $(addprefix -forbidden-headers ,$(DISTRIB_PROPRIETARY_HEADERS)) \ - -headache-config-file ./headers/headache_config.txt \ - -distrib-file file_list_to_check.tmp \ - -header-except-file file_list_exceptions.tmp \ - $(HEADER_SPEC_FILE) - $(RM) file_list_to_check.tmp file_list_exceptions.tmp +ALL_LIBRARY_NAMES=$(shell ocamlfind query -r -p-format $(LIBRARY_NAMES) $(LIBRARY_NAMES_GUI)) \ + frama-c.init frama-c.kernel frama-c.gui + +ifeq ($(HAS_OCAML408),yes) + DYNLINK_INIT=fun () -> () + FORMAT_STAG=stag + FORMAT_STRING_OF_STAG=match s with \ + Format.String_tag str -> str \ + | _ -> raise (Invalid_argument \"unsupported tag extension\") + FORMAT_STAG_OF_STRING=Format.String_tag s + FORMAT_PP_OPT=Format.pp_print_option + HAS_OCAML407_OR_408=yes +else + DYNLINK_INIT=Dynlink.init + FORMAT_STAG=tag + FORMAT_STRING_OF_STAG=s + FORMAT_STAG_OF_STRING=s + ifeq ($(HAS_OCAML407),yes) + HAS_OCAML407_OR_408=yes + else + HAS_OCAML407_OR_408=no + endif + FORMAT_PP_OPT=fun ?(none=(fun _ () -> ())) pp fmt o -> \ + match o with \ + | None -> none fmt () \ + | Some v -> pp fmt v +endif + +ifeq ($(HAS_OCAML407_OR_408),yes) + FLOAT_MAX_FLOAT=Float.max_float +else + FLOAT_MAX_FLOAT=Pervasives.max_float +endif + + +MAJOR_VERSION=$(shell $(SED) -E 's/^([0-9]+)\..*/\1/' VERSION) +MINOR_VERSION=$(shell $(SED) -E 's/^[0-9]+\.([0-9]+).*/\1/' VERSION) +VERSION_CODENAME=$(shell $(CAT) VERSION_CODENAME) + +config.sed: VERSION share/Makefile.config Makefile configure.in + @echo "# generated file" > $@ + @echo "s|@VERSION_CODENAME@|$(VERSION_CODENAME)|" >> $@ + @echo "s|@VERSION@|$(VERSION)|" >> $@ + @echo "s|@CURR_DATE@|$$(LC_ALL=C date)|" >> $@ + @echo "s|@OCAMLC@|$(OCAMLC)|" >> $@ + @echo "s|@OCAMLOPT@|$(OCAMLOPT)|" >> $@ + @echo "s|@WARNINGS@|$(WARNINGS)|" >> $@ + @echo "s|@FRAMAC_DATADIR@|$(FRAMAC_DATADIR)|" >> $@ + @echo "s|@FRAMAC_LIBDIR@|$(FRAMAC_LIBDIR)|" >> $@ + @echo "s|@FRAMAC_ROOT_SRCDIR@|$(FRAMAC_ROOT_SRCDIR)|" >> $@ + @echo "s|@FRAMAC_PLUGINDIR@|$(FRAMAC_PLUGINDIR)|" >> $@ + @echo "s|@FRAMAC_DEFAULT_CPP@|$(FRAMAC_DEFAULT_CPP)|" >> $@ + @echo "s|@FRAMAC_DEFAULT_CPP_ARGS@|$(FRAMAC_DEFAULT_CPP_ARGS)|" >> $@ + @echo "s|@FRAMAC_GNU_CPP@|$(FRAMAC_GNU_CPP)|" >> $@ + @echo "s|@DEFAULT_CPP_KEEP_COMMENTS@|$(DEFAULT_CPP_KEEP_COMMENTS)|" >> $@ + @echo "s|@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@|$(DEFAULT_CPP_SUPPORTED_ARCH_OPTS)|" >> $@ + @echo "s|@LIBRARY_NAMES@|$(foreach p,$(ALL_LIBRARY_NAMES),\"$p\";)|" >> $@ + @echo "s|@OPTDOT@|$(OPTDOT)|" >> $@ + @echo "s|@EXE@|$(EXE)|" >> $@ + @echo "s/@SPLIT_ON_CHAR@/$(SPLIT_ON_CHAR)/g" >> $@ + @echo "s/@STACK_FOLD@/$(STACK_FOLD)/g" >> $@ + @echo "s/@NTH_OPT@/$(NTH_OPT)/g" >> $@ + @echo "s/@FIND_OPT@/$(FIND_OPT)/g" >> $@ + @echo "s/@ASSOC_OPT@/$(ASSOC_OPT)/g" >> $@ + @echo "s/@ASSQ_OPT@/$(ASSQ_OPT)/g" >> $@ + @echo "s/@HAS_YOJSON@/$(HAS_YOJSON)/g" >> $@ + @echo "s|@MAJOR_VERSION@|$(MAJOR_VERSION)|g" >> $@ + @echo "s|@MINOR_VERSION@|$(MINOR_VERSION)|g" >> $@ + @echo "s/@DYNLINK_INIT@/$(DYNLINK_INIT)/g" >> $@ + @echo "s/@FORMAT_STAG@/$(FORMAT_STAG)/g" >> $@ + @echo "s/@FORMAT_STRING_OF_STAG@/$(FORMAT_STRING_OF_STAG)/g" >> $@ + @echo "s/@FORMAT_STAG_OF_STRING@/$(FORMAT_STAG_OF_STRING)/g" >> $@ + @echo "s/@FLOAT_MAX_FLOAT@/$(FLOAT_MAX_FLOAT)/g" >> $@ + @echo "s/@FORMAT_PP_OPT@/$(FORMAT_PP_OPT)/g" >> $@ + +clean: + dune clean + rm -rf _build .merlin config.sed + +%.cmxs: %.ml + dune exec -- ocamlfind ocamlopt -package frama-c.kernel -open Frama_c_kernel -shared -o $@ $< + +%.o: %.ml + dune exec -- ocamlfind ocamlopt -package frama-c.kernel -open Frama_c_kernel -c -o $@ $< ######################################################################## -# Makefile is rebuilt whenever Makefile.in or configure.in is modified # +# Makefile.config is rebuilt whenever configure.in is modified # ######################################################################## share/Makefile.config: share/Makefile.config.in config.status @@ -2193,353 +158,22 @@ configure: configure.in .force-reconfigure $(PRINT_MAKING) $@ autoconf -f -# If 'make clean' has to be performed after 'svn update': -# change '.make-clean-stamp' before 'svn commit' +# If 'make clean' has to be performed after 'git pull': +# change '.make-clean-stamp' before 'git commit' .make-clean: .make-clean-stamp $(TOUCH) $@ $(QUIET_MAKE) clean include .make-clean -# force "make clean" to be executed for all users of SVN +# force "make clean" to be executed for all users of GIT force-clean: expr `$(CAT) .make-clean-stamp` + 1 > .make-clean-stamp -# force a reconfiguration for all svn users +# force a reconfiguration for all git users force-reconfigure: expr `$(CAT) .force-reconfigure` + 1 > .force-reconfigure -.PHONY: force-clean force-reconfigure - -############ -# cleaning # -############ - -clean-journal: - $(PRINT_RM) journal - $(RM) frama_c_journal* - -clean-tests: - $(PRINT_RM) tests - $(RM) tests/*/*.byte$(EXE) tests/*/*.opt$(EXE) tests/*/*.cm* \ - tests/dynamic/.cm* tests/*/*~ tests/*/#* - $(RM) tests/*/result/*.* - -clean-doc:: $(PLUGIN_LIST:=_CLEAN_DOC) - $(PRINT_RM) documentation - $(RM) -r $(DOC_DIR)/html - $(RM) $(DOC_DIR)/docgen.cm* $(DOC_DIR)/*~ - $(RM) doc/db/*~ doc/db/ocamldoc.sty doc/db/db.tex - $(RM) doc/training/*/*.cm* - if [ -f doc/developer/Makefile ]; then \ - $(MAKE) --silent -C doc/developer clean; \ - fi - -clean-gui:: - $(PRINT_RM) gui - $(RM) src/*/*/*_gui.cm* src/*/*/*_gui.o \ - src/plugins/gui/*.cm* src/plugins/gui/*.o - -clean:: $(PLUGIN_LIST:=_CLEAN) \ - clean-tests clean-journal clean-check-libc - $(PRINT_RM) lib/plugins - $(RM) $(addprefix $(PLUGIN_LIB_DIR)/,*.mli *.cm* *.o META.*) - $(RM) $(addprefix $(PLUGIN_TOP_LIB_DIR)/,*.mli *.cm* *.o *.a) - $(RM) $(addprefix $(PLUGIN_GUI_LIB_DIR)/,*.mli *.cm* *.o *.a) - $(PRINT_RM) local installation - $(RM) lib/*.cm* lib/*.o lib/fc/*.cm* lib/fc/*.o lib/gui/*.cm* lib/*.cm* - $(PRINT_RM) other sources - for d in . $(SRC_DIRS) src/plugins/gui share; do \ - $(RM) $$d/*.cm* $$d/*.o $$d/*.a $$d/*.annot $$d/*~ $$d/*.output \ - $$d/*.annot $$d/\#*; \ - done - $(PRINT_RM) generated files - $(RM) $(GENERATED) - $(PRINT_RM) binaries - $(RM) bin/toplevel.byte$(EXE) bin/viewer.byte$(EXE) \ - bin/ptests.byte$(EXE) bin/*.opt$(EXE) bin/toplevel.top$(EXE) - $(RM) bin/fc-config$(EXE) - -smartclean: - $(MAKE) -f share/Makefile.clean smartclean - -# Do NOT use :: for this rule: it is mandatory to remove share/Makefile.config -# as the very last step performed by make (who'll otherwise try to regenerate -# it in the middle of cleaning) -dist-clean distclean: clean clean-doc \ - $(PLUGIN_LIST:=_DIST_CLEAN) - $(PRINT_RM) config - $(RM) share/Makefile.config - $(RM) config.cache config.log config.h - $(RM) -r autom4te.cache - $(PRINT_RM) documentation - $(RM) $(DOC_DIR)/kernel-doc.ocamldoc - $(PRINT_RM) dummy plug-ins - $(RM) src/dummy/*/*.cm* src/dummy/*/*.o src/dummy/*/*.a \ - src/dummy/*/*.annot src/dummy/*/*~ src/dummy/*/*.output \ - src/dummy/*/*.annot src/dummy/*/\#* - - -ifeq ($(OCAMLWIN32),yes) -# Use Win32 typical resources -share/frama-c.rc: share/frama-c.WIN32.rc - $(PRINT_MAKING) $@ - $(CP) $^ $@ -else -# Use Unix typical resources -share/frama-c.rc: share/frama-c.Unix.rc - $(PRINT_MAKING) $@ - $(CP) $^ $@ -endif - -GENERATED+=share/frama-c.rc - -########## -# Depend # -########## - -PLUGIN_DEP_LIST:=$(PLUGIN_LIST) - -.PHONY: depend - -# in case .depend is absent, we will make it. Otherwise, it will be left -# untouched. Only make depend will force a recomputation of dependencies -.depend: $(GENERATED) share/Makefile.dynamic_config - $(MAKE) depend - -depend:: $(GENERATED) share/Makefile.dynamic_config - $(PRINT_MAKING) .depend - $(RM) .depend - $(OCAMLDEP) $(INCLUDES) $(FILES_FOR_OCAMLDEP) > .depend - $(OCAMLDEP) $(INCLUDES) $(TEST_DIRS_AS_PLUGIN:%=-I tests/%) \ - $(LONELY_TESTS_ML_FILES) >> .depend - $(CHMOD_RO) .depend - -#Used by internal plugins to wait until the *.mli of all the plugins are in -# $(PLUGIN_LIB_DIR) before computing their .depend. Otherwise ocamldep doesn't -# mark inter-plugin dependencies -$(PLUGIN_LIB_DIR)/.placeholders_ready: - touch $@ - -ifneq ($(MAKECMDGOALS),clean) -ifneq ($(MAKECMDGOALS),distclean) -ifneq ($(MAKECMDGOALS),smartclean) -ifneq ($(MAKECMDGOALS),depend) -sinclude .depend -endif -endif -endif -endif - -##################### -# ptest development # -##################### - -.PHONY: ptests - -PTESTS_SRC=ptests/ptests_config.ml ptests/ptests.ml - -# Do not generate tests/ptests_config if we are compiling a distribution -# that does not contain a 'tests' dir -PTESTS_CONFIG:= $(shell if test -d tests; then echo tests/ptests_config; fi) - -ifneq ("$(PTESTS_CONFIG)","") -GENERATED_TESTS:=tests/spec/preprocess_dos.c -else -GENERATED_TESTS:= -endif - -tests/spec/preprocess_dos.c: tests/spec/preprocess_dos.c.in \ - Makefile share/Makefile.config - $(RM) $@ - $(SED) -e "s|@UNIX2DOS@|$(PP_DOS_UNIX2DOS)|g" \ - -e "s|@DONTRUN@|$(PP_DOS_DONTRUN)|g" \ - $< > $@ - $(CHMOD_RO) $@ - -ifneq ("$(HAS_UNIX2DOS)","no") -tests/spec/preprocess_dos.c: PP_DOS_UNIX2DOS=$(UNIX2DOS) -tests/spec/preprocess_dos.c: PP_DOS_DONTRUN= -else -tests/spec/preprocess_dos.c: PP_DOS_UNIX2DOS=unix2dos -tests/spec/preprocess_dos.c: PP_DOS_DONTRUN=DONTRUN: no unix2dos found -endif - -ptests: bin/ptests.$(OCAMLBEST)$(EXE) $(PTESTS_CONFIG) $(GENERATED_TESTS) - -bin/ptests.byte$(EXE): $(PTESTS_SRC) - $(PRINT_LINKING) $@ - $(OCAMLC) -I ptests -dtypes -thread -g -o $@ \ - unix.cma threads.cma str.cma dynlink.cma $^ - -bin/ptests.opt$(EXE): $(PTESTS_SRC) - $(PRINT_LINKING) $@ - $(OCAMLOPT) -I ptests -dtypes -thread -o $@ \ - unix.cmxa threads.cmxa str.cmxa dynlink.cmxa $^ - -GENERATED+=ptests/ptests_config.ml tests/ptests_config $(GENERATED_TESTS) - -####################### -# Source distribution # -####################### - -.PHONY: src-distrib - -STANDALONE_PLUGINS_FILES = \ - $(addprefix src/dummy/hello_world/,hello_world.ml Makefile) \ - $(addprefix src/dummy/untyped_metrics/,count_for.ml Makefile) - -DISTRIB_FILES += $(wildcard $(PLUGIN_DISTRIBUTED_LIST) \ - $(PLUGIN_DIST_EXTERNAL_LIST) \ - $(PLUGIN_DIST_DOC_LIST) $(STANDALONE_PLUGINS_FILES)) -DISTRIB_FILES:=$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST),\ - $(DISTRIB_FILES)) - -DISTRIB_TESTS += $(wildcard $(PLUGIN_DIST_TESTS_LIST)) - - -SPECIFIED_OPEN_SOURCE:=$(OPEN_SOURCE) -OPEN_SOURCE ?= no - -ifneq ($(OPEN_SOURCE),yes) -# close source version -DISTRIB_HEADERS:=close-source -DISTRIB_PROPRIETARY_HEADERS:= -else -# open source version -DISTRIB_HEADERS:=open-source -# for checking that distributed files aren't under proprietary licence. -DISTRIB_PROPRIETARY_HEADERS:=$(CEA_PROPRIETARY_HEADERS) -# DISTRIB_TESTS contents files that can be distributed without header checking -DISTRIB_TESTS:=$(filter-out $(CEA_PROPRIETARY_FILES) ,\ - $(DISTRIB_TESTS)) -# DISTRIB_FILES contents files that can be distributed with header checking -DISTRIB_FILES:=$(filter-out $(CEA_PROPRIETARY_FILES) ,\ - $(DISTRIB_FILES)) -endif - -# Set some variables for `headers`target. -ifeq ($(OPEN_SOURCE),$(SPECIFIED_OPEN_SOURCE)) -# The OPEN_SOURCE variable is specified. So, use it for `make headers` -HDRCK_OPEN_SOURCE=$(SPECIFIED_OPEN_SOURCE) -HDRCK_DISTRIB_HEADERS=$(DISTRIB_HEADERS) -HDRCK_DISTRIB_HEADER_DIRS=$(DISTRIB_HEADER_DIRS) -else -# The OPEN_SOURCE variable is unspecified. So, use open-source default for `make headers` -HDRCK_OPEN_SOURCE=unspecified -HDRCK_DISTRIB_HEADERS=open-source -HDRCK_DISTRIB_HEADER_DIRS?=$(addsuffix /$(HDRCK_DISTRIB_HEADERS),$(HEADER_DIRS)) -endif - -# Variables governing the name of the generated .tar.gz. -# Optionally define them as empty to silence warnings about undefined variables -CLIENT ?= - -DISTRIB_DIR=tmp -ifeq ("$(CLIENT)","") -VERSION_NAME:=$(VERSION) -else -VERSION_NAME:=$(VERSION)-$(CLIENT) -endif - -DISTRIB?=frama-c-$(VERSION_NAME)-$(VERSION_CODENAME) -CLIENT_DIR=$(DISTRIB_DIR)/$(DISTRIB) - - -# useful parameters: -# CLIENT: name of the client (in the version number, the archive name, etc) -# DISTRIB: name of the generated tarball and of the root tarball directory -# OPEN_SOURCE: set it to 'yes' if you want to exclude close source files -# note: make headers has to be applied... -src-distrib: $(HDRCK) check-headers -ifeq ("$(CLIENT)","") - $(PRINT_BUILD) "$(DISTRIB_HEADERS) tarball $(DISTRIB) (OPEN_SOURCE=$(OPEN_SOURCE))" -else - $(PRINT_BUILD) "$(DISTRIB_HEADERS) tarball $(DISTRIB) for $(CLIENT) (OPEN_SOURCE=$(OPEN_SOURCE))" -endif - $(RM) -r $(CLIENT_DIR) - $(MKDIR) -p $(CLIENT_DIR) - @#Workaround to avoid "argument list too long" in make 3.82+ without - @#using 'file' built-in, only available on make 4.0+ - @#for make 4.0+, using the 'file' function could be a better solution, - @#although it seems to segfault in 4.0 (but not in 4.1) - $(RM) file_list_to_archive.tmp - @$(foreach file,$(DISTRIB_FILES) $(DISTRIB_TESTS),\ - echo $(file) | $(SED) 's/@/ /g' >> file_list_to_archive.tmp$(NEWLINE)) - $(TAR) -cf - --files-from file_list_to_archive.tmp | $(TAR) -C $(CLIENT_DIR) -xf - - $(RM) file_list_to_archive.tmp - $(PRINT_MAKING) files - (cd $(CLIENT_DIR) ; \ - echo "$(VERSION_NAME)" > VERSION && \ - DISTRIB_CONF=yes autoconf > ../../.log.autoconf 2>&1) - $(MKDIR) $(CLIENT_DIR)/bin - $(MKDIR) $(CLIENT_DIR)/lib/plugins - $(MKDIR) $(CLIENT_DIR)/lib/gui - $(RM) ../$(DISTRIB).tar.gz - $(PRINT) "Updating files to archive with $(DISTRIB_HEADERS) headers" - $(HDRCK) \ - $(HDRCK_EXTRA) \ - -update -C $(CLIENT_DIR) \ - $(addprefix -header-dirs ,$(DISTRIB_HEADER_DIRS)) \ - -headache-config-file ./headers/headache_config.txt \ - $(HEADER_SPEC_FILE) - $(PRINT_TAR) $(DISTRIB).tar.gz - (cd $(DISTRIB_DIR); $(TAR) cf - \ - --numeric-owner --owner=0 --group=0 --sort=name \ - --mtime="$$(date +"%F") Z" --mode='a+rw' \ - --exclude "*autom4te.cache*" \ - $(DISTRIB) | gzip -9 -n > ../$(DISTRIB).tar.gz \ - ) - $(PRINT_RM) $(DISTRIB_DIR) - $(RM) -r $(DISTRIB_DIR) - -doc-companions: - $(MAKE) -C doc/developer archives VERSION=$(VERSION)-$(VERSION_CODENAME) - $(MV) doc/developer/hello-$(VERSION)-$(VERSION_CODENAME).tar.gz hello-$(VERSION)-$(VERSION_CODENAME).tar.gz - $(ECHO) "The documentation companion hello-$(VERSION)-$(VERSION_CODENAME).tar.gz has been generated." - -clean-distrib: dist-clean - $(PRINT_RM) distrib - $(RM) -r $(DISTRIB_DIR) $(DISTRIB).tar.gz - -create_lib_to_install_list = $(addprefix $(FRAMAC_LIB)/,$(call map,notdir,$(1))) - -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) lib/fc/META.frama-c - -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) lib/fc/META.frama-c - -top: bin/toplevel.top$(EXE) \ - $(call create_lib_to_install_list,$(LIB_BYTE_TO_INSTALL)) \ - $(PLUGIN_META_LIST) - -################## -# Copy in lib/fc # -################## - -define copy_in_lib -$(FRAMAC_LIB)/$(notdir $(1)): $(1) - $(MKDIR) $(FRAMAC_LIB) - $(CP) $$< $$@ - -endef -$(eval $(foreach file,$(LIB_BYTE_TO_INSTALL),$(call copy_in_lib,$(file)))) -$(eval $(foreach file,$(LIB_OPT_TO_INSTALL),$(call copy_in_lib,$(file)))) - -################ -# Generic part # -################ - -$(NON_OPAQUE_DEPS:%=%.cmx): OFLAGS := $(OFLAGS) -w -58 - -$(CROWBAR_AFL_TARGET:%=%.cmx): OFLAGS:=$(OFLAGS) -afl-instrument - -include share/Makefile.generic ############################################################################### # Local Variables: diff --git a/bin/frama-c b/bin/frama-c index 4591141e0851d21cfedc2a9447aa023e84106a3d..e345ea37e7eea417e96f067827e2a6d02f952306 100755 --- a/bin/frama-c +++ b/bin/frama-c @@ -22,6 +22,4 @@ ########################################################################## -. $(dirname $0)/local_export.sh - -exec $BINDIR/toplevel.opt "$@" +dune exec --root=$(dirname $0)/.. frama-c -- "$@" diff --git a/bin/frama-c-gui b/bin/frama-c-gui index 340da619cf3dfb431c19ffcd66e0103707533222..8f26e926b788a50d61fef2ac74554dbf0af68f68 100755 --- a/bin/frama-c-gui +++ b/bin/frama-c-gui @@ -22,6 +22,4 @@ ########################################################################## -. $(dirname $0)/local_export.sh - -exec $BINDIR/viewer.opt "$@" +dune exec --root=$(dirname $0)/.. frama-c-gui -- "$@" diff --git a/configure.in b/configure.in index 3f792af4a5f4938a604d93d181bcb4807ebd9999..aa745f3592c87a2d629dddc80894fbc71790a446 100644 --- a/configure.in +++ b/configure.in @@ -42,7 +42,7 @@ # EXE ".exe" if OCAMLWIN32=yes, "" otherwise # DLLEXT ".dll" if OCAMLWIN32=yes, ".so" otherwise -AC_INIT(src/kernel_internals/runtime/boot.ml) +AC_INIT(src/init/boot/boot.ml) define([FRAMAC_MAIN_AUTOCONF]) m4_include(share/configure.ac) diff --git a/dune b/dune new file mode 100644 index 0000000000000000000000000000000000000000..66a430ca57cd17fe6d6aee55f54cd56539728f8b --- /dev/null +++ b/dune @@ -0,0 +1 @@ +(dirs src ptests tests share) diff --git a/dune-project b/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..5223efa61d5e72036abbcf294e6f8e8d6df0a1c6 --- /dev/null +++ b/dune-project @@ -0,0 +1,4 @@ +(lang dune 2.8) + +(using dune_site 0.1) +(package (name frama-c) (sites (share share) (lib plugins) (lib plugins_gui))) diff --git a/frama-c.opam b/frama-c.opam new file mode 100644 index 0000000000000000000000000000000000000000..d988d4431d4eba5cc5ee0b5afc2ad9b47e521f2d --- /dev/null +++ b/frama-c.opam @@ -0,0 +1,118 @@ +opam-version: "1.2" +name: "frama-c-base" +version: "20170501" +maintainer: "francois.bobot@cea.fr" +authors: [ + "Michele Alberti" + "Gergö Barany" + "Patrick Baudin" + "François Bobot" + "Richard Bonichon" + "David Bühler" + "Loïc Correnson" + "Julien Crétin" + "Pascal Cuoq" + "Zaynah Dargaye" + "Jean-Christophe Filliâtre" + "Philippe Herrmann" + "Florent Kirchner" + "Tristan Le Gall" + "Jean-Christophe Léchenet" + "Matthieu Lemerre" + "David Maison" + "Claude Marché" + "André Maroneze" + "Benjamin Monate" + "Yannick Moy" + "Anne Pacalet" + "Valentin Perrelle" + "Guillaume Petiot" + "Virgile Prevosto" + "Armand Puccetti" + "Muriel Roger" + "Julien Signoles" + "Kostyantyn Vorobyov" + "Boris Yakobowski" +] +homepage: "http://frama-c.com/" +license: "GNU Lesser General Public License version 2.1" +dev-repo: "https://github.com/Frama-C/Frama-C-snapshot.git" +doc: ["http://frama-c.com/download/user-manual-Phosphorus-20170501.pdf"] +bug-reports: "https://bts.frama-c.com/" +tags: [ + "deductive" + "program verification" + "formal specification" + "automated theorem prover" + "interactive theorem prover" + "C" + "plugins" + "abstract interpretation" + "slicing" + "weakest precondition" + "ACSL" + "dataflow analysis" +] + +build: [ + ["sh" "-eux" "./run_autoconf_if_needed.sh"] # when used in pinned mode, + # the configure *cannot* yet be + # generated + ["./configure" "--prefix" prefix + "--disable-gui" { !conf-gtksourceview:installed | + !conf-gnomecanvas:installed } +] + [make "-j%{jobs}%"] +] + +install: [ + [make "install"] +] + +remove: [ + ["sh" "-eux" "./run_autoconf_if_needed.sh"] # when used in pinned mode, + # the configure *cannot* yet be + # generated + ["./configure" "--prefix" prefix + "--disable-gui" { !conf-gtksourceview:installed | + !conf-gnomecanvas:installed } +] + [make "uninstall"] + ["rm" "-rf" frama-c-base:doc] +] + +build-doc: [ + [make "-C" "doc" "download"] + [make "-C" "doc" "FRAMAC_DOCDIR=%{frama-c-base:doc}%" "install"] +] + +build-test: [ + [make "-j%{jobs}%" "PTESTS_OPTS=-error-code" "tests"] +] + +depends: [ + "ocamlgraph" { >= "1.8.5" & < "1.9~" } + "ocamlfind" + "zarith" +] + +depopts: [ + "lablgtk" + "conf-gtksourceview" + "conf-gnomecanvas" + "coq" { build } + "why3" { build } +] + +messages: [ + "Why3 can be used by the WP plug-in for running additional automatic solvers" { !why3:installed } + "Coq can be used with the WP plug-in for proving interactively proof obligations" { !coq:installed } +] + +conflicts: [ + "why3-base" { < "0.86" } #for WP plug-in + "coq" { < "8.4.6" } #for WP plug-in + "lablgtk" { < "2.18.2" } #for ocaml >= 4.02.1 +] + +available: [ ocaml-version >= "4.02.3" ] diff --git a/nix/default.nix b/nix/default.nix index 610b886c089a9da73b709082f2bde0900ac13421..56f33e2a54f5a5005ba64f6c99790cce8d3cba02 100644 --- a/nix/default.nix +++ b/nix/default.nix @@ -3,7 +3,8 @@ let mk_buildInputs = { opamPackages ? [], nixPackages ? [] } : [ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl pkgs.file pkgs.which pkgs.dos2unix] ++ nixPackages ++ opam2nix.build { - specs = opam2nix.toSpecs ([ "ocamlfind" "zarith" "ocamlgraph" "yojson" + specs = opam2nix.toSpecs ([ "ocamlfind" "zarith" "ocamlgraph" "yojson" "lablgtk" "conf-gtksourceview" "conf-gnomecanvas" + { name = "dune"; constraint = ">=2.7"; } { name = "coq"; constraint = "=8.11.1"; } { name = "why3" ; constraint = "=1.3.1"; } { name = "why3-coq" ; constraint = "=1.3.1"; } diff --git a/ptests/.merlin b/ptests/.merlin deleted file mode 100644 index 6863408c16f24b08a46a30db253008d7fa26cff8..0000000000000000000000000000000000000000 --- a/ptests/.merlin +++ /dev/null @@ -1,2 +0,0 @@ -B +threads - diff --git a/ptests/dune b/ptests/dune new file mode 100644 index 0000000000000000000000000000000000000000..9ab643b2927faaaff59464be208ec14347b663fc --- /dev/null +++ b/ptests/dune @@ -0,0 +1,5 @@ +(executable + (package frama-c) + (public_name ptests) + (libraries unix threads str) +) diff --git a/ptests/ptests.ml b/ptests/ptests.ml index 78469525850ec15315fe997160a282d72e422b8d..b3864bd8aa0ada7aaeb3cff4e79d772fcbf415fd 100644 --- a/ptests/ptests.ml +++ b/ptests/ptests.ml @@ -198,8 +198,10 @@ let do_cmp = ref (if Sys.os_type="Win32" then !do_diffs let do_make = ref "make" let n = ref 4 (* the level of parallelism *) let suites = ref [] + (** options appended to toplevel for all tests *) let additional_options = ref "" + (** options prepended to toplevel for all tests *) let additional_options_pre = ref "" @@ -474,7 +476,7 @@ end = struct let create_if_absent dir = if not (Sys.file_exists dir) - then Unix.mkdir dir 0o750 (** rwxr-w--- *) + then Unix.mkdir dir 0o750 (* rwxr-w--- *) else if not (Sys.is_directory dir) then fail (Printf.sprintf "the file %s exists but is not a directory" dir) @@ -771,7 +773,7 @@ let config_options = (fun _ s current -> let new_top = List.map - (fun (cmd,opts, log, macros,_) -> + (fun (cmd,opts, log, _,_) -> cmd, make_custom_opts opts s, log, current.dc_macros, current.dc_timeout) !current_default_cmds @@ -793,7 +795,7 @@ let config_options = (fun _ _ acc -> acc); "DONTRUN", - (fun _ s current -> { current with dc_dont_run = true }); + (fun _ _ current -> { current with dc_dont_run = true }); "EXECNOW", config_exec ~once:true; "EXEC", config_exec ~once:false; @@ -914,11 +916,11 @@ type log = Err | Res type diff = | Command_error of toplevel_command * log | Target_error of execnow - | Log_error of SubDir.t (** directory *) * string (** file *) + | Log_error of SubDir.t (* directory *) * string (* file *) type cmps = | Cmp_Toplevel of toplevel_command - | Cmp_Log of SubDir.t (** directory *) * string (** file *) + | Cmp_Log of SubDir.t (* directory *) * string (* file *) type shared = { lock : Mutex.t ; @@ -1186,13 +1188,12 @@ let remove_execnow_results execnow = module Make_Report(M:sig type t end)=struct module H=Hashtbl.Make - (struct - type t = toplevel_command - let project cmd = (cmd.directory,cmd.file,cmd.n) - let compare c1 c2 = compare (project c1) (project c2) - let equal c1 c2 = (project c1)=(project c2) - let hash c = Hashtbl.hash (project c) - end) + (struct + type t = toplevel_command + let project cmd = (cmd.directory,cmd.file,cmd.n) + let equal c1 c2 = (project c1)=(project c2) + let hash c = Hashtbl.hash (project c) + end) let tbl = H.create 774 let m = Mutex.create () let record cmd (v:M.t) = diff --git a/share/Makefile.config.in b/share/Makefile.config.in index 0739e3cef9cf47ea569ff43de2d365dc91910a61..a8668095137a0a7f2c49eb515c620544dbdb64b1 100644 --- a/share/Makefile.config.in +++ b/share/Makefile.config.in @@ -186,8 +186,7 @@ ENABLE_USERS ?=@ENABLE_USERS@ ENABLE_EVA ?=@ENABLE_EVA@ #bytes is part of the stdlib, but is used as a transitional package. -LIBRARY_NAMES := \ - findlib ocamlgraph unix str dynlink bytes zarith yojson bigarray +LIBRARY_NAMES := findlib ocamlgraph num unix str dynlink bytes zarith yojson threads threads.posix bigarray ifeq ($(HAS_LANDMARKS),yes) LIBRARY_NAMES += landmarks landmarks.ppx @@ -196,7 +195,7 @@ endif ifneq ($(ENABLE_GUI),no) LIBRARY_NAMES_GUI = $(LABLGTK) $(GTKSOURCEVIEW) ifeq ($(HAS_GNOMECANVAS),yes) - LIBRARY_NAMES_GUI+=lablgtk2.gnomecanvas + LIBRARY_NAMES_GUI+=lablgtk2.gnomecanvas ocamlgraph.dgraph endif else LIBRARY_NAMES_GUI = diff --git a/share/dune b/share/dune new file mode 100644 index 0000000000000000000000000000000000000000..c0f6372badf19109521786b7d1fe1be47f60109c --- /dev/null +++ b/share/dune @@ -0,0 +1,150 @@ +(install + (package frama-c) + (section (site (frama-c share))) + (files +(libc/__fc_define_uid_and_gid.h as libc/__fc_define_uid_and_gid.h) +(libc/__fc_define_clockid_t.h as libc/__fc_define_clockid_t.h) +(libc/assert.c as libc/assert.c) +(libc/stdbool.h as libc/stdbool.h) +(libc/__fc_define_ino_t.h as libc/__fc_define_ino_t.h) +(libc/__fc_inet.h as libc/__fc_inet.h) +(libc/termios.h as libc/termios.h) +(libc/glob.c as libc/glob.c) +(libc/sys/utsname.h as libc/sys/utsname.h) +(libc/sys/resource.h as libc/sys/resource.h) +(libc/sys/random.h as libc/sys/random.h) +(libc/sys/shm.h as libc/sys/shm.h) +(libc/sys/time.h as libc/sys/time.h) +(libc/sys/ioctl.h as libc/sys/ioctl.h) +(libc/sys/wait.h as libc/sys/wait.h) +(libc/sys/socket.h as libc/sys/socket.h) +(libc/sys/select.h as libc/sys/select.h) +(libc/sys/times.h as libc/sys/times.h) +(libc/sys/types.h as libc/sys/types.h) +(libc/sys/file.h as libc/sys/file.h) +(libc/sys/un.h as libc/sys/un.h) +(libc/sys/stat.h as libc/sys/stat.h) +(libc/sys/uio.h as libc/sys/uio.h) +(libc/sys/ipc.h as libc/sys/ipc.h) +(libc/sys/signal.h as libc/sys/signal.h) +(libc/sys/timex.h as libc/sys/timex.h) +(libc/sys/mman.h as libc/sys/mman.h) +(libc/__fc_define_dev_t.h as libc/__fc_define_dev_t.h) +(libc/glob.h as libc/glob.h) +(libc/__fc_define_id_t.h as libc/__fc_define_id_t.h) +(libc/__fc_define_time_t.h as libc/__fc_define_time_t.h) +(libc/stdint.h as libc/stdint.h) +(libc/sched.h as libc/sched.h) +(libc/__fc_define_blksize_t.h as libc/__fc_define_blksize_t.h) +(libc/regex.h as libc/regex.h) +(libc/__fc_define_sa_family_t.h as libc/__fc_define_sa_family_t.h) +(libc/__fc_define_sigset_t.h as libc/__fc_define_sigset_t.h) +(libc/__fc_define_fpos_t.h as libc/__fc_define_fpos_t.h) +(libc/float.h as libc/float.h) +(libc/poll.h as libc/poll.h) +(libc/wchar.c as libc/wchar.c) +(libc/time.c as libc/time.c) +(libc/grp.h as libc/grp.h) +(libc/fenv.h as libc/fenv.h) +(libc/dirent.h as libc/dirent.h) +(libc/semaphore.h as libc/semaphore.h) +(libc/__fc_define_mode_t.h as libc/__fc_define_mode_t.h) +(libc/__fc_define_size_t.h as libc/__fc_define_size_t.h) +(libc/__fc_define_file.h as libc/__fc_define_file.h) +(libc/ifaddrs.h as libc/ifaddrs.h) +(libc/__fc_integer.h as libc/__fc_integer.h) +(libc/__fc_define_off_t.h as libc/__fc_define_off_t.h) +(libc/tgmath.h as libc/tgmath.h) +(libc/iso646.h as libc/iso646.h) +(libc/stdlib.c as libc/stdlib.c) +(libc/stdio.h as libc/stdio.h) +(libc/__fc_define_fd_set_t.h as libc/__fc_define_fd_set_t.h) +(libc/locale.h as libc/locale.h) +(libc/features.h as libc/features.h) +(libc/getopt.h as libc/getopt.h) +(libc/wctype.h as libc/wctype.h) +(libc/ftw.h as libc/ftw.h) +(libc/__fc_runtime.c as libc/__fc_runtime.c) +(libc/stdlib.h as libc/stdlib.h) +(libc/unistd.h as libc/unistd.h) +(libc/math.c as libc/math.c) +(libc/utmpx.h as libc/utmpx.h) +(libc/arpa/inet.h as libc/arpa/inet.h) +(libc/dlfcn.h as libc/dlfcn.h) +(libc/setjmp.h as libc/setjmp.h) +(libc/time.h as libc/time.h) +(libc/fcntl.h as libc/fcntl.h) +(libc/netdb.h as libc/netdb.h) +(libc/__fc_define_pid_t.h as libc/__fc_define_pid_t.h) +(libc/math.h as libc/math.h) +(libc/inttypes.c as libc/inttypes.c) +(libc/pthread.h as libc/pthread.h) +(libc/iconv.h as libc/iconv.h) +(libc/netinet/in.h as libc/netinet/in.h) +(libc/netinet/tcp.h as libc/netinet/tcp.h) +(libc/nl_types.h as libc/nl_types.h) +(libc/libgen.h as libc/libgen.h) +(libc/string.c as libc/string.c) +(libc/memory.h as libc/memory.h) +(libc/stddef.h as libc/stddef.h) +(libc/stropts.h as libc/stropts.h) +(libc/errno.h as libc/errno.h) +(libc/__fc_define_timespec.h as libc/__fc_define_timespec.h) +(libc/pwd.h as libc/pwd.h) +(libc/malloc.h as libc/malloc.h) +(libc/resolv.h as libc/resolv.h) +(libc/netdb.c as libc/netdb.c) +(libc/__fc_gcc_builtins.h as libc/__fc_gcc_builtins.h) +(libc/ctype.c as libc/ctype.c) +(libc/ctype.h as libc/ctype.h) +(libc/unistd.c as libc/unistd.c) +(libc/stdio.c as libc/stdio.c) +(libc/fnmatch.h as libc/fnmatch.h) +(libc/syslog.h as libc/syslog.h) +(libc/endian.h as libc/endian.h) +(libc/stdarg.h as libc/stdarg.h) +(libc/fenv.c as libc/fenv.c) +(libc/string.h as libc/string.h) +(libc/__fc_define_useconds_t.h as libc/__fc_define_useconds_t.h) +(libc/n1336.pdf as libc/n1336.pdf) +(libc/__fc_define_sockaddr.h as libc/__fc_define_sockaddr.h) +(libc/__fc_define_null.h as libc/__fc_define_null.h) +(libc/__fc_machdep.h as libc/__fc_machdep.h) +(libc/__fc_string_axiomatic.h as libc/__fc_string_axiomatic.h) +(libc/__fc_builtin.c as libc/__fc_builtin.c) +(libc/__fc_define_iovec.h as libc/__fc_define_iovec.h) +(libc/__fc_machdep_linux_shared.h as libc/__fc_machdep_linux_shared.h) +(libc/__fc_alloc_axiomatic.h as libc/__fc_alloc_axiomatic.h) +(libc/naming-conventions.md as libc/naming-conventions.md) +(libc/signal.c as libc/signal.c) +(libc/assert.h as libc/assert.h) +(libc/__fc_select.h as libc/__fc_select.h) +(libc/utime.h as libc/utime.h) +(libc/limits.h as libc/limits.h) +(libc/wchar.h as libc/wchar.h) +(libc/getopt.c as libc/getopt.c) +(libc/byteswap.h as libc/byteswap.h) +(libc/__fc_define_intptr_t.h as libc/__fc_define_intptr_t.h) +(libc/__fc_define_pthread_types.h as libc/__fc_define_pthread_types.h) +(libc/__fc_define_nlink_t.h as libc/__fc_define_nlink_t.h) +(libc/inttypes.h as libc/inttypes.h) +(libc/alloca.h as libc/alloca.h) +(libc/__fc_define_key_t.h as libc/__fc_define_key_t.h) +(libc/__fc_define_wchar_t.h as libc/__fc_define_wchar_t.h) +(libc/signal.h as libc/signal.h) +(libc/__fc_define_blkcnt_t.h as libc/__fc_define_blkcnt_t.h) +(libc/net/if.h as libc/net/if.h) +(libc/n1362.pdf as libc/n1362.pdf) +(libc/__fc_define_ssize_t.h as libc/__fc_define_ssize_t.h) +(libc/complex.h as libc/complex.h) +(libc/strings.h as libc/strings.h) +(libc/__fc_define_wint_t.h as libc/__fc_define_wint_t.h) +(libc/__fc_define_eof.h as libc/__fc_define_eof.h) +(libc/__fc_define_suseconds_t.h as libc/__fc_define_suseconds_t.h) +(libc/locale.c as libc/locale.c) +(libc/__fc_define_seek_macros.h as libc/__fc_define_seek_macros.h) +(libc/__fc_define_timer_t.h as libc/__fc_define_timer_t.h) +(libc/__fc_define_stat.h as libc/__fc_define_stat.h) +(libc/errno.c as libc/errno.c) +(libc/__fc_builtin.h as libc/__fc_builtin.h) +)) diff --git a/src/dune b/src/dune new file mode 100644 index 0000000000000000000000000000000000000000..71ff17d8ddf65aa05232bf24dd10d700c9e0a8fc --- /dev/null +++ b/src/dune @@ -0,0 +1,59 @@ +(library + (name frama_c_kernel) + (public_name frama-c.kernel) + (foreign_stubs (language c) (names c_bindings)) + (flags -w -50) + (libraries frama-c.init str unix zarith ocamlgraph dynlink bytes yojson dune-site dune-site.plugins) +) + +(ocamllex json) +(ocamllex logic_preprocess) +(ocamllex logic_lexer) +(ocamlyacc logic_parser) +(ocamllex clexer) +(ocamlyacc cparser) + +(rule + (targets fc_config.ml) + (deps fc_config.ml.in ../config.sed) + (action (with-stdout-to fc_config.ml (run sed -f ../config.sed fc_config.ml.in))) +) + +(generate_module (module config_data) (sites frama-c) (plugins (frama-c plugins) (frama-c plugins_gui))) + +(rule + (targets transitioning.ml) + (deps transitioning.ml.in ../config.sed) + (action (with-stdout-to transitioning.ml (run sed -f ../config.sed transitioning.ml.in))) +) + +;(include_subdirs unqualified) + +(copy_files# kernel_internals/*.ml*) +(copy_files# kernel_services/ast_transformations/*.ml*) +(copy_files# kernel_internals/parsing/*.ml*) +(copy_files# kernel_services/cmdline_parameters/*.ml*) +(copy_files# kernel_internals/runtime/*.ml*) +(copy_files# kernel_services/parsetree/*.ml*) +(copy_files# kernel_internals/typing/*.ml*) +(copy_files# kernel_services/plugin_entry_points/*.ml*) +(copy_files# kernel_services/*.ml*) +(copy_files# kernel_services/visitors/*.ml*) +(copy_files# kernel_services/abstract_interp/*.ml*) +(copy_files# libraries/*.ml*) +(copy_files# kernel_services/analysis/*.ml*) +(copy_files# libraries/datatype/*.ml*) +(copy_files# kernel_services/ast_data/*.ml*) +(copy_files# libraries/project/*.ml*) +(copy_files# kernel_services/ast_printing/*.ml*) +(copy_files# libraries/stdlib/*.ml*) +(copy_files# kernel_services/ast_queries/*.ml*) +(copy_files# libraries/utils/*.ml*) +(copy_files# libraries/utils/*.c) +(copy_files# plugins/value_types/*.ml*) +(copy_files# plugins/pdg_types/*.ml*) + +(alias + (name all) + (deps (file frama_c_kernel.cma)(file frama_c_kernel.cmxa)) +) diff --git a/src/kernel_internals/runtime/boot.ml b/src/init/boot/boot.ml similarity index 100% rename from src/kernel_internals/runtime/boot.ml rename to src/init/boot/boot.ml diff --git a/src/init/boot/dune b/src/init/boot/dune new file mode 100644 index 0000000000000000000000000000000000000000..09aa27a91555089726d0373164317d81266cc3cc --- /dev/null +++ b/src/init/boot/dune @@ -0,0 +1,38 @@ +(library + (name frama_c_boot) + (public_name frama-c.boot) + (modules boot) + (flags -open Frama_c_kernel) + (libraries frama_c_kernel) +) + + +(rule + (targets empty_file.ml) + (action (with-stdout-to empty_file.ml (echo ""))) +) + +(rule + (targets empty_file_gui.ml) + (deps empty_file.ml) + (action (copy# empty_file.ml empty_file_gui.ml)) +) + +(executable + (name empty_file) + (public_name frama-c) + (modules empty_file) + (package frama-c) + (flags -open Frama_c_kernel -linkall) + (libraries frama-c.kernel frama-c.init.cmdline frama-c.boot) +) + +(executable + (name empty_file_gui) + (public_name frama-c-gui) + (modules empty_file_gui) + (package frama-c) + (flags -open Frama_c_kernel -linkall) + (libraries threads frama-c.init.gui frama-c.kernel frama-c.gui frama-c.boot) + (optional) +) diff --git a/src/init/dune b/src/init/dune new file mode 100644 index 0000000000000000000000000000000000000000..ab598dbeef8dbc606f87948736b072847082761f --- /dev/null +++ b/src/init/dune @@ -0,0 +1,6 @@ +(library + (name frama_c_very_first) + (public_name frama-c.init) + (modules frama_c_init gui_init) + (virtual_modules gui_init) +) diff --git a/src/kernel_internals/runtime/frama_c_init.ml b/src/init/frama_c_init.ml similarity index 100% rename from src/kernel_internals/runtime/frama_c_init.ml rename to src/init/frama_c_init.ml diff --git a/src/kernel_internals/runtime/frama_c_init.mli b/src/init/frama_c_init.mli similarity index 100% rename from src/kernel_internals/runtime/frama_c_init.mli rename to src/init/frama_c_init.mli diff --git a/src/kernel_internals/runtime/gui_init.mli b/src/init/gui_init.mli similarity index 93% rename from src/kernel_internals/runtime/gui_init.mli rename to src/init/gui_init.mli index 13608b411ed418dd5f4697a436c104f24415fc99..749539c2becae2b32c97163acbdbe4139b09470b 100644 --- a/src/kernel_internals/runtime/gui_init.mli +++ b/src/init/gui_init.mli @@ -20,8 +20,10 @@ (* *) (**************************************************************************) -(** Very early initialization step required by any GUI. - This interface should be empty. *) +(** Very early initialization step that indicate using a virtual module + if we are in cmdline or gui. *) + +val is_gui: bool (* Local Variables: diff --git a/src/init/impl_cmdline/dune b/src/init/impl_cmdline/dune new file mode 100644 index 0000000000000000000000000000000000000000..0be66d4035c677dda2e77d1835d6279459e20787 --- /dev/null +++ b/src/init/impl_cmdline/dune @@ -0,0 +1,5 @@ +(library + (name frama_c_very_first_cmdline) + (public_name frama-c.init.cmdline) + (implements frama-c.init) +) diff --git a/src/init/impl_cmdline/gui_init.ml b/src/init/impl_cmdline/gui_init.ml new file mode 100644 index 0000000000000000000000000000000000000000..414d5d77d75f96238fd9b1baa7c717ce68a2a392 --- /dev/null +++ b/src/init/impl_cmdline/gui_init.ml @@ -0,0 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2018 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +(** Frama-C Cmdline early initialization. *) + +let is_gui = false diff --git a/src/init/impl_gui/dune b/src/init/impl_gui/dune new file mode 100644 index 0000000000000000000000000000000000000000..5e875e5cd44c78988dd1232ced29f62fd5df2082 --- /dev/null +++ b/src/init/impl_gui/dune @@ -0,0 +1,5 @@ +(library + (name frama_c_very_first_gui) + (public_name frama-c.init.gui) + (implements frama-c.init) +) diff --git a/src/kernel_internals/runtime/gui_init.ml b/src/init/impl_gui/gui_init.ml similarity index 94% rename from src/kernel_internals/runtime/gui_init.ml rename to src/init/impl_gui/gui_init.ml index e01dc6f61c92e28d9a758dd4b1502f7258a5cd9b..78aa2d51667db65368701089a903c55a56138009 100644 --- a/src/kernel_internals/runtime/gui_init.ml +++ b/src/init/impl_gui/gui_init.ml @@ -22,12 +22,6 @@ (** Frama-C GUI early initialization. *) -let () = Fc_config.is_gui := true +let is_gui = true let () = Unix.putenv "UBUNTU_MENUPROXY" "0" - -(* -Local Variables: -compile-command: "make -C ../../.." -End: -*) diff --git a/src/kernel_internals/runtime/toplevel_config.ml b/src/init/toplevel/toplevel_config.ml similarity index 100% rename from src/kernel_internals/runtime/toplevel_config.ml rename to src/init/toplevel/toplevel_config.ml diff --git a/src/kernel_internals/parsing/check_logic_parser.ml b/src/kernel_internals/parsing/tests/check_logic_parser.ml similarity index 100% rename from src/kernel_internals/parsing/check_logic_parser.ml rename to src/kernel_internals/parsing/tests/check_logic_parser.ml diff --git a/src/kernel_internals/runtime/fc_config.ml.in b/src/kernel_internals/runtime/fc_config.ml.in index 8fda151a90da255afe4368634d054349eda881f2..327e1e30a456d33ca9bf5b158b61ad9a567393cf 100644 --- a/src/kernel_internals/runtime/fc_config.ml.in +++ b/src/kernel_internals/runtime/fc_config.ml.in @@ -30,49 +30,17 @@ let major_version = @MAJOR_VERSION@ let minor_version = @MINOR_VERSION@ -let is_gui = ref false +let is_gui = Frama_c_very_first.Gui_init.is_gui let lablgtk = "@LABLGTK@" -let ocamlc = "@OCAMLC@" -let ocamlopt = "@OCAMLOPT@" let ocaml_wflags = "@WARNINGS@" +let datadirs = Config_data.Sites.share +let datadir = List.hd (List.rev Config_data.Sites.share) -let getenv_list name = - let path = Sys.getenv name in - Str.split (Str.regexp ":") path +let plugin_dir = Config_data.Sites.plugins -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 - 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 () = add_symbolic_dir_list "FRAMAC_PLUGIN" plugin_dir let default_cpp = "@FRAMAC_DEFAULT_CPP@" @@ -96,7 +64,4 @@ let preprocessor_supported_arch_options = [@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@] let preprocessor_keep_comments = env_or_default (fun _ -> true) @DEFAULT_CPP_KEEP_COMMENTS@ -let compilation_unit_names = [@COMPILATION_UNITS@] -let library_names = [@LIBRARY_NAMES@] - let dot = @OPTDOT@ diff --git a/src/kernel_internals/runtime/fc_config.mli b/src/kernel_internals/runtime/fc_config.mli index 14f5169a9f042608154549b61dd561c07b36c82a..1cda05b644eff11d468c01fdb6f18edf5c1b7a47 100644 --- a/src/kernel_internals/runtime/fc_config.mli +++ b/src/kernel_internals/runtime/fc_config.mli @@ -42,59 +42,37 @@ val minor_version: int (** Frama-C minor version number. @since 19.0-Potassium *) -val is_gui: bool ref +val is_gui: bool (** Is the Frama-C GUI running? - @since Beryllium-20090601-beta1 *) + @since Beryllium-20090601-beta1 + @since frama-c-trunk not anymore a reference + *) val lablgtk: string (** Name of the lablgtk version against which Frama-C has been compiled. blank if only command-line mode is available. *) -val ocamlc: string -(** Name of the bytecode compiler. - @since Boron-20100401 *) - -val ocamlopt: string -(** Name of the native compiler. - @since Boron-20100401 *) - val ocaml_wflags: string (** Warning flags used when compiling Frama-C. @since Chlorine-20180501 *) -val datadir: string -(** 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 19.0-Potassium *) -val framac_libc: string -(** Directory where Frama-C libc headers are. - @since 19.0-Potassium *) +val datadir: string + (** Last directory of datadirs (the directory of frama-c installation) + @since 19.0-Potassium *) -val libdir: string -(** Directory where the Frama-C kernel library is. - @since Beryllium-20090601-beta1 *) +val framac_libc: string + (** Directory where Frama-C libc headers are. + @since 19.0-Potassium *) val plugin_dir: string list (** Directory where the Frama-C dynamic plug-ins are. @modify Magnesium-20151001 *) -val plugin_path: string -(** The coma-separated concatenation of [plugin_dir]. - @since Magnesium-20151001 *) - -val compilation_unit_names: string list -(** List of names of all kernel compilation units. - @since Boron-20100401 *) - -val library_names: string list -(** List of linked libraries. - @since Magnesium-20151001 *) - val preprocessor: string (** Name of the default command to call the preprocessor. If the CPP environment variable is set, use it diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml index ea0bc0bba1122acb9aecf4d823d43d5999c042fc..b9eb84ac449d1c06a16c85880a3e3024493f5fb2 100644 --- a/src/kernel_internals/runtime/special_hooks.ml +++ b/src/kernel_internals/runtime/special_hooks.ml @@ -36,10 +36,10 @@ let print_config () = "Frama-C %s@\n\ Environment:@\n \ FRAMAC_SHARE = %S@\n \ - FRAMAC_LIB = %S@\n \ FRAMAC_PLUGIN = %S%t@." Fc_config.version_and_codename - Fc_config.datadir Fc_config.libdir Fc_config.plugin_path + (String.concat ":" Fc_config.datadirs) + (String.concat ":" Fc_config.plugin_dir) (fun fmt -> if Fc_config.preprocessor = "" then Format.fprintf fmt "@\nWarning: no default pre-processor" @@ -59,19 +59,21 @@ let print_config get value () = raise Cmdline.Exit end +let print_configl get value () = + if get () then begin + Log.print_on_output (fun fmt -> List.iter (Format.fprintf fmt "%s\n%!") value) ; + raise Cmdline.Exit + end + let print_version = print_config Kernel.PrintVersion.get Fc_config.version_and_codename let () = Cmdline.run_after_early_stage print_version -let print_sharepath = print_config Kernel.PrintShare.get Fc_config.datadir +let print_sharepath = print_configl Kernel.PrintShare.get Fc_config.datadirs let () = Cmdline.run_after_early_stage print_sharepath -let print_libpath = print_config Kernel.PrintLib.get Fc_config.libdir +let print_libpath = print_configl Kernel.PrintLib.get Fc_config.plugin_dir let () = Cmdline.run_after_early_stage print_libpath -let print_pluginpath = - print_config Kernel.PrintPluginPath.get Fc_config.plugin_path -let () = Cmdline.run_after_early_stage print_pluginpath - let print_machdep () = if Kernel.PrintMachdep.get () then begin File.pretty_machdep (); diff --git a/src/kernel_services/abstract_interp/eva_lattice_type.mli b/src/kernel_services/abstract_interp/eva_lattice_type.ml similarity index 100% rename from src/kernel_services/abstract_interp/eva_lattice_type.mli rename to src/kernel_services/abstract_interp/eva_lattice_type.ml diff --git a/src/kernel_services/abstract_interp/float_interval_sig.mli b/src/kernel_services/abstract_interp/float_interval_sig.ml similarity index 100% rename from src/kernel_services/abstract_interp/float_interval_sig.mli rename to src/kernel_services/abstract_interp/float_interval_sig.ml diff --git a/src/kernel_services/abstract_interp/float_sig.mli b/src/kernel_services/abstract_interp/float_sig.ml similarity index 100% rename from src/kernel_services/abstract_interp/float_sig.mli rename to src/kernel_services/abstract_interp/float_sig.ml diff --git a/src/kernel_services/abstract_interp/int_Intervals.mli b/src/kernel_services/abstract_interp/int_Intervals.mli index 9bba8a2b8ec649e58c0f49b7270606554926fd78..284612c257b5570987df029c969c7ed6f8c6e719 100644 --- a/src/kernel_services/abstract_interp/int_Intervals.mli +++ b/src/kernel_services/abstract_interp/int_Intervals.mli @@ -27,7 +27,7 @@ {!Int_Intervals_sig}, and the implementation is in {!Offsetmap.Int_Intervals}. *) -include module type of Int_Intervals_sig +include Int_Intervals_sig.S with type t = Offsetmap.Int_Intervals.t diff --git a/src/kernel_services/abstract_interp/int_Intervals_sig.mli b/src/kernel_services/abstract_interp/int_Intervals_sig.ml similarity index 99% rename from src/kernel_services/abstract_interp/int_Intervals_sig.mli rename to src/kernel_services/abstract_interp/int_Intervals_sig.ml index a33aea2d443e72424b966e6da9c50710bec5f7de..380d9d6da8abb0680ec3e386fb88dcaa4aef2ac9 100644 --- a/src/kernel_services/abstract_interp/int_Intervals_sig.mli +++ b/src/kernel_services/abstract_interp/int_Intervals_sig.ml @@ -27,6 +27,8 @@ open Abstract_interp type itv = Int.t * Int.t +module type S = sig + include Lattice_type.Full_Lattice val is_top: t -> bool @@ -70,6 +72,7 @@ val range_covers_whole_type: Cil_types.typ -> t -> bool val pretty_debug: t Pretty_utils.formatter +end (* Local Variables: diff --git a/src/kernel_services/abstract_interp/lattice_type.mli b/src/kernel_services/abstract_interp/lattice_type.ml similarity index 100% rename from src/kernel_services/abstract_interp/lattice_type.mli rename to src/kernel_services/abstract_interp/lattice_type.ml diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml index f41d068c2d27d1e9426eb2f9d57f84ed7313157e..a462bed04d9b99a6429dfad4898c4c67878931e9 100644 --- a/src/kernel_services/abstract_interp/lmap.ml +++ b/src/kernel_services/abstract_interp/lmap.ml @@ -29,14 +29,14 @@ type 'a default_contents = | Bottom | Top of 'a | Constant of 'a - | Other + | Other module Make_LOffset (V: sig - include module type of Offsetmap_lattice_with_isotropy + include Offsetmap_lattice_with_isotropy.S include Lattice_type.With_Top_Opt with type t := t end) - (Offsetmap: module type of Offsetmap_sig + (Offsetmap: Offsetmap_sig.S with type v = V.t and type widen_hint = V.numerical_widen_hint) (Default_offsetmap: sig diff --git a/src/kernel_services/abstract_interp/lmap.mli b/src/kernel_services/abstract_interp/lmap.mli index 5db64b00f90c7a1516c728f4e684e2aa7c4d72a8..33d655ad5088a713655016f1ebd1a75d7ea6c6bb 100644 --- a/src/kernel_services/abstract_interp/lmap.mli +++ b/src/kernel_services/abstract_interp/lmap.mli @@ -34,10 +34,10 @@ type 'a default_contents = module Make_LOffset (V: sig - include module type of Offsetmap_lattice_with_isotropy + include Offsetmap_lattice_with_isotropy.S include Lattice_type.With_Top_Opt with type t := t end) - (Offsetmap: module type of Offsetmap_sig + (Offsetmap: Offsetmap_sig.S with type v = V.t and type widen_hint = V.numerical_widen_hint) (Default_offsetmap: sig @@ -70,7 +70,7 @@ module Make_LOffset match [default_contents] on constant keys. *) end): - module type of Lmap_sig + Lmap_sig.S with type v = V.t and type widen_hint_base = V.numerical_widen_hint and type offsetmap = Offsetmap.t diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.ml b/src/kernel_services/abstract_interp/lmap_bitwise.ml index dd2baf8560700ee1aa70690f7ad1e74b3a9a380b..0007c6841ad5ed14e72004d3033930d034a6732b 100644 --- a/src/kernel_services/abstract_interp/lmap_bitwise.ml +++ b/src/kernel_services/abstract_interp/lmap_bitwise.ml @@ -37,7 +37,7 @@ module type Location_map_bitwise = sig include Lattice_type.With_Top with type t := t module LOffset : - module type of Offsetmap_bitwise_sig + Offsetmap_bitwise_sig.S with type v = v and type intervals = Int_Intervals.t diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.mli b/src/kernel_services/abstract_interp/lmap_bitwise.mli index 629b07a4179465002fd50ca9b1240fd699e73e29..8c07c548122c7aa1df58784703e2dc264da4aa94 100644 --- a/src/kernel_services/abstract_interp/lmap_bitwise.mli +++ b/src/kernel_services/abstract_interp/lmap_bitwise.mli @@ -40,7 +40,7 @@ module type Location_map_bitwise = sig include Lattice_type.With_Top with type t := t module LOffset : - module type of Offsetmap_bitwise_sig + Offsetmap_bitwise_sig.S with type v = v and type intervals = Int_Intervals.t diff --git a/src/kernel_services/abstract_interp/lmap_sig.mli b/src/kernel_services/abstract_interp/lmap_sig.ml similarity index 99% rename from src/kernel_services/abstract_interp/lmap_sig.mli rename to src/kernel_services/abstract_interp/lmap_sig.ml index 1640a2a118ad2af338051298658abebb23921f8d..de556ea7769e90e3811f01f170548f3f49c1f60b 100644 --- a/src/kernel_services/abstract_interp/lmap_sig.mli +++ b/src/kernel_services/abstract_interp/lmap_sig.ml @@ -25,6 +25,8 @@ open Locations +module type S = sig + type v (** type of the values associated to a location *) type offsetmap (** type of the maps associated to a base *) type widen_hint_base (** widening hints for each base *) @@ -32,6 +34,7 @@ type widen_hint_base (** widening hints for each base *) type map (** Maps from {!Base.t} to {!offsetmap} *) type lmap = private Bottom | Top | Map of map + include Datatype.S_with_collections with type t = lmap val pretty: Format.formatter -> t -> unit @@ -204,6 +207,7 @@ val equal_subtree : subtree -> subtree -> bool exception Found_prefix of Hptmap.prefix * subtree * subtree +end diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml index e3c5c99c8db5ef823e98341d23bceef3eec40262..8421d01cc1b1adb0be7027ca6df26e9c23f5a965 100644 --- a/src/kernel_services/abstract_interp/offsetmap.ml +++ b/src/kernel_services/abstract_interp/offsetmap.ml @@ -103,7 +103,7 @@ let get_plevel () = !plevel let debug = false -module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct +module Make (V : Offsetmap_lattice_with_isotropy.S) = struct open Format @@ -3028,8 +3028,8 @@ end the warning about unused modules. *) module Aux - (V1 : module type of Offsetmap_lattice_with_isotropy) - (V2 : module type of Offsetmap_lattice_with_isotropy) + (V1 : Offsetmap_lattice_with_isotropy.S) + (V2 : Offsetmap_lattice_with_isotropy.S) = struct module M1 = Make(V1) diff --git a/src/kernel_services/abstract_interp/offsetmap.mli b/src/kernel_services/abstract_interp/offsetmap.mli index 279e77e49d1ff0fbc2271e0f3ecdbd7c4581f381..fdc1110d7570283c1bea135799bcf1e0c16576d2 100644 --- a/src/kernel_services/abstract_interp/offsetmap.mli +++ b/src/kernel_services/abstract_interp/offsetmap.mli @@ -24,14 +24,14 @@ (** Maps from intervals to values. The documentation of the returned maps is in module {!Offsetmap_sig}. *) -module Make (V : module type of Offsetmap_lattice_with_isotropy) : - module type of Offsetmap_sig +module Make (V : Offsetmap_lattice_with_isotropy.S) : + Offsetmap_sig.S with type v = V.t and type widen_hint = V.numerical_widen_hint (**/**) (* Exported as Int_Intervals, do not use this module directly *) -module Int_Intervals: module type of Int_Intervals_sig +module Int_Intervals: Int_Intervals_sig.S (**/**) @@ -42,7 +42,7 @@ module Make_bitwise(V: sig include Lattice_type.With_Narrow with type t := t include Lattice_type.With_Top with type t := t end) : - module type of Offsetmap_bitwise_sig + Offsetmap_bitwise_sig.S with type v = V.t and type intervals = Int_Intervals.t diff --git a/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli b/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml similarity index 99% rename from src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli rename to src/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml index 2ce217401450dd018cebb554763d54d0628c4d0c..86abd55e85654e478fd7a031ef7fd15d69f652a9 100644 --- a/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli +++ b/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml @@ -29,7 +29,7 @@ retrieve a more precise value, you must use the {!Offsetmap} module instead. *) - +module type S = sig type v (** Type of the values stored in the offsetmap *) include Datatype.S (** Datatype for the offsetmap *) @@ -158,3 +158,5 @@ val clear_caches: unit -> unit (**/**) val imprecise_write_msg: string ref + +end diff --git a/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli b/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.ml similarity index 99% rename from src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli rename to src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.ml index e23e62dfd81d74b44da8a4cb9a4f342d12c29b1c..2945813a4dd2d4201eb90b8687aa60580c90c31f 100644 --- a/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli +++ b/src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.ml @@ -24,6 +24,8 @@ open Lattice_type +module type S = sig + type numerical_widen_hint type size_widen_hint = Integer.t @@ -92,6 +94,7 @@ val anisotropic_cast : size:Integer.t -> t -> t assumption that it fits in [size] bits. Returning the value argument is alwas correct. *) +end (* Local Variables: diff --git a/src/kernel_services/abstract_interp/offsetmap_sig.mli b/src/kernel_services/abstract_interp/offsetmap_sig.ml similarity index 99% rename from src/kernel_services/abstract_interp/offsetmap_sig.mli rename to src/kernel_services/abstract_interp/offsetmap_sig.ml index 9c434b5a7d6bff96bd6d268946ab171da2628593..788f8d12242014934bc8c30bcaf6a9e8622b16db 100644 --- a/src/kernel_services/abstract_interp/offsetmap_sig.mli +++ b/src/kernel_services/abstract_interp/offsetmap_sig.ml @@ -27,6 +27,8 @@ open Abstract_interp +module type S = sig + type v (** Type of the values stored in the offsetmap *) type widen_hint include Datatype.S (** Datatype for the offsetmaps *) @@ -291,6 +293,8 @@ val clear_caches: unit -> unit val pretty_debug: t Pretty_utils.formatter +end + (* Local Variables: compile-command: "make -C ../../.." diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.ml similarity index 100% rename from src/kernel_services/ast_data/cil_types.mli rename to src/kernel_services/ast_data/cil_types.ml diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.ml similarity index 100% rename from src/kernel_services/ast_printing/printer_api.mli rename to src/kernel_services/ast_printing/printer_api.ml diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index 319f65e11a927a36afa0fcaff587ae6524aa7a0e..97264eb5a3c3cd16ee95cdfc57aa8a97b6e57a20 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -1675,7 +1675,7 @@ let init_from_cmdline () = Project.set_current prj2; end; let files = Kernel.Files.get () in - if files = [] && not !Fc_config.is_gui then Kernel.warning "no input file."; + if files = [] && not Fc_config.is_gui then Kernel.warning "no input file."; let files = List.map (fun f -> from_filename f) files in try init_from_c_files files; diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml index 808046e9e9180b7639fc2a73fe8091dfd354cae5..f3210b908e38ed557bf9ad55338e63c00aef6586 100644 --- a/src/kernel_services/cmdline_parameters/cmdline.ml +++ b/src/kernel_services/cmdline_parameters/cmdline.ml @@ -71,7 +71,7 @@ module Kernel_log = let dkey = Kernel_log.register_category "cmdline" let quiet_ref = ref false -let journal_enable_ref = ref !Fc_config.is_gui +let journal_enable_ref = ref Fc_config.is_gui let journal_isset_ref = ref false let use_obj_ref = ref true let use_type_ref = ref true @@ -87,7 +87,7 @@ let long_plugin_name s = if s = Log.kernel_label_name then "Frama-C" else "Plug-in " ^ s let additional_info () = - if !Fc_config.is_gui then + if Fc_config.is_gui then "\nReverting to previous state.\n\ Check the Console tab for additional information." else diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli index db33fb745847cabe9fa7b88dc972026eb8f64eaa..e90f49af9605d478eeadf0a6fc519e3423aabdc7 100644 --- a/src/kernel_services/cmdline_parameters/cmdline.mli +++ b/src/kernel_services/cmdline_parameters/cmdline.mli @@ -227,7 +227,7 @@ val nb_given_options: unit -> int Should not be called before the end of the command line parsing. @since Beryllium-20090601-beta1 *) -val use_cmdline_files: (Datatype.Filepath.t list -> unit) -> unit +val use_cmdline_files: (Filepath.Normalized.t list -> unit) -> unit (** What to do with the list of files put on the command lines. @since Beryllium-20090601-beta1 *) diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.ml similarity index 100% rename from src/kernel_services/cmdline_parameters/parameter_sig.mli rename to src/kernel_services/cmdline_parameters/parameter_sig.ml diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.ml similarity index 100% rename from src/kernel_services/parsetree/logic_ptree.mli rename to src/kernel_services/parsetree/logic_ptree.ml diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml index 8d52b20163f8efcb9f77d1deb3fe64a445a5d7e4..f66cdfea26159397015ca5e3e9f46690079d38e8 100644 --- a/src/kernel_services/plugin_entry_points/dynamic.ml +++ b/src/kernel_services/plugin_entry_points/dynamic.ml @@ -122,133 +122,25 @@ let is_object base = (* --- Package Loading --- *) (* -------------------------------------------------------------------------- *) -let packages = Hashtbl.create 64 - -let () = List.iter (fun p -> Hashtbl.add packages p ()) ("frama-c.kernel"::Fc_config.library_names) - -let missing pkg = not (Hashtbl.mem packages pkg) - -let once pkg = - if Hashtbl.mem packages pkg then false - else ( Hashtbl.add packages pkg () ; true ) - -exception ArchiveError of string - -let load_archive pkg base file = - let path = - try Findlib.resolve_path ~base file - with Not_found -> - let msg = Printf.sprintf "archive '%s' not found in '%s'" file base in - raise (ArchiveError msg) - in dynlib_module pkg path - -let mem_package pkg = - try ignore (Findlib.package_directory pkg) ; true - with Findlib.No_such_package _ -> false - -let is_virtual pkg = - try ignore (Findlib.package_property [] pkg "archive") ; false - with Not_found -> true - let load_packages pkgs = - Klog.debug ~dkey "trying to load %a" - (Pretty_utils.pp_list ~sep:"@, " Format.pp_print_string) pkgs; - try - let pkgs = List.filter missing pkgs in - List.iter - begin fun pkg -> - if once pkg then - let base = Findlib.package_directory pkg in - (* The way plugins are specified in META have been - normalized late. So people started to - specified it in different ways: - - archive(byte,plugin) - - archive(byte) - - archive(native,plugin) - - archive(plugin) - - The normalized one are: - - plugin(byte) - - plugin(native) - *) - let gui = if !Fc_config.is_gui then ["gui"] else [] in - let predicates = - (** The order is important for the archive cases *) - if Dynlink.is_native then - [ - "plugin", ["native"]@gui; - "archive", ["plugin"]@gui; - "archive", ["native";"plugin"]@gui; - ] - else - [ - "plugin", ["byte"]@gui; - "archive", ["byte";"plugin"]@gui; - "archive", ["byte"]@gui; - ] - in - let rec find_package_archives = function - - (* Search by priority order *) - | (var,predicates)::others -> - begin - try Some (Findlib.package_property predicates pkg var) - with Not_found -> find_package_archives others - end - - (* Look for virtual package *) - | [] -> - if is_virtual pkg then None else - let msg = Printf.sprintf - "package '%s' doesn't contains any known \ - specification for dynamic linking" - pkg - in raise (ArchiveError msg) - - in match find_package_archives predicates with - | None -> (* virtual package *) () - | Some archive -> - let archives = split_word archive in - if archives = [] then - Klog.warning "no archive to load for package '%s'" pkg - else - List.iter (load_archive pkg base) archives - end - (Findlib.package_deep_ancestors - (if Dynlink.is_native then [ "native" ] else [ "byte" ]) - pkgs) - with - | Findlib.No_such_package(pkg,details) -> - Cmdline.add_loading_failures pkg; - Klog.error "[findlib] package '%s' not found (%s)" pkg details - | Findlib.Package_loop pkg -> - Cmdline.add_loading_failures pkg; - Klog.error "[findlib] cyclic dependencies for package '%s'" pkg - | ArchiveError msg -> - Cmdline.add_loading_failures "unknown package"; - Klog.error "[findlib] %s" msg + List.iter Dune_site_plugins.V1.load pkgs (* -------------------------------------------------------------------------- *) (* --- Load Objects --- *) (* -------------------------------------------------------------------------- *) -let load_path = ref [] (* initialized by load_modules *) - let load_script base = Klog.feedback ~dkey "compiling script '%s.ml'" base ; let cmd = Buffer.create 80 in let fmt = Format.formatter_of_buffer cmd in begin if Dynlink.is_native then - Format.fprintf fmt "%s -shared -o %S.cmxs" Fc_config.ocamlopt base + Format.fprintf fmt "ocamlfind ocamlopt -shared -o %S.cmxs" base else - Format.fprintf fmt "%s -c" Fc_config.ocamlc ; - Format.fprintf fmt - " -g %s -warn-error a -I %s" Fc_config.ocaml_wflags Fc_config.libdir ; - if !Fc_config.is_gui && Fc_config.lablgtk <> "" then - Format.fprintf fmt " -package %s" Fc_config.lablgtk; - List.iter (fun p -> Format.fprintf fmt " -I %s" p) !load_path ; - Format.fprintf fmt " %S.ml" base ; + Format.fprintf fmt "ocamlfind ocamlc -c"; + Format.fprintf fmt " -package frama-c.kernel -open Frama_c_kernel -g %s -warn-error a" Fc_config.ocaml_wflags ; + if Fc_config.is_gui then Format.pp_print_string fmt " -package lablgtk2" ; + Format.fprintf fmt " %s.ml" base ; Format.pp_print_flush fmt () ; let cmd = Buffer.contents cmd in Klog.feedback ~dkey "running '%s'" cmd ; @@ -279,44 +171,22 @@ let load_script base = let ocamlfind_path_separator = if Sys.cygwin || Sys.win32 then ";" else ":" let set_module_load_path path = - let add_dir ~user d ps = - if is_dir d then d::ps else + let check_dir ~user d = + if is_dir d then true else ( if user then Klog.warning "cannot load '%s' (not a directory)" d - ; ps ) in - Klog.debug ~dkey "plugin_dir: %s" - (String.concat ocamlfind_path_separator Fc_config.plugin_dir); - load_path := - List.fold_right (add_dir ~user:true) path - (List.fold_right (add_dir ~user:false) (Fc_config.libdir::Fc_config.plugin_dir) []); - let env_ocamlpath = - try Str.split (Str.regexp ocamlfind_path_separator) (Sys.getenv "OCAMLPATH") - with Not_found -> [] - in - let findlib_path = - String.concat ocamlfind_path_separator (!load_path@env_ocamlpath) - in - Klog.debug ~dkey "setting findlib path to %s" findlib_path; - Findlib.init ~env_ocamlpath:findlib_path () + ; false ) in + let paths = + [List.filter (check_dir ~user:true) path; + (if Fc_config.is_gui then Config_data.Plugins.Plugins_gui.paths else []); + Config_data.Plugins.Plugins.paths] in + let ocamlpath = (String.concat ":" (List.flatten paths)) in + (* Unix.putenv "OCAMLPATH" ocamlpath; (\* for script *\) *) + Klog.debug ~dkey "setting findlib path to %s" ocamlpath + (* Config_data.Plugins.Plugins. .init paths () *) let load_plugin_path () = - let scan_directory pkgs dir = - Klog.feedback ~dkey "Loading directory '%s'" dir ; - try - let content = Sys.readdir dir in - Array.sort String.compare content ; - Array.iter - (fun name -> - if is_meta name then - (* name starts with "META.frama-c-" *) - let pkg = String.sub name 5 (String.length name - 5) in - pkgs := pkg :: !pkgs - ) content ; - with Sys_error error -> - Klog.error "impossible to read '%s' (%s)" dir error - in - let pkgs = ref [] in - List.iter (scan_directory pkgs) !load_path ; - load_packages (List.rev !pkgs) + if Fc_config.is_gui then Config_data.Plugins.Plugins_gui.load_all (); + Config_data.Plugins.Plugins.load_all () let load_module m = let base,ext = split_ext m in @@ -337,13 +207,12 @@ let load_module m = match is_file base ".ml" with | Some _ -> load_script base | None -> - if is_package m && mem_package m then load_packages [m] + if is_package m then load_packages [m] else let fc = "frama-c-" ^ String.lowercase_ascii m in - if mem_package fc then load_packages [fc] - else Klog.error "package or module '%s' not found" m + load_packages [fc] end | _ -> Klog.error "don't know what to do with '%s' (unexpected %s)" m ext diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 0d5cfc8f14bd3213c0d186142b7ed97f41605dd9..be9e4b003541e6de9630fbbb02d6ff64740e5e5c 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -639,8 +639,8 @@ module PrintLibc = let option_name = "-print-libc" let help = "when pretty-printing C code, keep prototypes coming \ from Frama-C standard library" - let default = !Fc_config.is_gui (* always print by default on the GUI *) - end) + let default = Fc_config.is_gui (* always print by default on the GUI *) + end) let () = Parameter_customize.set_group inout_source module PrintReturn = diff --git a/src/libraries/datatype/unmarshal_hashtbl_test.ml b/src/libraries/datatype/tests/unmarshal_hashtbl_test.ml similarity index 100% rename from src/libraries/datatype/unmarshal_hashtbl_test.ml rename to src/libraries/datatype/tests/unmarshal_hashtbl_test.ml diff --git a/src/libraries/datatype/unmarshal_test.ml b/src/libraries/datatype/tests/unmarshal_test.ml similarity index 100% rename from src/libraries/datatype/unmarshal_test.ml rename to src/libraries/datatype/tests/unmarshal_test.ml diff --git a/src/libraries/utils/command.ml b/src/libraries/utils/command.ml index 22ab26bbb6a8c694c5244c66eb5762068ce9e68d..45ee755a10e886ebedb484f8ee313e72f0f19ffb 100644 --- a/src/libraries/utils/command.ml +++ b/src/libraries/utils/command.ml @@ -238,7 +238,7 @@ let command_async ?stdout ?stderr cmd args = command_generic ~async:true ?stdout ?stderr cmd args let command ?(timeout=0) ?stdout ?stderr cmd args = - if !Fc_config.is_gui || timeout > 0 then + if Fc_config.is_gui || timeout > 0 then let f = command_generic ~async:true ?stdout ?stderr cmd args in let res = ref(Unix.WEXITED 99) in let ftimeout = float_of_int timeout in diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml index 4e5a859748ce24d79b52a441a180bfe9b23d351f..b408b1729b19bcbca0402b0639e0031a6ffaba1a 100644 --- a/src/libraries/utils/filepath.ml +++ b/src/libraries/utils/filepath.ml @@ -265,6 +265,20 @@ type position = let pp_pos fmt pos = Format.fprintf fmt "%a:%d" Normalized.pretty pos.pos_path pos.pos_lnum +(** Initialize using Config *) +let add_symbolic_dir_list name = function + | [d] -> add_symbolic_dir name d + | ds -> + List.iteri + (fun i d -> + let path = Printf.sprintf "%s#%d" name (succ i) in + add_symbolic_dir path d) + ds + +let () = add_symbolic_dir_list "FRAMAC_SHARE" Fc_config.datadirs +let () = add_symbolic_dir_list "FRAMAC_PLUGIN" Fc_config.plugin_dir + + (* Local Variables: compile-command: "make -C ../../.." diff --git a/src/libraries/utils/hptmap_sig.mli b/src/libraries/utils/hptmap_sig.ml similarity index 100% rename from src/libraries/utils/hptmap_sig.mli rename to src/libraries/utils/hptmap_sig.ml diff --git a/src/plugins/aorai/Aorai.mli b/src/plugins/aorai/Aorai.ml similarity index 100% rename from src/plugins/aorai/Aorai.mli rename to src/plugins/aorai/Aorai.ml diff --git a/src/plugins/aorai/dune b/src/plugins/aorai/dune new file mode 100644 index 0000000000000000000000000000000000000000..b1073c1cbd487930474de3de9388046a8a6a02b0 --- /dev/null +++ b/src/plugins/aorai/dune @@ -0,0 +1,11 @@ +( library + (name aorai) + (public_name frama-c-aorai.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(ocamllex promelalexer_withexps promelalexer ltllexer yalexer) +(ocamlyacc promelaparser_withexps promelaparser ltlparser yaparser) + +(plugin (name frama-c-plugins-aorai) (libraries frama-c-aorai.core) (site (frama-c plugins))) diff --git a/src/plugins/aorai/dune-project b/src/plugins/aorai/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..45f8b203b1705682f01b875ca7ac91efabbe6d4c --- /dev/null +++ b/src/plugins/aorai/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-aorai) +(using dune_site 0.1) diff --git a/src/plugins/aorai/frama-c-aorai.opam b/src/plugins/aorai/frama-c-aorai.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/aorai/ltlast.mli b/src/plugins/aorai/ltlast.ml similarity index 100% rename from src/plugins/aorai/ltlast.mli rename to src/plugins/aorai/ltlast.ml diff --git a/src/plugins/aorai/promelaast.mli b/src/plugins/aorai/promelaast.ml similarity index 100% rename from src/plugins/aorai/promelaast.mli rename to src/plugins/aorai/promelaast.ml diff --git a/src/plugins/callgraph/callgraph.ml b/src/plugins/callgraph/callgraph.ml new file mode 100644 index 0000000000000000000000000000000000000000..56583de47481196ebd344088a4fbf0214c35ac27 --- /dev/null +++ b/src/plugins/callgraph/callgraph.ml @@ -0,0 +1,26 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2017 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +module Options = Options +module Cg = Cg +module Services = Services +module Uses = Uses diff --git a/src/plugins/callgraph/Callgraph.mli b/src/plugins/callgraph/callgraph.mli similarity index 87% rename from src/plugins/callgraph/Callgraph.mli rename to src/plugins/callgraph/callgraph.mli index 4a66ce06fe873d435c5f32c4b8e971acddca9fd5..223acbd678d5413a702d2b0016336b986e4ac4ef 100644 --- a/src/plugins/callgraph/Callgraph.mli +++ b/src/plugins/callgraph/callgraph.mli @@ -22,13 +22,15 @@ (** Callgraph plugin. *) -module Options: sig - module Filename: Parameter_sig.String - module Service_roots: Parameter_sig.Kernel_function_set - module Uncalled: Parameter_sig.Bool - module Uncalled_leaf: Parameter_sig.Bool - module Services: Parameter_sig.Bool -end +module Options: module type of Options + +(* sig + * module Filename: Parameter_sig.String + * module Service_roots: Parameter_sig.Kernel_function_set + * module Uncalled: Parameter_sig.Bool + * module Uncalled_leaf: Parameter_sig.Bool + * module Services: Parameter_sig.Bool + * end *) module Cg: module type of Cg (** The callgraph itself *) diff --git a/src/plugins/callgraph/callgraph_api.mli b/src/plugins/callgraph/callgraph_api.ml similarity index 100% rename from src/plugins/callgraph/callgraph_api.mli rename to src/plugins/callgraph/callgraph_api.ml diff --git a/src/plugins/callgraph/dune b/src/plugins/callgraph/dune new file mode 100644 index 0000000000000000000000000000000000000000..e491ec6eb5d0c590f079702bfdeaaf180e481fb5 --- /dev/null +++ b/src/plugins/callgraph/dune @@ -0,0 +1,22 @@ +( library + (name callgraph) + (public_name frama-c-callgraph.core) + (modules Options Journalize Cg Services Uses Register Callgraph_api Callgraph Subgraph) +; (private_modules Options Journalize Cg Uses Register) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-callgraph) (libraries frama-c-callgraph.core) (site (frama-c plugins))) + +( library + (name callgraph_gui) + (public_name frama-c-callgraph.gui) + (optional) + (modules Cg_viewer) +; (private_modules Cg_viewer) + (flags -open Frama_c_kernel -open Frama_c_gui -open Callgraph) + (libraries callgraph frama-c.kernel frama-c.gui) +) + +(plugin (name frama-c-plugins-callgraph) (libraries frama-c-callgraph.gui) (site (frama-c plugins_gui))) diff --git a/src/plugins/callgraph/dune-project b/src/plugins/callgraph/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..4e8bcc33115d77c6bc2303c0d4a165e413d2367e --- /dev/null +++ b/src/plugins/callgraph/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-callgraph) +(using dune_site 0.1) diff --git a/src/plugins/callgraph/frama-c-callgraph.opam b/src/plugins/callgraph/frama-c-callgraph.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/callgraph/services.ml b/src/plugins/callgraph/services.ml index b283fbfc36e7628ae301b12ccb07e2e7dc364c76..4ab403c6ffcc33536f8aaed468b775b00aec1180 100644 --- a/src/plugins/callgraph/services.ml +++ b/src/plugins/callgraph/services.ml @@ -20,6 +20,8 @@ (* *) (**************************************************************************) +module type S = Graph.Graphviz.GraphWithDotAttrs + let initial_service_roots cg = let roots = Options.Service_roots.get () in let roots = diff --git a/src/plugins/constant_propagation/Constant_Propagation.mli b/src/plugins/constant_propagation/Constant_Propagation.ml similarity index 99% rename from src/plugins/constant_propagation/Constant_Propagation.mli rename to src/plugins/constant_propagation/Constant_Propagation.ml index b34db0dbfe1d4e2105a0b1bbae7f1b86dd74b4c9..4d73c5252a018229da633b4cd8aa706fdf3ee205 100644 --- a/src/plugins/constant_propagation/Constant_Propagation.mli +++ b/src/plugins/constant_propagation/Constant_Propagation.ml @@ -38,4 +38,4 @@ module Api : sig val self: State.t (** Internal state of the constant propagation plugin. *) -end +end = Api diff --git a/src/plugins/constant_propagation/dune b/src/plugins/constant_propagation/dune new file mode 100644 index 0000000000000000000000000000000000000000..d30cb23a713ecb602462cfdc6996e326111ab967 --- /dev/null +++ b/src/plugins/constant_propagation/dune @@ -0,0 +1,8 @@ +( library + (name constant_propagation) + (public_name frama-c-constant_propagation.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-constant_propagation) (libraries frama-c-constant_propagation.core) (site (frama-c plugins))) diff --git a/src/plugins/constant_propagation/dune-project b/src/plugins/constant_propagation/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..127ff0753d25b22a20e55b8ad07e71844d0e6c14 --- /dev/null +++ b/src/plugins/constant_propagation/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-constant_propagation) +(using dune_site 0.1) diff --git a/src/plugins/constant_propagation/frama-c-constant_propagation.opam b/src/plugins/constant_propagation/frama-c-constant_propagation.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/dive/Dive.mli b/src/plugins/dive/Dive.ml similarity index 100% rename from src/plugins/dive/Dive.mli rename to src/plugins/dive/Dive.ml diff --git a/src/plugins/dive/dive_types.mli b/src/plugins/dive/dive_types.ml similarity index 100% rename from src/plugins/dive/dive_types.mli rename to src/plugins/dive/dive_types.ml diff --git a/src/plugins/dive/dune b/src/plugins/dive/dune new file mode 100644 index 0000000000000000000000000000000000000000..cc86e48cebdd17851e7edeb1da5014bae4cd2d78 --- /dev/null +++ b/src/plugins/dive/dune @@ -0,0 +1,8 @@ +( library + (name dive) + (public_name frama-c-dive.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel frama-c-studia.core frama-c-server.core) +) + +(plugin (name frama-c-plugins-dive) (libraries frama-c-dive.core) (site (frama-c plugins))) diff --git a/src/plugins/dive/dune-project b/src/plugins/dive/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..6ee3b0f0e6f41581bc6808e787c20431e1a020c4 --- /dev/null +++ b/src/plugins/dive/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-dive) +(using dune_site 0.1) diff --git a/src/plugins/dive/frama-c-dive.opam b/src/plugins/dive/frama-c-dive.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.ml similarity index 98% rename from src/plugins/e-acsl/E_ACSL.mli rename to src/plugins/e-acsl/E_ACSL.ml index f6304d722fd813a62af1879555e4b5c8b1af2bae..9b1aebd33a7832ca9946de458d313ed0fcfca0a8 100644 --- a/src/plugins/e-acsl/E_ACSL.mli +++ b/src/plugins/e-acsl/E_ACSL.ml @@ -27,7 +27,7 @@ open Cil_types module Error: sig exception Typing_error of string exception Not_yet of string -end +end = Error module Translate: sig exception No_simple_translation of term @@ -37,7 +37,7 @@ module Translate: sig @raise Not_yet when the given term contains an unsupported construct. @raise No_simple_translation when the given term cannot be translated into a single expression. *) -end +end = Translate module Functions: sig module RTL: sig @@ -45,7 +45,7 @@ module Functions: sig (** @return [true] if the prefix of the given name indicates that it has been generated by E-ACSL instrumentation (see [mk_gen_name] function). *) end -end +end = Functions (** No function is directly exported: they are dynamically registered. *) diff --git a/src/plugins/e-acsl/dune b/src/plugins/e-acsl/dune new file mode 100644 index 0000000000000000000000000000000000000000..f61d74412ed9268c383dcd5bbb79266d77e1c0a3 --- /dev/null +++ b/src/plugins/e-acsl/dune @@ -0,0 +1,14 @@ +( library + (name eacsl) + (public_name frama-c-e-acsl.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-e-acsl) (libraries frama-c-e-acsl.core) (site (frama-c plugins))) + +(copy_files# src/*.ml*) +(copy_files# src/analyses/*.ml*) +(copy_files# src/code_generator/*.ml*) +(copy_files# src/libraries/*.ml*) +(copy_files# src/project_initializer/*.ml*) diff --git a/src/plugins/e-acsl/dune-project b/src/plugins/e-acsl/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..493dd54d16739b2a83b6b59668df331c897f2a35 --- /dev/null +++ b/src/plugins/e-acsl/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-e-acsl) +(using dune_site 0.1) diff --git a/src/plugins/e-acsl/frama-c-e-acsl.opam b/src/plugins/e-acsl/frama-c-e-acsl.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/src/local_config.ml b/src/plugins/e-acsl/src/local_config.ml new file mode 100644 index 0000000000000000000000000000000000000000..23bb44a71030a2dd8cb85b358dfe3370346a739c --- /dev/null +++ b/src/plugins/e-acsl/src/local_config.ml @@ -0,0 +1 @@ +let version = "todo" diff --git a/src/plugins/from/From.mli b/src/plugins/from/From.mli.bak similarity index 100% rename from src/plugins/from/From.mli rename to src/plugins/from/From.mli.bak diff --git a/src/plugins/from/dune b/src/plugins/from/dune new file mode 100644 index 0000000000000000000000000000000000000000..3bdf9591656387ee1c429aa43e3c3dc0767e7cf2 --- /dev/null +++ b/src/plugins/from/dune @@ -0,0 +1,8 @@ +( library + (name from) + (public_name frama-c-from.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel frama-c-callgraph.core frama-c-eva.core frama-c-postdominators.core) +) + +(plugin (name frama-c-plugins-from) (libraries frama-c-from.core) (site (frama-c plugins))) diff --git a/src/plugins/from/dune-project b/src/plugins/from/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..87efda35afc655e0bfb8247b63eec166fbcf074c --- /dev/null +++ b/src/plugins/from/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-from) +(using dune_site 0.1) diff --git a/src/plugins/from/frama-c-from.opam b/src/plugins/from/frama-c-from.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/from/gui/dune b/src/plugins/from/gui/dune new file mode 100644 index 0000000000000000000000000000000000000000..3a5e21cae6862f0b6a3e8e7b6ea09b81513b2eae --- /dev/null +++ b/src/plugins/from/gui/dune @@ -0,0 +1,7 @@ +( library + (name from_gui) + (public_name frama-c-from.gui) + (optional) + (flags -open Frama_c_kernel -open Frama_c_gui) + (libraries frama-c.kernel frama-c.gui frama-c-from.core) +) diff --git a/src/plugins/from/from_register_gui.ml b/src/plugins/from/gui/from_register_gui.ml similarity index 100% rename from src/plugins/from/from_register_gui.ml rename to src/plugins/from/gui/from_register_gui.ml diff --git a/src/plugins/from/from_register_gui.mli b/src/plugins/from/gui/from_register_gui.mli similarity index 100% rename from src/plugins/from/from_register_gui.mli rename to src/plugins/from/gui/from_register_gui.mli diff --git a/src/plugins/gui/GSourceView2.ml.in b/src/plugins/gui/GSourceView.2.ml similarity index 100% rename from src/plugins/gui/GSourceView2.ml.in rename to src/plugins/gui/GSourceView.2.ml diff --git a/src/plugins/gui/GSourceView2.mli.in b/src/plugins/gui/GSourceView.2.mli similarity index 100% rename from src/plugins/gui/GSourceView2.mli.in rename to src/plugins/gui/GSourceView.2.mli diff --git a/src/plugins/gui/GSourceView3.ml.in b/src/plugins/gui/GSourceView.3.ml similarity index 100% rename from src/plugins/gui/GSourceView3.ml.in rename to src/plugins/gui/GSourceView.3.ml diff --git a/src/plugins/gui/GSourceView3.mli.in b/src/plugins/gui/GSourceView.3.mli similarity index 100% rename from src/plugins/gui/GSourceView3.mli.in rename to src/plugins/gui/GSourceView.3.mli diff --git a/src/plugins/gui/dune b/src/plugins/gui/dune new file mode 100644 index 0000000000000000000000000000000000000000..7cb1ff502e0dab6277a2db8ee4c322127474d52f --- /dev/null +++ b/src/plugins/gui/dune @@ -0,0 +1,41 @@ +( library + (name frama_c_gui) + (public_name frama-c.gui) + (optional) + (modules + wutil wutil_once widget wbox wfile wpane wpalette wtext wtable + gui_parameters + gtk_helper gtk_form + source_viewer pretty_source source_manager book_manager + warning_manager + filetree + launcher + menu_manager + history + gui_printers + design + analyses_manager file_manager project_manager debug_manager + help_manager + property_navigator GSourceView gtk_compat + dgraph_helper +) + (flags -open Frama_c_kernel -linkall) + (libraries frama-c.init.gui frama-c.kernel ocamlgraph.dgraph + (select gtk_compat.ml from + (lablgtk2 lablgtk2.gnomecanvas lablgtk2.sourceview2 -> gtk_compat.2.ml) + (lablgtk3 lablgtk3-sourceview3 -> gtk_compat.3.ml) + ) + (select GSourceView.ml from + (lablgtk2 lablgtk2.gnomecanvas lablgtk2.sourceview2 -> GSourceView.2.ml) + (lablgtk3 lablgtk3-sourceview3 -> GSourceView.3.ml) + ) + (select GSourceView.mli from + (lablgtk2 lablgtk2.gnomecanvas lablgtk2.sourceview2 -> GSourceView.2.mli) + (lablgtk3 lablgtk3-sourceview3 -> GSourceView.3.mli) + ) + (select dgraph_helper.ml from + (dgraph -> dgraph_helper.yes.ml) + ( -> dgraph_helper.no.ml) + ) +) +) diff --git a/src/plugins/impact/Impact.mli b/src/plugins/impact/Impact.ml.bak similarity index 99% rename from src/plugins/impact/Impact.mli rename to src/plugins/impact/Impact.ml.bak index d94e6cc32600611eb6e7fc8b79c3dbf0bd905941..b88fb122270fee4aee8f258c36007b79b7000192 100644 --- a/src/plugins/impact/Impact.mli +++ b/src/plugins/impact/Impact.ml.bak @@ -40,4 +40,4 @@ module Register : sig (** Compute the impact analysis of the given set of PDG nodes, that come from the given function. @return the impacted nodes *) -end +end = Register diff --git a/src/plugins/impact/dune b/src/plugins/impact/dune new file mode 100644 index 0000000000000000000000000000000000000000..e4b26bb7b4642f3402d63467b56def937183129e --- /dev/null +++ b/src/plugins/impact/dune @@ -0,0 +1,8 @@ +( library + (name impact) + (public_name frama-c-impact.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel frama-c-slicing.core frama-c-callgraph.core frama-c-inout.core) +) + +(plugin (name frama-c-plugins-impact) (libraries frama-c-impact.core) (site (frama-c plugins))) diff --git a/src/plugins/impact/dune-project b/src/plugins/impact/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..5b7ebfaf8048d162d2437516c11abec4104393c1 --- /dev/null +++ b/src/plugins/impact/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-impact) +(using dune_site 0.1) diff --git a/src/plugins/impact/frama-c-impact.opam b/src/plugins/impact/frama-c-impact.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/impact/gui/dune b/src/plugins/impact/gui/dune new file mode 100644 index 0000000000000000000000000000000000000000..8a0f675048f4380dd1bc70109747f8abefd91405 --- /dev/null +++ b/src/plugins/impact/gui/dune @@ -0,0 +1,7 @@ +( library + (name impact_gui) + (public_name frama-c-impact.gui) + (optional) + (flags -open Frama_c_kernel -open Frama_c_gui -open Impact) + (libraries frama-c.kernel frama-c.gui frama-c-impact.core frama-c-slicing.core frama-c-callgraph.core) +) diff --git a/src/plugins/impact/register_gui.ml b/src/plugins/impact/gui/register_gui.ml similarity index 100% rename from src/plugins/impact/register_gui.ml rename to src/plugins/impact/gui/register_gui.ml diff --git a/src/plugins/impact/register_gui.mli b/src/plugins/impact/gui/register_gui.mli similarity index 100% rename from src/plugins/impact/register_gui.mli rename to src/plugins/impact/gui/register_gui.mli diff --git a/src/plugins/inout/Inout.mli b/src/plugins/inout/Inout.mli.bak similarity index 100% rename from src/plugins/inout/Inout.mli rename to src/plugins/inout/Inout.mli.bak diff --git a/src/plugins/inout/context.mli b/src/plugins/inout/context.ml similarity index 98% rename from src/plugins/inout/context.mli rename to src/plugins/inout/context.ml index 1fd2ec53d676c7eabcf967ca0e8f594b9a851d3d..13a1811ee55e4ae11a75f0fa637006efbb1bfdb5 100644 --- a/src/plugins/inout/context.mli +++ b/src/plugins/inout/context.ml @@ -20,8 +20,10 @@ (* *) (**************************************************************************) +module type S = sig val pretty_internal: Format.formatter -> Cil_types.kernel_function -> unit val pretty_external_with_formals: Format.formatter -> Cil_types.kernel_function -> unit +end (* Local Variables: diff --git a/src/plugins/inout/dune b/src/plugins/inout/dune new file mode 100644 index 0000000000000000000000000000000000000000..0560845e12c0d8a74f5a807767909193fda7ae47 --- /dev/null +++ b/src/plugins/inout/dune @@ -0,0 +1,8 @@ +( library + (name inout) + (public_name frama-c-inout.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel frama-c-callgraph.core frama-c-eva.core frama-c-from.core) +) + +(plugin (name frama-c-plugins-inout) (libraries frama-c-inout.core) (site (frama-c plugins))) diff --git a/src/plugins/inout/dune-project b/src/plugins/inout/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..b7e5599a94ba41393d1c608443d6316c8f912530 --- /dev/null +++ b/src/plugins/inout/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-inout) +(using dune_site 0.1) diff --git a/src/plugins/inout/frama-c-inout.opam b/src/plugins/inout/frama-c-inout.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/instantiate/Instantiate.mli b/src/plugins/instantiate/Instantiate.ml similarity index 98% rename from src/plugins/instantiate/Instantiate.mli rename to src/plugins/instantiate/Instantiate.ml index 4444dd5d95bae406b65c2def46efcd16145479da..dde264b3532b1b1ca44df0f44fe99216b6849f0c 100644 --- a/src/plugins/instantiate/Instantiate.mli +++ b/src/plugins/instantiate/Instantiate.ml @@ -91,7 +91,7 @@ module Instantiator_builder: sig *) val generate_spec: override_key -> fundec -> location -> funspec end -end +end = Instantiator_builder module Transform: sig (** Registers a new [Instantiator] to the visitor from the [Generator_sig] module @@ -99,7 +99,7 @@ module Transform: sig globally. *) val register: (module Instantiator_builder.Generator_sig) -> unit -end +end = Transform module Global_context:sig (** [get_variable name f] searches for an existing variable [name]. If this @@ -109,4 +109,4 @@ module Global_context:sig perform the registration, it will be done by the transformation. *) val get_variable: string -> (unit -> varinfo) -> varinfo -end +end = Global_context diff --git a/src/plugins/instantiate/dune b/src/plugins/instantiate/dune new file mode 100644 index 0000000000000000000000000000000000000000..959aeac29829decb29f258dcca960bc316d216d1 --- /dev/null +++ b/src/plugins/instantiate/dune @@ -0,0 +1,8 @@ +( library + (name instantiate) + (public_name frama-c-instantiate.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-instantiate) (libraries frama-c-instantiate.core) (site (frama-c plugins))) diff --git a/src/plugins/instantiate/dune-project b/src/plugins/instantiate/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..e0c6816ddba732278a0660d3552093f1976b615f --- /dev/null +++ b/src/plugins/instantiate/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-instantiate) +(using dune_site 0.1) diff --git a/src/plugins/instantiate/frama-c-instantiate.opam b/src/plugins/instantiate/frama-c-instantiate.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/loop_analysis/LoopAnalysis.ml b/src/plugins/loop_analysis/LoopAnalysis.ml new file mode 100644 index 0000000000000000000000000000000000000000..2a70c138792fa878773161d371def9ddc0c560da --- /dev/null +++ b/src/plugins/loop_analysis/LoopAnalysis.ml @@ -0,0 +1,23 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2017 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +module Loop_analysis = Loop_analysis diff --git a/src/plugins/loop_analysis/dune b/src/plugins/loop_analysis/dune new file mode 100644 index 0000000000000000000000000000000000000000..70ffc9d6371bf9fe4008cdddc6610169d5ec031b --- /dev/null +++ b/src/plugins/loop_analysis/dune @@ -0,0 +1,10 @@ +( library + (name LoopAnalysis) + (public_name frama-c-loop-analysis.core) + (modules options region_analysis_sig region_analysis region_analysis_stmt loop_analysis slevel_analysis register LoopAnalysis) + (private_modules region_analysis_sig region_analysis region_analysis_stmt loop_analysis slevel_analysis register) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-loop-analysis) (libraries frama-c-loop-analysis.core) (site (frama-c plugins))) diff --git a/src/plugins/loop_analysis/dune-project b/src/plugins/loop_analysis/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..6b271be3ec8f3e32fc9ab3f3aa55ebb46326e427 --- /dev/null +++ b/src/plugins/loop_analysis/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-loop_analysis) +(using dune_site 0.1) diff --git a/src/plugins/loop_analysis/frama-c-loop-analysis.opam b/src/plugins/loop_analysis/frama-c-loop-analysis.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/markdown-report/.gitignore b/src/plugins/markdown-report/.gitignore index 6c2faaa71d31861e38605eb6bebc51dec9a0e3da..fa7f0c4cd6963ee82502138bd0f4994ee1eab51f 100644 --- a/src/plugins/markdown-report/.gitignore +++ b/src/plugins/markdown-report/.gitignore @@ -8,7 +8,6 @@ top/ .merlin *~ /Makefile -/Markdown_report.mli /tests/ptests_config /tests/*/result /tests/*/result_* diff --git a/src/plugins/markdown-report/Mardown_report.ml b/src/plugins/markdown-report/Mardown_report.ml new file mode 100644 index 0000000000000000000000000000000000000000..b87543e2fbaba3fd935a360753c6771cfa050c08 --- /dev/null +++ b/src/plugins/markdown-report/Mardown_report.ml @@ -0,0 +1,2 @@ +module Mdr_params = Mdr_params +module Md_gen = Md_gen diff --git a/src/plugins/markdown-report/dune b/src/plugins/markdown-report/dune new file mode 100644 index 0000000000000000000000000000000000000000..18c46eaac3820d6c1dcc6f6e0e263ee7287e3c3d --- /dev/null +++ b/src/plugins/markdown-report/dune @@ -0,0 +1,10 @@ +( library + (name markdown_report) + (public_name frama-c-markdown-report.core) + (optional) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel frama-c-eva.core) + (preprocess (pps ppx_deriving_yojson)) +) + +(plugin (name frama-c-plugins-markdown-report) (libraries frama-c-markdown-report.core) (site (frama-c plugins))) diff --git a/src/plugins/markdown-report/dune-project b/src/plugins/markdown-report/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..8bbef9b0080e0e0f93044f100e2b57be65bf29ed --- /dev/null +++ b/src/plugins/markdown-report/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-markdown-report) +(using dune_site 0.1) diff --git a/src/plugins/markdown-report/frama-c-markdown-report.opam b/src/plugins/markdown-report/frama-c-markdown-report.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/metrics/Metrics.ml b/src/plugins/metrics/Metrics.ml new file mode 100644 index 0000000000000000000000000000000000000000..4e96f34677973d1764ad4a5c94d2632656118627 --- /dev/null +++ b/src/plugins/metrics/Metrics.ml @@ -0,0 +1,31 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2020 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +module Metrics_coverage = Metrics_coverage +module Metrics_base = Metrics_base +module Metrics_cilast = Metrics_cilast + +(* +Local Variables: +compile-command: "make -C ../../.." +End: +*) diff --git a/src/plugins/metrics/dune b/src/plugins/metrics/dune new file mode 100644 index 0000000000000000000000000000000000000000..3240bb3407ff88e49c9a029098a415703d21a093 --- /dev/null +++ b/src/plugins/metrics/dune @@ -0,0 +1,22 @@ +( library + (name metrics) + (public_name frama-c-metrics.core) + (modules metrics_parameters css_html metrics_base metrics_acsl + metrics_cabs metrics_cilast metrics_coverage + register) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel frama-c-eva.core) +) + +(plugin (name frama-c-plugins-metrics) (libraries frama-c-metrics.core) (site (frama-c plugins))) + +( library + (name metrics_gui) + (public_name frama-c-metrics.gui) + (optional) + (modules metrics_gui_panels register_gui) + (flags -open Frama_c_kernel -open Frama_c_gui -open Metrics) + (libraries metrics frama-c.kernel frama-c.gui) +) + +(plugin (name frama-c-plugins-metrics) (libraries frama-c-metrics.gui) (site (frama-c plugins_gui))) diff --git a/src/plugins/metrics/dune-project b/src/plugins/metrics/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..f02ee83d3d5221471c3b848ec9a72f7aa25ab4cb --- /dev/null +++ b/src/plugins/metrics/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-metrics) +(using dune_site 0.1) diff --git a/src/plugins/metrics/frama-c-metrics.opam b/src/plugins/metrics/frama-c-metrics.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/metrics/metrics_gui.ml b/src/plugins/metrics/metrics_gui_panels.ml similarity index 100% rename from src/plugins/metrics/metrics_gui.ml rename to src/plugins/metrics/metrics_gui_panels.ml diff --git a/src/plugins/metrics/metrics_gui.mli b/src/plugins/metrics/metrics_gui_panels.mli similarity index 100% rename from src/plugins/metrics/metrics_gui.mli rename to src/plugins/metrics/metrics_gui_panels.mli diff --git a/src/plugins/metrics/register_gui.ml b/src/plugins/metrics/register_gui.ml index 8674e439cd21e72d233cceeb08354ca8df2b8e26..efec0263fc675d20e7e329db4d5dea90e62ba7dd 100644 --- a/src/plugins/metrics/register_gui.ml +++ b/src/plugins/metrics/register_gui.ml @@ -54,14 +54,14 @@ module HalsteadMetricsGUI = struct ignore(GMisc.separator `HORIZONTAL ~packing:box#pack ()); let metrics = Metrics_cabs.Halstead.get_metrics () in let table_contents = Metrics_cabs.Halstead.to_list metrics in - Metrics_gui.display_as_table table_contents box + Metrics_gui_panels.display_as_table table_contents box with | Ast.NoUntypedAst -> main_ui#error "Cannot compute Halstead metrics: untyped AST not present.\n\ It has been removed either by user request or \ by some AST transformation." - let register main_ui = Metrics_gui.register_metrics name (display_result main_ui) + let register main_ui = Metrics_gui_panels.register_metrics name (display_result main_ui) end module CyclomaticMetricsGUI = struct @@ -114,7 +114,7 @@ module CyclomaticMetricsGUI = struct ["stmts analyzed";(string_of_int valeur)]; ["percentage of stmts covered"; (string_of_float percent)] ] in - Metrics_gui.display_as_table metrics_data vbox; + Metrics_gui_panels.display_as_table metrics_data vbox; let close_button = GButton.button ~stock:`OK ~packing:vbox#pack () in close_button#set_border_width 10; ignore (close_button#connect#clicked ~callback:dialog#misc#hide); @@ -145,7 +145,7 @@ module CyclomaticMetricsGUI = struct ~justify:`LEFT ~packing:vbox#pack ()); ignore(GMisc.separator `HORIZONTAL ~packing:vbox#pack ()); let metrics_data = BasicMetrics.to_list self#get_data in - Metrics_gui.display_as_table metrics_data vbox; + Metrics_gui_panels.display_as_table metrics_data vbox; let close_button = GButton.button ~stock:`OK ~packing:vbox#pack () in close_button#set_border_width 10; ignore (close_button#connect#clicked ~callback:dialog#misc#hide); @@ -204,11 +204,11 @@ module CyclomaticMetricsGUI = struct ignore(GMisc.separator `HORIZONTAL ~packing:box#pack ()); let metrics = Metrics_cilast.get_global_metrics ~libc in let table_contents = BasicMetrics.to_list metrics in - Metrics_gui.display_as_table table_contents box + Metrics_gui_panels.display_as_table table_contents box let register ~libc main_ui = ignore (new cyclo_class ~libc main_ui); - Metrics_gui.register_metrics name (display_result ~libc) + Metrics_gui_panels.register_metrics name (display_result ~libc) end (** GUI hooks value coverage *) @@ -362,16 +362,16 @@ module ValueCoverageGUI = struct Design.register_reset_extension (fun _ -> result := None); main_ui#register_source_highlighter highlighter; let apply = Metrics_parameters.ValueCoverage.get () in - Metrics_gui.register_metrics ~apply name (display_result ~libc main_ui); + Metrics_gui_panels.register_metrics ~apply name (display_result ~libc main_ui); end let register_final ?(libc=Metrics_parameters.Libc.get ()) main_ui = - let box = Metrics_gui.init_panel main_ui in - Design.register_reset_extension Metrics_gui.reset_panel; + let box = Metrics_gui_panels.init_panel main_ui in + Design.register_reset_extension Metrics_gui_panels.reset_panel; HalsteadMetricsGUI.register main_ui; CyclomaticMetricsGUI.register ~libc main_ui; ValueCoverageGUI.register ~libc main_ui; - Metrics_gui.coerce_panel_to_ui box main_ui + Metrics_gui_panels.coerce_panel_to_ui box main_ui let gui (main_ui:Design.main_window_extension_points) = main_ui#register_panel register_final diff --git a/src/plugins/nonterm/Nonterm.mli b/src/plugins/nonterm/Nonterm.ml similarity index 100% rename from src/plugins/nonterm/Nonterm.mli rename to src/plugins/nonterm/Nonterm.ml diff --git a/src/plugins/nonterm/dune b/src/plugins/nonterm/dune new file mode 100644 index 0000000000000000000000000000000000000000..78bb592a89a316a16002876c12d9746750881ea4 --- /dev/null +++ b/src/plugins/nonterm/dune @@ -0,0 +1,8 @@ +( library + (name nonterm) + (public_name frama-c-nonterm.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-nonterm) (libraries frama-c-nonterm.core) (site (frama-c plugins))) diff --git a/src/plugins/nonterm/dune-project b/src/plugins/nonterm/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..13bd116327967b565b4e9524051a2275a4ff6a0b --- /dev/null +++ b/src/plugins/nonterm/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-nonterm) +(using dune_site 0.1) diff --git a/src/plugins/nonterm/frama-c-nonterm.opam b/src/plugins/nonterm/frama-c-nonterm.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/obfuscator/Obfuscator.mli b/src/plugins/obfuscator/Obfuscator.ml similarity index 100% rename from src/plugins/obfuscator/Obfuscator.mli rename to src/plugins/obfuscator/Obfuscator.ml diff --git a/src/plugins/obfuscator/dune b/src/plugins/obfuscator/dune new file mode 100644 index 0000000000000000000000000000000000000000..6a71414de99e327169817291b7299f1e0acc5c9d --- /dev/null +++ b/src/plugins/obfuscator/dune @@ -0,0 +1,8 @@ +( library + (name obfuscator) + (public_name frama-c-obfuscator.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-obfuscator) (libraries frama-c-obfuscator.core) (site (frama-c plugins))) diff --git a/src/plugins/obfuscator/dune-project b/src/plugins/obfuscator/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..3c6f1ab3460ffe9066c52b81f76775630e802384 --- /dev/null +++ b/src/plugins/obfuscator/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-obfuscator) +(using dune_site 0.1) diff --git a/src/plugins/obfuscator/frama-c-obfuscator.opam b/src/plugins/obfuscator/frama-c-obfuscator.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/occurrence/Occurrence.mli b/src/plugins/occurrence/Occurrence.ml similarity index 99% rename from src/plugins/occurrence/Occurrence.mli rename to src/plugins/occurrence/Occurrence.ml index f34ddc18afbf5bc33113ebb00fe27659ae077706..0979ef198ac7b79952a62b53a3e2c329fbf8863d 100644 --- a/src/plugins/occurrence/Occurrence.mli +++ b/src/plugins/occurrence/Occurrence.ml @@ -35,7 +35,7 @@ module Register: sig [vi] at the position [ki]. *) val print_all: (unit -> unit) (** Print all the occurrence of each variable declarations. *) -end +end = Register (* Local Variables: diff --git a/src/plugins/occurrence/dune b/src/plugins/occurrence/dune new file mode 100644 index 0000000000000000000000000000000000000000..27e25ec02f3a1f1933bd96fe938f0a687e8fd5bc --- /dev/null +++ b/src/plugins/occurrence/dune @@ -0,0 +1,20 @@ +( library + (name occurrence) + (public_name frama-c-occurrence.core) + (modules options register) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-occurrence) (libraries frama-c-occurrence.core) (site (frama-c plugins))) + +( library + (name occurrence_gui) + (public_name frama-c-occurrence.gui) + (optional) + (modules register_gui) + (flags -open Frama_c_kernel -open Frama_c_gui -open Occurrence) + (libraries occurrence frama-c.kernel frama-c.gui) +) + +(plugin (name frama-c-plugins-occurrence) (libraries frama-c-occurrence.gui) (site (frama-c plugins_gui))) diff --git a/src/plugins/occurrence/dune-project b/src/plugins/occurrence/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..feb3ee1059b3d4e9b34fd0ea9486490f9b15c8a0 --- /dev/null +++ b/src/plugins/occurrence/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-occurrence) +(using dune_site 0.1) diff --git a/src/plugins/occurrence/frama-c-occurrence.opam b/src/plugins/occurrence/frama-c-occurrence.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/pdg/Pdg.ml b/src/plugins/pdg/Pdg.ml new file mode 100644 index 0000000000000000000000000000000000000000..95f4052f96df8cd1b0b9928a6a562d51c0e6db2d --- /dev/null +++ b/src/plugins/pdg/Pdg.ml @@ -0,0 +1,28 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2018 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +(** Program Dependences Graph. *) + +(** Functions for this plugin are registered through the [Db] module, + the dynamic API, and the module Below. *) + +module Register = Register diff --git a/src/plugins/pdg/dune b/src/plugins/pdg/dune new file mode 100644 index 0000000000000000000000000000000000000000..0ff2e85ddae88ce0412d8c7f32a91efa35b770ba --- /dev/null +++ b/src/plugins/pdg/dune @@ -0,0 +1,8 @@ +( library + (name pdg) + (public_name frama-c-pdg.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel frama-c-callgraph.core frama-c-from.core frama-c-eva.core) +) + +(plugin (name frama-c-plugins-pdg) (libraries frama-c-pdg.core) (site (frama-c plugins))) diff --git a/src/plugins/pdg/dune-project b/src/plugins/pdg/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..fabc92ddc8d80eb3b79b67a0cbfc5b83576c1b19 --- /dev/null +++ b/src/plugins/pdg/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-pdg) +(using dune_site 0.1) diff --git a/src/plugins/pdg/frama-c-pdg.opam b/src/plugins/pdg/frama-c-pdg.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/postdominators/Postdominators.mli b/src/plugins/postdominators/Postdominators.mli.bak similarity index 100% rename from src/plugins/postdominators/Postdominators.mli rename to src/plugins/postdominators/Postdominators.mli.bak diff --git a/src/plugins/postdominators/dune b/src/plugins/postdominators/dune new file mode 100644 index 0000000000000000000000000000000000000000..696623c9896bd9c2244c833de2f03d48fdb77284 --- /dev/null +++ b/src/plugins/postdominators/dune @@ -0,0 +1,8 @@ +( library + (name postdominators) + (public_name frama-c-postdominators.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-postdominators) (libraries frama-c-postdominators.core) (site (frama-c plugins))) diff --git a/src/plugins/postdominators/dune-project b/src/plugins/postdominators/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..2ba287aabf547b88afe767c83512e649c05e783f --- /dev/null +++ b/src/plugins/postdominators/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-postdominators) +(using dune_site 0.1) diff --git a/src/plugins/postdominators/frama-c-postdominators.opam b/src/plugins/postdominators/frama-c-postdominators.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/print_api/Print_api.mli b/src/plugins/print_api/Print_api.ml similarity index 100% rename from src/plugins/print_api/Print_api.mli rename to src/plugins/print_api/Print_api.ml diff --git a/src/plugins/print_api/dune b/src/plugins/print_api/dune new file mode 100644 index 0000000000000000000000000000000000000000..ad864970a02de07731d94653a24778a8076537b9 --- /dev/null +++ b/src/plugins/print_api/dune @@ -0,0 +1,8 @@ +; ( library +; (name print_api) +; (public_name frama-c-print_api.core) +; (flags -open Frama_c_kernel) +; (libraries frama-c.kernel frama-c-callgraph.core frama-c-eva.core frama-c-postdominators.core) +; ) + +; (plugin (name frama-c-plugins-print_api) (libraries frama-c-print_api.core) (site (frama-c plugins))) diff --git a/src/plugins/print_api/dune-project b/src/plugins/print_api/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..18504e0cec5cff9af3c5a7ddc6b12fdcbc615592 --- /dev/null +++ b/src/plugins/print_api/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-print_api) +(using dune_site 0.1) diff --git a/src/plugins/print_api/frama-c-print_api.opam b/src/plugins/print_api/frama-c-print_api.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/qed/bvars.mli b/src/plugins/qed/bvars.mli index 237f47314a27422978f4975611f5e2b25464bf6a..39ef5c549e5637dfb460b1caa9ec9cdb77c857ea 100644 --- a/src/plugins/qed/bvars.mli +++ b/src/plugins/qed/bvars.mli @@ -32,12 +32,17 @@ type t (** An over-approximation of set of integers *) val empty : t val singleton : int -> t -val order : t -> int (** Max stack of binders *) -val bind : t -> t (** Decrease all elements in [s] after removing [0] *) +val order : t -> int +(** Max stack of binders *) + +val bind : t -> t +(** Decrease all elements in [s] after removing [0] *) val union : t -> t -> t -val closed : t -> bool (** All variables are bound *) +val closed : t -> bool +(** All variables are bound *) + val closed_at : int -> t -> bool (** [closed_at n a] Does not contains variables [k<n] *) diff --git a/src/plugins/qed/dune b/src/plugins/qed/dune new file mode 100644 index 0000000000000000000000000000000000000000..91cf79acb486a387df6a4344a4524fe4d4fc9e07 --- /dev/null +++ b/src/plugins/qed/dune @@ -0,0 +1,6 @@ +(library + (name qed) + (public_name qed) + (flags (-open Frama_c_kernel)) + (libraries frama-c.kernel zarith) +) diff --git a/src/plugins/qed/dune-project b/src/plugins/qed/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..e6bf112d3ee7a635ebc4671612ed94e3ba8f6d87 --- /dev/null +++ b/src/plugins/qed/dune-project @@ -0,0 +1,2 @@ +(lang dune 2.8) +(name qed) diff --git a/src/plugins/qed/engine.ml b/src/plugins/qed/engine.ml index 56bd28dc69364c91ae336608193fc4e04c468b89..dceb6c0380505391c61daf079128123376b2e373 100644 --- a/src/plugins/qed/engine.ml +++ b/src/plugins/qed/engine.ml @@ -110,9 +110,15 @@ class type virtual ['z,'adt,'field,'logic,'tau,'var,'term,'env] engine = (** {3 Global and Local Environment} *) - method env : 'env (** Returns a fresh copy of the current environment. *) - method set_env : 'env -> unit (** Set environment. *) - method lookup : 'term -> scope (** Term scope in the current environment. *) + method env : 'env + (** Returns a fresh copy of the current environment. *) + + method set_env : 'env -> unit + (** Set environment. *) + + method lookup : 'term -> scope + (** Term scope in the current environment. *) + method scope : 'env -> (unit -> unit) -> unit (** Calls the continuation in the provided environment. Previous environment is restored after return. *) @@ -137,14 +143,22 @@ class type virtual ['z,'adt,'field,'logic,'tau,'var,'term,'env] engine = method t_prop : string method t_atomic : 'tau -> bool - method pp_array : 'tau printer (** For [Z->a] arrays *) - method pp_farray : 'tau printer2 (** For [k->a] arrays *) + method pp_array : 'tau printer + (** For [Z->a] arrays *) + + method pp_farray : 'tau printer2 + (** For [k->a] arrays *) + + method pp_tvar : int printer + (** Type variables. *) - method pp_tvar : int printer (** Type variables. *) method pp_datatype : 'adt -> 'tau list printer - method pp_tau : 'tau printer (** Without parentheses. *) - method pp_subtau : 'tau printer (** With parentheses if non-atomic. *) + method pp_tau : 'tau printer + (** Without parentheses. *) + + method pp_subtau : 'tau printer + (** With parentheses if non-atomic. *) (** {3 Current Mode} @@ -165,8 +179,11 @@ class type virtual ['z,'adt,'field,'logic,'tau,'var,'term,'env] engine = (** {3 Primitives} *) - method e_true : cmode -> string (** ["true"] *) - method e_false : cmode -> string (** ["false"] *) + method e_true : cmode -> string + (** ["true"] *) + + method e_false : cmode -> string + (** ["false"] *) method pp_int : amode -> 'z printer method pp_real : Q.t printer diff --git a/src/plugins/qed/export.mli b/src/plugins/qed/export.mli index cf273f58c28739e13281185b64280e531b1558ce..b529f511849950028e50b1a33f475056694d85cb 100644 --- a/src/plugins/qed/export.mli +++ b/src/plugins/qed/export.mli @@ -61,9 +61,15 @@ sig method virtual field : Field.t -> string method virtual link : Fun.t -> link - method env : Env.t (** A safe copy of the environment *) - method set_env : Env.t -> unit (** Set the environment *) - method marks : Env.t * T.marks (** The current environment with empty marks *) + method env : Env.t + (** A safe copy of the environment *) + + method set_env : Env.t -> unit + (** Set the environment *) + + method marks : Env.t * T.marks + (** The current environment with empty marks *) + method lookup : term -> scope method set_env : Env.t -> unit method scope : Env.t -> (unit -> unit) -> unit diff --git a/src/plugins/qed/hcons.mli b/src/plugins/qed/hcons.mli index 875202b1fca52bbfe60deea5896c6f6697a7e5d0..ba48048f3fa497a7a112090782f32556de6556b2 100644 --- a/src/plugins/qed/hcons.mli +++ b/src/plugins/qed/hcons.mli @@ -33,8 +33,12 @@ val hash_list : ('a -> int) -> int -> 'a list -> int val hash_array : ('a -> int) -> int -> 'a array -> int val hash_opt : ('a -> int) -> int -> 'a option -> int -val eq_list : 'a list -> 'a list -> bool (** Uses [==]. *) -val eq_array : 'a array -> 'a array -> bool (** Uses [==]. *) +val eq_list : 'a list -> 'a list -> bool +(** Uses [==]. *) + +val eq_array : 'a array -> 'a array -> bool +(** Uses [==]. *) + val equal_list : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool val equal_array : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool val compare_list : ('a -> 'a -> int) -> 'a list -> 'a list -> int diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml index e7ce8e4908713e84c148054f6bc35c04dd134517..5e55e6c4308390dc3cf71e38f469724b8b628f83 100644 --- a/src/plugins/qed/logic.ml +++ b/src/plugins/qed/logic.ml @@ -104,8 +104,11 @@ module type Function = sig include Symbol val category : t -> t category - val params : t -> sort list (** params ; exceeding params use Sdata *) - val sort : t -> sort (** result *) + val params : t -> sort list + (** params ; exceeding params use Sdata *) + + val sort : t -> sort + (** result *) end (** {2 Bound Variables} *) @@ -225,23 +228,50 @@ sig type record = (Field.t * term) list - val decide : term -> bool (** Return [true] if and only the term is [e_true]. Constant time. *) - val is_true : term -> maybe (** Constant time. *) - val is_false : term -> maybe (** Constant time. *) - val is_prop : term -> bool (** Boolean or Property *) - val is_int : term -> bool (** Integer sort *) - val is_real : term -> bool (** Real sort *) - val is_arith : term -> bool (** Integer or Real sort *) + val decide : term -> bool + (** Return [true] if and only the term is [e_true]. Constant time. *) + + val is_true : term -> maybe + (** Constant time. *) + + val is_false : term -> maybe + (** Constant time. *) + + val is_prop : term -> bool + (** Boolean or Property *) + + val is_int : term -> bool + (** Integer sort *) + + val is_real : term -> bool + (** Real sort *) + + val is_arith : term -> bool + (** Integer or Real sort *) + + val are_equal : term -> term -> maybe + (** Computes equality *) + + val eval_eq : term -> term -> bool + (** Same as [are_equal] is [Yes] *) + + val eval_neq : term -> term -> bool + (** Same as [are_equal] is [No] *) + + val eval_lt : term -> term -> bool + (** Same as [e_lt] is [e_true] *) + + val eval_leq : term -> term -> bool + (** Same as [e_leq] is [e_true] *) + + val repr : term -> repr + (** Constant time *) - val are_equal : term -> term -> maybe (** Computes equality *) - val eval_eq : term -> term -> bool (** Same as [are_equal] is [Yes] *) - val eval_neq : term -> term -> bool (** Same as [are_equal] is [No] *) - val eval_lt : term -> term -> bool (** Same as [e_lt] is [e_true] *) - val eval_leq : term -> term -> bool (** Same as [e_leq] is [e_true] *) + val sort : term -> sort + (** Constant time *) - val repr : term -> repr (** Constant time *) - val sort : term -> sort (** Constant time *) - val vars : term -> Vars.t (** Constant time *) + val vars : term -> Vars.t + (** Constant time *) (** Path-positioning access @@ -468,6 +498,7 @@ sig val consequence : term -> term -> term (** Knowing [h], [consequence h a] returns [b] such that [h -> (a<->b)] *) + val literal : term -> bool * term val affine : term -> term affine @@ -476,19 +507,36 @@ sig (** {3 Symbol} *) type t = term - val id : t -> int (** unique identifier (stored in t) *) - val hash : t -> int (** constant access (stored in t) *) - val equal : t -> t -> bool (** physical equality *) - val compare : t -> t -> int (** atoms are lower than complex terms ; otherwise, sorted by id. *) + val id : t -> int + (** unique identifier (stored in t) *) + + val hash : t -> int + (** constant access (stored in t) *) + + val equal : t -> t -> bool + (** physical equality *) + + val compare : t -> t -> int + (** atoms are lower than complex terms ; otherwise, sorted by id. *) + val pretty : Format.formatter -> t -> unit - val weigth : t -> int (** Informal size *) + val weigth : t -> int + (** Informal size *) (** {3 Utilities} *) - val is_closed : t -> bool (** No bound variables *) - val is_simple : t -> bool (** Constants, variables, functions of arity 0 *) - val is_atomic : t -> bool (** Constants and variables *) - val is_primitive : t -> bool (** Constants only *) + val is_closed : t -> bool + (** No bound variables *) + + val is_simple : t -> bool + (** Constants, variables, functions of arity 0 *) + + val is_atomic : t -> bool + (** Constants and variables *) + + val is_primitive : t -> bool + (** Constants only *) + val is_neutral : Fun.t -> t -> bool val is_absorbant : Fun.t -> t -> bool @@ -496,9 +544,14 @@ sig val basename : t -> string val debug : Format.formatter -> t -> unit - val pp_id : Format.formatter -> t -> unit (** internal id *) - val pp_rid : Format.formatter -> t -> unit (** head symbol with children id's *) - val pp_repr : Format.formatter -> repr -> unit (** head symbol with children id's *) + val pp_id : Format.formatter -> t -> unit + (** internal id *) + + val pp_rid : Format.formatter -> t -> unit + (** head symbol with children id's *) + + val pp_repr : Format.formatter -> repr -> unit + (** head symbol with children id's *) (** {2 Shared sub-terms} *) diff --git a/src/plugins/qed/pool.mli b/src/plugins/qed/pool.mli index a3821955bb19548c00e9b3436b82e6094dabf021..bcb3dfb4d3c498477b90d0e9e5bca3eebbd007de 100644 --- a/src/plugins/qed/pool.mli +++ b/src/plugins/qed/pool.mli @@ -34,7 +34,8 @@ end module Make(T : Type) : sig - type var = (** Hashconsed *) + (** Hashconsed *) + type var = private { vid : int ; vbase : string ; @@ -44,8 +45,12 @@ sig val dummy : var (** null vid *) - val hash : var -> int (** [vid] *) - val equal : var -> var -> bool (** [==] *) + val hash : var -> int + (** [vid] *) + + val equal : var -> var -> bool + (** [==] *) + val compare : var -> var -> int val pretty : Format.formatter -> var -> unit diff --git a/src/plugins/qed/qed.opam b/src/plugins/qed/qed.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/qed/term.mli b/src/plugins/qed/term.mli index 20e68173867ce13d1c70424461daf945f6ab421f..9fb199e2f177fa6e7e4c5857dbba6d7841c448f6 100644 --- a/src/plugins/qed/term.mli +++ b/src/plugins/qed/term.mli @@ -39,13 +39,20 @@ module Make (** {2 Global State} One given [term] has valid meaning only for one particular state. *) - type state (** Hash-consing, cache, rewriting rules, etc. *) + type state + (** Hash-consing, cache, rewriting rules, etc. *) + val create : unit -> state (** Create a new fresh state. Local state is not modified. *) - val get_state : unit -> state (** Return local state. *) - val set_state : state -> unit (** Update local state. *) - val clr_state : state -> unit (** Clear local state. *) + val get_state : unit -> state + (** Return local state. *) + + val set_state : state -> unit + (** Update local state. *) + + val clr_state : state -> unit + (** Clear local state. *) val in_state : state -> ('a -> 'b) -> 'a -> 'b (** execute in a particular state. *) diff --git a/src/plugins/report/Report.ml b/src/plugins/report/Report.ml new file mode 100644 index 0000000000000000000000000000000000000000..3ee1c4ee43c2e62e302add7748a7793a4d0fd25a --- /dev/null +++ b/src/plugins/report/Report.ml @@ -0,0 +1,30 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2018 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + + +module Register = Register + +(* +Local Variables: +compile-command: "make -C ../../../.." +End: +*) diff --git a/src/plugins/report/dune b/src/plugins/report/dune new file mode 100644 index 0000000000000000000000000000000000000000..a5c8e6f7f575133d649cfcb305fb5745432ac00b --- /dev/null +++ b/src/plugins/report/dune @@ -0,0 +1,10 @@ +( library + (name report) + (public_name frama-c-report.core) + (modules report_parameters scan dump csv register Report) + (private_modules report_parameters scan dump csv) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-report) (libraries frama-c-report.core) (site (frama-c plugins))) diff --git a/src/plugins/report/dune-project b/src/plugins/report/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..9a58724e2bcafa4ccb98b3239449845379163d6e --- /dev/null +++ b/src/plugins/report/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-report) +(using dune_site 0.1) diff --git a/src/plugins/report/frama-c-report.opam b/src/plugins/report/frama-c-report.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/rte/RteGen.ml b/src/plugins/rte/RteGen.ml new file mode 100644 index 0000000000000000000000000000000000000000..d4b544b52514408fc0cc781256ea5730030200d5 --- /dev/null +++ b/src/plugins/rte/RteGen.ml @@ -0,0 +1,30 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2017 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +(** Flags for filtering Alarms *) +module Flags = Flags + +(** RTE Generator Status & Emitters *) +module Generator = Generator + +(** Visitors to iterate over Alarms and/or generate Code-Annotations *) +module Visit = Visit diff --git a/src/plugins/rte/dune b/src/plugins/rte/dune new file mode 100644 index 0000000000000000000000000000000000000000..585f60e1a9690da86293277fc16c3cc206120b9a --- /dev/null +++ b/src/plugins/rte/dune @@ -0,0 +1,9 @@ +(library + (name RteGen) + (public_name frama-c-rtegen.core) + (private_modules options generator rte visit register RteGen) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-rtegen) (libraries frama-c-rtegen.core) (site (frama-c plugins))) diff --git a/src/plugins/rte/dune-project b/src/plugins/rte/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..4496af78fa42a572338b07b013b54f8fe04c9fee --- /dev/null +++ b/src/plugins/rte/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-rte) +(using dune_site 0.1) diff --git a/src/plugins/rte/frama-c-rtegen.opam b/src/plugins/rte/frama-c-rtegen.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/scope/Scope.ml b/src/plugins/scope/Scope.ml new file mode 100644 index 0000000000000000000000000000000000000000..a1460db17d5b58aeae92aecd399ca5103e224299 --- /dev/null +++ b/src/plugins/scope/Scope.ml @@ -0,0 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2019 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +module Defs = Defs +module Datascope = Datascope +module Zones = Zones diff --git a/src/plugins/scope/dune b/src/plugins/scope/dune new file mode 100644 index 0000000000000000000000000000000000000000..95bc60aace09b2299a2bd1215b3223b27ed5a6fb --- /dev/null +++ b/src/plugins/scope/dune @@ -0,0 +1,19 @@ +(library + (name Scope) + (public_name frama-c-scope.core) + (modules datascope zones defs) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(library + (name Scope_gui) + (public_name frama-c-scope.gui) + (optional) + (modules dpds_gui) + (flags -open Frama_c_kernel -open Frama_c_gui -open Scope) + (libraries frama-c.kernel frama-c.gui frama-c-scope.core) +) + +(plugin (name frama-c-plugins-scope) (libraries frama-c-scope.core) (site (frama-c plugins))) +(plugin (name frama-c-plugins-scope) (libraries frama-c-scope.gui) (site (frama-c plugins_gui))) diff --git a/src/plugins/scope/dune-project b/src/plugins/scope/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..98f1847821a675561a98e1199ccb0ba32669686f --- /dev/null +++ b/src/plugins/scope/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-scope) +(using dune_site 0.1) diff --git a/src/plugins/scope/frama-c-scope.opam b/src/plugins/scope/frama-c-scope.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/security_slicing/Security_slicing.mli b/src/plugins/security_slicing/Security_slicing.ml similarity index 100% rename from src/plugins/security_slicing/Security_slicing.mli rename to src/plugins/security_slicing/Security_slicing.ml diff --git a/src/plugins/security_slicing/dune b/src/plugins/security_slicing/dune new file mode 100644 index 0000000000000000000000000000000000000000..0067ab236e44e18ce847be78d7c0a2c5e9728a2a --- /dev/null +++ b/src/plugins/security_slicing/dune @@ -0,0 +1,21 @@ +( library + (name security_slicing) + (public_name frama-c-security_slicing.core) + (modules security_slicing_parameters components) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-security_slicing) (libraries frama-c-security_slicing.core) (site (frama-c plugins))) + + +( library + (name security_slicing_gui) + (public_name frama-c-security_slicing.gui) + (optional) + (modules register_gui) + (flags -open Frama_c_kernel -open Frama_c_gui -open Security_slicing) + (libraries security_slicing frama-c.kernel frama-c.gui) +) + +(plugin (name frama-c-plugins-security_slicing) (libraries frama-c-security_slicing.gui) (site (frama-c plugins_gui))) diff --git a/src/plugins/security_slicing/dune-project b/src/plugins/security_slicing/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..f01ab008f59598642ca3f10205c69af1f5db17f0 --- /dev/null +++ b/src/plugins/security_slicing/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-security_slicing) +(using dune_site 0.1) diff --git a/src/plugins/security_slicing/frama-c-security_slicing.opam b/src/plugins/security_slicing/frama-c-security_slicing.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/server/dune b/src/plugins/server/dune new file mode 100644 index 0000000000000000000000000000000000000000..509a77579bcdb4b041f4165a59af6f86a532f283 --- /dev/null +++ b/src/plugins/server/dune @@ -0,0 +1,12 @@ +( library + (name server) + (public_name frama-c-server.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel + (select server_zmq.ml from + (zmq -> server_zmq.ok.ml) + ( -> server_zmq.ko.ml) + )) +) + +(plugin (name frama-c-plugins-server) (libraries frama-c-server.core) (site (frama-c plugins))) diff --git a/src/plugins/server/dune-project b/src/plugins/server/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..7c5cf832bd235fb22c3d016afcc1c3cdf7f1d344 --- /dev/null +++ b/src/plugins/server/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-server) +(using dune_site 0.1) diff --git a/src/plugins/server/frama-c-server.opam b/src/plugins/server/frama-c-server.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml index e3c92e75a42f4a775c52c41233fe388559f4dfe2..74cda9e9c2ab4a67b54b21555eb472757099adbc 100644 --- a/src/plugins/server/kernel_main.ml +++ b/src/plugins/server/kernel_main.ml @@ -40,21 +40,18 @@ let () = let signature = Request.signature ~input:(module Junit) () in let result name descr = Request.result signature ~name ~descr:(Md.plain descr) (module Jstring) in + let result_list name descr = + Request.result signature ~name ~descr:(Md.plain descr) (module Jlist (Jstring)) in let set_version = result "version" "Frama-C version" in - let set_datadir = result "datadir" "Shared directory (FRAMAC_SHARE)" in - let set_libdir = result "libdir" "Lib directory (FRAMAC_LIB)" in - let set_pluginpath = Request.result signature - ~name:"pluginpath" - ~descr:(Md.plain "Plugin directories (FRAMAC_PLUGIN)") - (module Jlist(Jstring)) in + let set_datadir = result_list "datadir" "Shared directory (FRAMAC_SHARE)" in + let set_pluginpath = result_list "pluginpath" "Plugin directories (FRAMAC_PLUGIN)" in Request.register_sig ~package ~kind:`GET ~name:"getConfig" ~descr:(Md.plain "Frama-C Kernel configuration") signature begin fun rq () -> set_version rq Fc_config.version ; - set_datadir rq Fc_config.datadir ; - set_libdir rq Fc_config.libdir ; + set_datadir rq Fc_config.datadirs ; set_pluginpath rq Fc_config.plugin_dir ; end diff --git a/src/plugins/server/server_zmq.ko.ml b/src/plugins/server/server_zmq.ko.ml new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/server/server_zmq.ml b/src/plugins/server/server_zmq.ok.ml similarity index 100% rename from src/plugins/server/server_zmq.ml rename to src/plugins/server/server_zmq.ok.ml diff --git a/src/plugins/slicing/Slicing.mli b/src/plugins/slicing/Slicing.ml.bak similarity index 99% rename from src/plugins/slicing/Slicing.mli rename to src/plugins/slicing/Slicing.ml.bak index 67a5f2f7094c1f92f3ae50248de53a56bcd71596..83e0e23b1ffdb93068c2eefa4a658b0476b0e76e 100644 --- a/src/plugins/slicing/Slicing.mli +++ b/src/plugins/slicing/Slicing.ml.bak @@ -564,7 +564,7 @@ module Api:sig end -end +end = Api (* ---------------------------------------------------------------------- *) (** For debugging purpose only. @@ -576,7 +576,7 @@ module PrintSlice: sig Format.formatter -> kernel_function -> unit -end +end = PrintSlice (* Local Variables: diff --git a/src/plugins/slicing/dune b/src/plugins/slicing/dune new file mode 100644 index 0000000000000000000000000000000000000000..d6e78e23d47fb626bd3dbd4ffe64a561e71076c8 --- /dev/null +++ b/src/plugins/slicing/dune @@ -0,0 +1,8 @@ +( library + (name slicing) + (public_name frama-c-slicing.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel frama-c-pdg.core frama-c-sparecode.core) +) + +(plugin (name frama-c-plugins-slicing) (libraries frama-c-slicing.core) (site (frama-c plugins))) diff --git a/src/plugins/slicing/dune-project b/src/plugins/slicing/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..5793f766405734a902f6f43db6f1b501a5b27ebe --- /dev/null +++ b/src/plugins/slicing/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-slicing) +(using dune_site 0.1) diff --git a/src/plugins/slicing/frama-c-slicing.opam b/src/plugins/slicing/frama-c-slicing.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/slicing/gui/dune b/src/plugins/slicing/gui/dune new file mode 100644 index 0000000000000000000000000000000000000000..38839c6f40cef0dd2f99571401a0a4252fa0fa7f --- /dev/null +++ b/src/plugins/slicing/gui/dune @@ -0,0 +1,7 @@ +( library + (name slicing_gui) + (public_name frama-c-slicing.gui) + (optional) + (flags -open Frama_c_kernel -open Frama_c_gui -open Slicing) + (libraries frama-c.kernel frama-c.gui frama-c-slicing.core) +) diff --git a/src/plugins/slicing/register_gui.ml b/src/plugins/slicing/gui/register_gui.ml similarity index 100% rename from src/plugins/slicing/register_gui.ml rename to src/plugins/slicing/gui/register_gui.ml diff --git a/src/plugins/slicing/register_gui.mli b/src/plugins/slicing/gui/register_gui.mli similarity index 100% rename from src/plugins/slicing/register_gui.mli rename to src/plugins/slicing/gui/register_gui.mli diff --git a/src/plugins/sparecode/Sparecode.ml b/src/plugins/sparecode/Sparecode.ml new file mode 100644 index 0000000000000000000000000000000000000000..baf062aa11b424982e037a9447b36288d92912a5 --- /dev/null +++ b/src/plugins/sparecode/Sparecode.ml @@ -0,0 +1,23 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2019 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +module Register = Register diff --git a/src/plugins/sparecode/dune b/src/plugins/sparecode/dune new file mode 100644 index 0000000000000000000000000000000000000000..c81c4d44ec376d0773a5f800ec0c9d132dec9bff --- /dev/null +++ b/src/plugins/sparecode/dune @@ -0,0 +1,9 @@ +(library + (name Sparecode) + (public_name frama-c-sparecode.core) + (private_modules sparecode_params globs spare_marks transform register) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel frama-c-users.core frama-c-eva.core frama-c-pdg.core) +) + +(plugin (name frama-c-plugins-sparecode) (libraries frama-c-sparecode.core) (site (frama-c plugins))) diff --git a/src/plugins/sparecode/dune-project b/src/plugins/sparecode/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..1c1aa51970195c68ab3ef1d5a228f2d67e56044c --- /dev/null +++ b/src/plugins/sparecode/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-sparecode) +(using dune_site 0.1) diff --git a/src/plugins/sparecode/frama-c-sparecode.opam b/src/plugins/sparecode/frama-c-sparecode.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/studia/Studia.mli b/src/plugins/studia/Studia.ml similarity index 97% rename from src/plugins/studia/Studia.mli rename to src/plugins/studia/Studia.ml index 0d6d4ead926007792f326ac84d47d3469b781e24..f4c7f5b6a751e919eadc7d0338b7830d5fae6fde 100644 --- a/src/plugins/studia/Studia.mli +++ b/src/plugins/studia/Studia.ml @@ -21,6 +21,10 @@ (**************************************************************************) (** Computations of the statements that write a given memory zone. *) +include (struct + module Writes = Writes + module Reads = Reads +end : sig module Writes: sig (** Given an effect [e], something is directly modified by [e] (through an @@ -48,3 +52,4 @@ module Reads: sig or through an inner call for [Call] instructions. *) end +end) diff --git a/src/plugins/studia/dune b/src/plugins/studia/dune new file mode 100644 index 0000000000000000000000000000000000000000..a8a01d23e3241b7f05c083a5008903364b50f151 --- /dev/null +++ b/src/plugins/studia/dune @@ -0,0 +1,21 @@ +( library + (name studia) + (public_name frama-c-studia.core) + (modules options writes reads) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-studia) (libraries frama-c-studia.core) (site (frama-c plugins))) + + +( library + (name studia_gui) + (public_name frama-c-studia.gui) + (optional) + (modules studia_gui) + (flags -open Frama_c_kernel -open Frama_c_gui -open Studia) + (libraries studia frama-c.kernel frama-c.gui) +) + +(plugin (name frama-c-plugins-studia) (libraries frama-c-studia.gui) (site (frama-c plugins_gui))) diff --git a/src/plugins/studia/dune-project b/src/plugins/studia/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..9048eb084a9000f8f2e2a43b88d7ccc69db24103 --- /dev/null +++ b/src/plugins/studia/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-studia) +(using dune_site 0.1) diff --git a/src/plugins/studia/frama-c-studia.opam b/src/plugins/studia/frama-c-studia.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/users/Users.ml b/src/plugins/users/Users.ml new file mode 100644 index 0000000000000000000000000000000000000000..a185bed44a9019822977a3af5a80a3fac60da5bc --- /dev/null +++ b/src/plugins/users/Users.ml @@ -0,0 +1,26 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2019 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +(* $Id: Users.mli,v 1.5 2008-04-01 09:25:22 uid568 Exp $ *) +(** Functions used by another function. + @see <../users/index.html> internal documentation. *) +module Users_register = Users_register diff --git a/src/plugins/users/dune b/src/plugins/users/dune new file mode 100644 index 0000000000000000000000000000000000000000..f3a9ef31adc4fcda474299c18ae190107fbb235f --- /dev/null +++ b/src/plugins/users/dune @@ -0,0 +1,8 @@ +(library + (name Users) + (public_name frama-c-users.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel frama-c-callgraph.core) +) + +(plugin (name frama-c-plugins-users) (libraries frama-c-users.core) (site (frama-c plugins))) diff --git a/src/plugins/users/dune-project b/src/plugins/users/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..f8e04564f3fb326dbe7a1a6caa04e18a9260cbda --- /dev/null +++ b/src/plugins/users/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-users) +(using dune_site 0.1) diff --git a/src/plugins/users/frama-c-users.opam b/src/plugins/users/frama-c-users.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/value/Eva.ml b/src/plugins/value/Eva.ml new file mode 100644 index 0000000000000000000000000000000000000000..839d8d79bb179df1a67dc6c071ff2e7a746cc490 --- /dev/null +++ b/src/plugins/value/Eva.ml @@ -0,0 +1,27 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2018 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +(** Analysis for values and pointers *) + +(** No function is directly exported: they are registered in {!Db.Value}. *) + +module Value_results = Value_results diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.ml similarity index 100% rename from src/plugins/value/domains/abstract_domain.mli rename to src/plugins/value/domains/abstract_domain.ml diff --git a/src/plugins/value/domains/numerors/numerors.ml b/src/plugins/value/domains/numerors/numerors.ml new file mode 100644 index 0000000000000000000000000000000000000000..6e3be0a1e271eb4fddc3a77bc83af3182df199c7 --- /dev/null +++ b/src/plugins/value/domains/numerors/numerors.ml @@ -0,0 +1,158 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2018 *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +#24 "src/plugins/value/domains/numerors/numerors_domain.ok.ml" + +open Eval +open Cil_types + +type value = Numerors_value.t +type location = Precise_locs.precise_location +let value_key = Numerors_value.error_key + +let ok = true + +module Numerors_Value = struct + include Numerors_value + + (* In this domain, we only track floating-point variables. *) + let track_variable vi = Cil.isFloatingType vi.vtype + + (* No widen in the domain for now *) + let widen _ _ = top + + let dbetween = function + | min :: max :: [] -> Numerors_value.dbetween min max + | _ -> `Value Numerors_value.top + + let rbetween = function + | min :: max :: [] -> Numerors_value.rbetween min max + | _ -> `Value Numerors_value.top + + let sqrt = function + | x :: [] -> Numerors_value.sqrt x + | _ -> `Value Numerors_value.top + + let log = function + | x :: [] -> Numerors_value.log x + | _ -> `Value Numerors_value.top + + let exp = function + | x :: [] -> Numerors_value.exp x + | _ -> `Value Numerors_value.top + + let dprint_callstack = ref [] + let dprint = function + | x :: [] -> + let call fmt () = + let abs = Numerors_value.get_max_absolute_error x in + let rel = Numerors_value.get_max_relative_error x in + match abs, rel with + | Some x, Some y -> + Format.fprintf fmt "@[%a@]@.@[%a@]@." + Numerors_float.pretty x + Numerors_float.pretty y + | _, _ -> () + (* + Format.fprintf fmt "@[%a@]@.@." Numerors_value.pretty x + *) + in dprint_callstack := !dprint_callstack @ [call] ; + `Value Numerors_value.top + | _ -> `Value Numerors_value.top + + let builtins = + [ ("Frama_C_double_interval", dbetween) + ; ("Frama_C_real_interval_as_double", rbetween) + ; ("log", log) ; ("exp", exp) ; ("sqrt", sqrt) + ; ("DPRINT", dprint) + ] +end + +let add_numerors_value (module Value: Abstract_value.Internal) = + let module External_Value = Structure.Open (Structure.Key_Value) (Value) in + let module V = struct + include Value_product.Make (Value) (Numerors_value) + + let forward_cast = match External_Value.get Main_values.cvalue_key with + | None -> forward_cast + | Some get_cvalue -> + fun ~src_type ~dst_type (value, num) -> + forward_cast ~src_type ~dst_type (value, num) >>-: fun (value', num) -> + let num = match src_type, dst_type with + | Eval_typ.TSInt _, Eval_typ.TSFloat fkind -> + begin + try + let cvalue = get_cvalue value in + let ival = Cvalue.V.project_ival cvalue in + match Ival.min_and_max ival with + | Some min, Some max -> + let min, max = Integer.to_int min, Integer.to_int max in + let prec = Numerors_utils.Precisions.of_fkind fkind in + Numerors_value.of_ints ~prec min max + | _, _ -> num + (* Integer.to_int may fail for too big integers. *) + with Cvalue.V.Not_based_on_null | Failure _ -> num + end + | _, _ -> num + in + value', num + end in + (module V: Abstract_value.Internal) + +let reduce_error (type v) (module V: Abstract_value.External with type t = v) = + match V.get Numerors_value.error_key, V.get Main_values.cvalue_key with + | Some get_error, Some get_cvalue -> + begin + let set_error = V.set Numerors_value.error_key in + fun t -> + let cvalue = get_cvalue t in + try + let ival = Cvalue.V.project_ival cvalue in + match ival with + | Ival.Float fval -> + begin + let error = get_error t in + let error = Numerors_value.reduce fval error in + match error with + | `Value error -> set_error error t + | `Bottom -> t (* TODO: we should be able to reduce to bottom. *) + end + | _ -> t + with Cvalue.V.Not_based_on_null -> t + end + | _, _ -> fun x -> x + + +module Domain = struct + module Name = struct let name = "numerors" end + include Simple_memory.Make_Domain (Name) (Numerors_Value) + + let post_analysis f = + match f, Value_parameters.NumerorsLogFile.get () with + | _, s when s = "" -> () + | `Value _, s -> + let log = Pervasives.open_out s in + let fmt = Format.formatter_of_out_channel log in + List.iter (fun f -> f fmt ()) !Numerors_Value.dprint_callstack ; + Pervasives.close_out log + | _, _ -> () +end diff --git a/src/plugins/value/domains/numerors/numerors_domain.ml b/src/plugins/value/domains/numerors/numerors_domain.ml index 6fe3f9da06ad0730570a32512d780c7de505d3ea..116913b274f5c16f7bfa3fbf1470d08d2e9003af 100644 --- a/src/plugins/value/domains/numerors/numerors_domain.ml +++ b/src/plugins/value/domains/numerors/numerors_domain.ml @@ -24,6 +24,10 @@ open Eval open Cil_types (* The numerors values, plus some builtin functions. *) +let value_key = Numerors_value.error_key + +let ok = true + module Numerors_Value = struct include Numerors_value diff --git a/src/plugins/value/domains/simpler_domains.mli b/src/plugins/value/domains/simpler_domains.ml similarity index 100% rename from src/plugins/value/domains/simpler_domains.mli rename to src/plugins/value/domains/simpler_domains.ml diff --git a/src/plugins/value/dune b/src/plugins/value/dune new file mode 100644 index 0000000000000000000000000000000000000000..62af8574299546302fafa950636ffba0975fe16c --- /dev/null +++ b/src/plugins/value/dune @@ -0,0 +1,109 @@ +( library + (name eva) + (public_name frama-c-eva.core) + (modules + split_strategy value_parameters + value_perf value_util + mark_noresults + widen_hints_ext widen + alarmset warn eval_typ backward_formals + eval_op + locals_scoping + builtins + builtins_malloc + library_functions + builtins_string + builtins_misc + value_results + builtins_memory + builtins_print_c + builtins_watchpoint + state_import + function_args split_return + per_stmt_slevel + eval structure + powerset transfer_logic + value_product location_lift + cvalue_forward cvalue_backward + eval_terms eval_annots + main_values main_locations offsm_value + domain_store domain_builder + domain_product domain_lift unit_domain + gauges_domain + hcexprs + equality equality_domain + offsm_domain + symbolic_locs + cvalue_transfer cvalue_init + cvalue_specification + cvalue_domain builtins_float + evaluation subdivided_evaluation + recursion + abstract abstract_value abstract_location abstract_domain + red_statuses + cvalue_offsetmap + simpler_domains + simple_memory + sign_value + inout_domain + sign_domain + printer_domain + abstractions partitioning_index trace_partitioning partition partitioning_parameters + transfer_stmt mem_exec iterator + transfer_specification initialization analysis register compute_functions + eva_annotations octagons traces_domain auto_loop_unroll domain_mode +) +; (public_interfaces (Eva)) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel frama-c-callgraph.core frama-c-rtegen.core frama-c-loop-analysis.core frama-c-scope.core) +) + +(plugin (name frama-c-plugins-eva) (libraries frama-c-eva.core) (site (frama-c plugins))) + +( library + (name numerors) + (public_name frama-c-eva.numerors) + (flags -open Frama_c_kernel -open Eva) + (modules numerors numerors_domain numerors_utils numerors_float numerors_interval numerors_arithmetics numerors_value) + (libraries frama-c.kernel frama-c-eva.core mlmpfr) + (optional) +) + +;(plugin (name frama-c-plugins-eva-numerors) (libraries frama-c-eva.numerors) (site (frama-c plugins))) + +( library + (name apron_domain) + (public_name frama-c-eva.apron) + (flags -open Frama_c_kernel -open Eva) + (modules apron_domain) + (libraries frama-c.kernel frama-c-eva.core apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron) + (optional) +) + + + +( library + (name eva_gui) + (public_name frama-c-eva.gui) + (optional) + (modules gui_callstacks_filters gui_callstacks_manager gui_eval gui_types register_gui gui_red) +; (public_interfaces ()) + (flags -open Frama_c_kernel -open Frama_c_gui -open Eva) + (libraries eva frama-c.kernel frama-c.gui) +) + +(plugin (name frama-c-plugins-eva-gui) (libraries frama-c-eva.gui) (site (frama-c plugins_gui))) + +(copy_files# domains/*) +(copy_files# domains/equality/*) +(copy_files# domains/cvalue/*) +(copy_files# domains/gauges/*) +(copy_files# domains/apron/*) +(copy_files# domains/numerors/*) +(copy_files# engine/*) +(copy_files# utils/*) +(copy_files# legacy/*) +(copy_files# values/*) +(copy_files# values/numerors/*) +(copy_files# gui_files/*) +(copy_files# partitioning/*) diff --git a/src/plugins/value/dune-project b/src/plugins/value/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..5015dc8479713e4bc39268e268c2855394084c7a --- /dev/null +++ b/src/plugins/value/dune-project @@ -0,0 +1,2 @@ +(lang dune 2.8) +(using dune_site 0.1) diff --git a/src/plugins/value/frama-c-eva.opam b/src/plugins/value/frama-c-eva.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/value/utils/mark_noresults.ml b/src/plugins/value/utils/mark_noresults.ml index 6a35df078cdc6c5f35690531e83470c4a6bccf4c..954752b066e08ae1b48e0dfdd23f69a725fabe0b 100644 --- a/src/plugins/value/utils/mark_noresults.ml +++ b/src/plugins/value/utils/mark_noresults.ml @@ -35,7 +35,6 @@ let no_memoization_enabled () = not (Value_parameters.NoResultsFunctions.is_empty ()) - (* Local Variables: compile-command: "make -C ../../../.." diff --git a/src/plugins/value/values/abstract_location.mli b/src/plugins/value/values/abstract_location.ml similarity index 100% rename from src/plugins/value/values/abstract_location.mli rename to src/plugins/value/values/abstract_location.ml diff --git a/src/plugins/value/values/abstract_value.mli b/src/plugins/value/values/abstract_value.ml similarity index 100% rename from src/plugins/value/values/abstract_value.mli rename to src/plugins/value/values/abstract_value.ml diff --git a/src/plugins/value_types/cvalue.mli b/src/plugins/value_types/cvalue.mli index dc2f6ae7dd335273ae7014033fba9926c1cfb4e6..d47be466d5db8ddeedd8c7cbcb9b9ad0583f185b 100644 --- a/src/plugins/value_types/cvalue.mli +++ b/src/plugins/value_types/cvalue.mli @@ -49,7 +49,7 @@ module V : sig and type numerical_widen_hint = Location_Bytes.numerical_widen_hint and type size_widen_hint = Location_Bytes.size_widen_hint - include module type of Offsetmap_lattice_with_isotropy + include Offsetmap_lattice_with_isotropy.S with type t := t and type numerical_widen_hint := numerical_widen_hint and type size_widen_hint := size_widen_hint @@ -172,7 +172,7 @@ module V_Or_Uninitialized : sig | C_init_esc of V.t | C_init_noesc of V.t - include module type of Offsetmap_lattice_with_isotropy + include Offsetmap_lattice_with_isotropy.S with type t := t and type size_widen_hint = Location_Bytes.size_widen_hint and type numerical_widen_hint = Location_Bytes.numerical_widen_hint @@ -235,7 +235,7 @@ module V_Or_Uninitialized : sig (** Memory slices. They are maps from intervals to values with flags. All sizes and intervals are in bits. *) module V_Offsetmap: sig - include module type of Offsetmap_sig + include Offsetmap_sig.S with type v = V_Or_Uninitialized.t and type widen_hint = V_Or_Uninitialized.numerical_widen_hint @@ -254,7 +254,7 @@ end module Model: sig (** Functions inherited from [Lmap_sig] interface *) - include module type of Lmap_sig + include Lmap_sig.S with type v = V_Or_Uninitialized.t and type offsetmap = V_Offsetmap.t and type widen_hint_base = V_Or_Uninitialized.numerical_widen_hint diff --git a/src/plugins/variadic/Variadic.mli b/src/plugins/variadic/Variadic.ml similarity index 100% rename from src/plugins/variadic/Variadic.mli rename to src/plugins/variadic/Variadic.ml diff --git a/src/plugins/variadic/dune b/src/plugins/variadic/dune new file mode 100644 index 0000000000000000000000000000000000000000..19a8a03154ab3f15f2dda2427b0c5a2eddc38594 --- /dev/null +++ b/src/plugins/variadic/dune @@ -0,0 +1,8 @@ +( library + (name variadic) + (public_name frama-c-variadic.core) + (flags -open Frama_c_kernel) + (libraries frama-c.kernel) +) + +(plugin (name frama-c-plugins-variadic) (libraries frama-c-variadic.core) (site (frama-c plugins))) diff --git a/src/plugins/variadic/dune-project b/src/plugins/variadic/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..c2839f3ae38306c9d09dfc0555bc984828c2763b --- /dev/null +++ b/src/plugins/variadic/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-variadic) +(using dune_site 0.1) diff --git a/src/plugins/variadic/format_types.mli b/src/plugins/variadic/format_types.ml similarity index 100% rename from src/plugins/variadic/format_types.mli rename to src/plugins/variadic/format_types.ml diff --git a/src/plugins/variadic/frama-c-variadic.opam b/src/plugins/variadic/frama-c-variadic.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/variadic/va_types.mli b/src/plugins/variadic/va_types.ml similarity index 100% rename from src/plugins/variadic/va_types.mli rename to src/plugins/variadic/va_types.ml diff --git a/src/plugins/wp/.merlin b/src/plugins/wp/.merlin deleted file mode 100644 index d4209155cd3e7debb97a64fc44ef4bcf0bc60184..0000000000000000000000000000000000000000 --- a/src/plugins/wp/.merlin +++ /dev/null @@ -1,2 +0,0 @@ -REC -PKG why3 diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml index d08034e93ca7bd84a44ba06bb4d5b340ad474e75..0a892c66dd7423550ebe6967246874150a15fa73 100644 --- a/src/plugins/wp/Cache.ml +++ b/src/plugins/wp/Cache.ml @@ -37,7 +37,7 @@ let get_miss () = !miss let get_removed () = !removed let mark_cache ~mode hash = - if mode = Cleanup || !Fc_config.is_gui then Hashtbl.replace cleanup hash () + if mode = Cleanup || Fc_config.is_gui then Hashtbl.replace cleanup hash () module CACHEDIR = WpContext.StaticGenerator(Datatype.Unit) (struct diff --git a/src/plugins/wp/dune b/src/plugins/wp/dune new file mode 100644 index 0000000000000000000000000000000000000000..0e648a050ac2babe59602ad1e38a9f38723a64b9 --- /dev/null +++ b/src/plugins/wp/dune @@ -0,0 +1,99 @@ +(library + (name wp) + (public_name frama-c-wp.core) + (flags (-open Frama_c_kernel)) + (libraries frama-c.kernel why3 qed zarith ocamlgraph) +) + +(plugin (name frama-c-plugins-wp) (libraries frama-c-wp.core) (site (frama-c plugins))) + + +(ocamllex driver rformat script) + +;find share \( -not -name ".gitignore" \) -type f -printf "(%p as wp/%p)\n" >> dune +; wp/share -> wp + +(install + (package frama-c-wp) + (section (site (frama-c share))) + (files +(share/Makefile.resources as wp/Makefile.resources) +(share/install.ml as wp/install.ml) +(share/ergo/int.Abs.mlw as wp/ergo/int.Abs.mlw) +(share/ergo/Cint.mlw as wp/ergo/Cint.mlw) +(share/ergo/int.MinMax.mlw as wp/ergo/int.MinMax.mlw) +(share/ergo/real.Hyperbolic.mlw as wp/ergo/real.Hyperbolic.mlw) +(share/ergo/bool.Bool.mlw as wp/ergo/bool.Bool.mlw) +(share/ergo/real.Square.mlw as wp/ergo/real.Square.mlw) +(share/ergo/int.ComputerOfEuclideanDivision.mlw as wp/ergo/int.ComputerOfEuclideanDivision.mlw) +(share/ergo/ExpLog.mlw as wp/ergo/ExpLog.mlw) +(share/ergo/real.Real.mlw as wp/ergo/real.Real.mlw) +(share/ergo/Cbits.mlw as wp/ergo/Cbits.mlw) +(share/ergo/real.Trigonometry.mlw as wp/ergo/real.Trigonometry.mlw) +(share/ergo/int.Int.mlw as wp/ergo/int.Int.mlw) +(share/ergo/map.Const.mlw as wp/ergo/map.Const.mlw) +(share/ergo/Memory.mlw as wp/ergo/Memory.mlw) +(share/ergo/real.FromInt.mlw as wp/ergo/real.FromInt.mlw) +(share/ergo/int.ComputerDivision.mlw as wp/ergo/int.ComputerDivision.mlw) +(share/ergo/ArcTrigo.mlw as wp/ergo/ArcTrigo.mlw) +(share/ergo/real.Truncate.mlw as wp/ergo/real.Truncate.mlw) +(share/ergo/real.MinMax.mlw as wp/ergo/real.MinMax.mlw) +(share/ergo/Cfloat.mlw as wp/ergo/Cfloat.mlw) +(share/ergo/real.Polar.mlw as wp/ergo/real.Polar.mlw) +(share/ergo/real.PowerReal.mlw as wp/ergo/real.PowerReal.mlw) +(share/ergo/Square.mlw as wp/ergo/Square.mlw) +(share/ergo/map.Map.mlw as wp/ergo/map.Map.mlw) +(share/ergo/Vset.mlw as wp/ergo/Vset.mlw) +(share/ergo/real.RealInfix.mlw as wp/ergo/real.RealInfix.mlw) +(share/ergo/Vlist.mlw as wp/ergo/Vlist.mlw) +(share/ergo/real.Abs.mlw as wp/ergo/real.Abs.mlw) +(share/ergo/Cmath.mlw as wp/ergo/Cmath.mlw) +(share/ergo/Qed.mlw as wp/ergo/Qed.mlw) +(share/ergo/real.ExpLog.mlw as wp/ergo/real.ExpLog.mlw) +(share/why3/frama_c_wp/vlist.mlw as wp/why3/frama_c_wp/vlist.mlw) +(share/why3/frama_c_wp/cbits.mlw as wp/why3/frama_c_wp/cbits.mlw) +(share/why3/frama_c_wp/cint.mlw as wp/why3/frama_c_wp/cint.mlw) +(share/why3/frama_c_wp/qed.mlw as wp/why3/frama_c_wp/qed.mlw) +(share/why3/frama_c_wp/vset.mlw as wp/why3/frama_c_wp/vset.mlw) +(share/why3/frama_c_wp/memory.mlw as wp/why3/frama_c_wp/memory.mlw) +(share/why3/frama_c_wp/cmath.mlw as wp/why3/frama_c_wp/cmath.mlw) +(share/why3/frama_c_wp/cfloat.mlw as wp/why3/frama_c_wp/cfloat.mlw) +(share/coqwp/Cmath.v as wp/coqwp/Cmath.v) +(share/coqwp/Qedlib.v as wp/coqwp/Qedlib.v) +(share/coqwp/Memory.v as wp/coqwp/Memory.v) +(share/coqwp/map/Const.v as wp/coqwp/map/Const.v) +(share/coqwp/map/Map.v as wp/coqwp/map/Map.v) +(share/coqwp/HighOrd.v as wp/coqwp/HighOrd.v) +(share/coqwp/int/Abs.v as wp/coqwp/int/Abs.v) +(share/coqwp/int/Int.v as wp/coqwp/int/Int.v) +(share/coqwp/int/Exponentiation.v as wp/coqwp/int/Exponentiation.v) +(share/coqwp/int/Power.v as wp/coqwp/int/Power.v) +(share/coqwp/int/MinMax.v as wp/coqwp/int/MinMax.v) +(share/coqwp/int/ComputerOfEuclideanDivision.v as wp/coqwp/int/ComputerOfEuclideanDivision.v) +(share/coqwp/int/ComputerDivision.v as wp/coqwp/int/ComputerDivision.v) +(share/coqwp/int/EuclideanDivision.v as wp/coqwp/int/EuclideanDivision.v) +(share/coqwp/Cfloat.v as wp/coqwp/Cfloat.v) +(share/coqwp/bool/Bool.v as wp/coqwp/bool/Bool.v) +(share/coqwp/Qed.v as wp/coqwp/Qed.v) +(share/coqwp/Bits.v as wp/coqwp/Bits.v) +(share/coqwp/ExpLog.v as wp/coqwp/ExpLog.v) +(share/coqwp/Square.v as wp/coqwp/Square.v) +(share/coqwp/real/Abs.v as wp/coqwp/real/Abs.v) +(share/coqwp/real/Trigonometry.v as wp/coqwp/real/Trigonometry.v) +(share/coqwp/real/RealInfix.v as wp/coqwp/real/RealInfix.v) +(share/coqwp/real/MinMax.v as wp/coqwp/real/MinMax.v) +(share/coqwp/real/ExpLog.v as wp/coqwp/real/ExpLog.v) +(share/coqwp/real/Square.v as wp/coqwp/real/Square.v) +(share/coqwp/real/Real.v as wp/coqwp/real/Real.v) +(share/coqwp/real/PowerReal.v as wp/coqwp/real/PowerReal.v) +(share/coqwp/real/FromInt.v as wp/coqwp/real/FromInt.v) +(share/coqwp/Vset.v as wp/coqwp/Vset.v) +(share/coqwp/Vlist.v as wp/coqwp/Vlist.v) +(share/coqwp/Zbits.v as wp/coqwp/Zbits.v) +(share/coqwp/ArcTrigo.v as wp/coqwp/ArcTrigo.v) +(share/coqwp/Cint.v as wp/coqwp/Cint.v) +(share/coqwp/Cbits.v as wp/coqwp/Cbits.v) +(share/coqwp/BuiltIn.v as wp/coqwp/BuiltIn.v) +(share/wp.driver as wp/wp.driver) +(share/Makefile.coqwp as wp/Makefile.coqwp) +)) diff --git a/src/plugins/wp/dune-project b/src/plugins/wp/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..22036288a26a0a232d6b52e8902a4b6c599eb72e --- /dev/null +++ b/src/plugins/wp/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.8) +(name frama-c-wp) +(using dune_site 0.1) diff --git a/src/plugins/wp/frama-c-wp.opam b/src/plugins/wp/frama-c-wp.opam new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/wp/GuiComposer.ml b/src/plugins/wp/gui/GuiComposer.ml similarity index 100% rename from src/plugins/wp/GuiComposer.ml rename to src/plugins/wp/gui/GuiComposer.ml diff --git a/src/plugins/wp/GuiComposer.mli b/src/plugins/wp/gui/GuiComposer.mli similarity index 100% rename from src/plugins/wp/GuiComposer.mli rename to src/plugins/wp/gui/GuiComposer.mli diff --git a/src/plugins/wp/GuiConfig.ml b/src/plugins/wp/gui/GuiConfig.ml similarity index 100% rename from src/plugins/wp/GuiConfig.ml rename to src/plugins/wp/gui/GuiConfig.ml diff --git a/src/plugins/wp/GuiConfig.mli b/src/plugins/wp/gui/GuiConfig.mli similarity index 100% rename from src/plugins/wp/GuiConfig.mli rename to src/plugins/wp/gui/GuiConfig.mli diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/gui/GuiGoal.ml similarity index 100% rename from src/plugins/wp/GuiGoal.ml rename to src/plugins/wp/gui/GuiGoal.ml diff --git a/src/plugins/wp/GuiGoal.mli b/src/plugins/wp/gui/GuiGoal.mli similarity index 100% rename from src/plugins/wp/GuiGoal.mli rename to src/plugins/wp/gui/GuiGoal.mli diff --git a/src/plugins/wp/GuiList.ml b/src/plugins/wp/gui/GuiList.ml similarity index 100% rename from src/plugins/wp/GuiList.ml rename to src/plugins/wp/gui/GuiList.ml diff --git a/src/plugins/wp/GuiList.mli b/src/plugins/wp/gui/GuiList.mli similarity index 100% rename from src/plugins/wp/GuiList.mli rename to src/plugins/wp/gui/GuiList.mli diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/gui/GuiNavigator.ml similarity index 100% rename from src/plugins/wp/GuiNavigator.ml rename to src/plugins/wp/gui/GuiNavigator.ml diff --git a/src/plugins/wp/GuiNavigator.mli b/src/plugins/wp/gui/GuiNavigator.mli similarity index 100% rename from src/plugins/wp/GuiNavigator.mli rename to src/plugins/wp/gui/GuiNavigator.mli diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/gui/GuiPanel.ml similarity index 100% rename from src/plugins/wp/GuiPanel.ml rename to src/plugins/wp/gui/GuiPanel.ml diff --git a/src/plugins/wp/GuiPanel.mli b/src/plugins/wp/gui/GuiPanel.mli similarity index 100% rename from src/plugins/wp/GuiPanel.mli rename to src/plugins/wp/gui/GuiPanel.mli diff --git a/src/plugins/wp/GuiProof.ml b/src/plugins/wp/gui/GuiProof.ml similarity index 100% rename from src/plugins/wp/GuiProof.ml rename to src/plugins/wp/gui/GuiProof.ml diff --git a/src/plugins/wp/GuiProof.mli b/src/plugins/wp/gui/GuiProof.mli similarity index 100% rename from src/plugins/wp/GuiProof.mli rename to src/plugins/wp/gui/GuiProof.mli diff --git a/src/plugins/wp/GuiProver.ml b/src/plugins/wp/gui/GuiProver.ml similarity index 100% rename from src/plugins/wp/GuiProver.ml rename to src/plugins/wp/gui/GuiProver.ml diff --git a/src/plugins/wp/GuiProver.mli b/src/plugins/wp/gui/GuiProver.mli similarity index 100% rename from src/plugins/wp/GuiProver.mli rename to src/plugins/wp/gui/GuiProver.mli diff --git a/src/plugins/wp/GuiSequent.ml b/src/plugins/wp/gui/GuiSequent.ml similarity index 100% rename from src/plugins/wp/GuiSequent.ml rename to src/plugins/wp/gui/GuiSequent.ml diff --git a/src/plugins/wp/GuiSequent.mli b/src/plugins/wp/gui/GuiSequent.mli similarity index 100% rename from src/plugins/wp/GuiSequent.mli rename to src/plugins/wp/gui/GuiSequent.mli diff --git a/src/plugins/wp/GuiSource.ml b/src/plugins/wp/gui/GuiSource.ml similarity index 100% rename from src/plugins/wp/GuiSource.ml rename to src/plugins/wp/gui/GuiSource.ml diff --git a/src/plugins/wp/GuiSource.mli b/src/plugins/wp/gui/GuiSource.mli similarity index 100% rename from src/plugins/wp/GuiSource.mli rename to src/plugins/wp/gui/GuiSource.mli diff --git a/src/plugins/wp/GuiTactic.ml b/src/plugins/wp/gui/GuiTactic.ml similarity index 100% rename from src/plugins/wp/GuiTactic.ml rename to src/plugins/wp/gui/GuiTactic.ml diff --git a/src/plugins/wp/GuiTactic.mli b/src/plugins/wp/gui/GuiTactic.mli similarity index 100% rename from src/plugins/wp/GuiTactic.mli rename to src/plugins/wp/gui/GuiTactic.mli diff --git a/src/plugins/wp/gui/dune b/src/plugins/wp/gui/dune new file mode 100644 index 0000000000000000000000000000000000000000..adff62055a7c85f27dec2f8b0566947150761fd2 --- /dev/null +++ b/src/plugins/wp/gui/dune @@ -0,0 +1,7 @@ +( library + (name wp_gui) + (public_name frama-c-wp.gui) + (optional) + (flags -open Frama_c_kernel -open Frama_c_gui -open Wp) + (libraries frama-c-wp.core frama-c.kernel frama-c.gui why3 qed lablgtk2) +) diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml index c350f0f5779d5de2272bee29683161bf140e4290..28e4daf8012378928a8072fbae490f95900b676a 100644 --- a/src/plugins/wp/register.ml +++ b/src/plugins/wp/register.ml @@ -937,7 +937,7 @@ let () = Cmdline.run_after_setting_files let () = Cmdline.run_after_configuring_stage Why3Provers.configure let do_prover_detect () = - if not !Fc_config.is_gui && Wp_parameters.Detect.get () then + if not Fc_config.is_gui && Wp_parameters.Detect.get () then let provers = Why3Provers.provers () in if provers = [] then Wp_parameters.result "No Why3 provers detected." diff --git a/src/plugins/wp/wp.ml b/src/plugins/wp/wp.ml new file mode 100644 index 0000000000000000000000000000000000000000..b98ab116339ab6942898142a42e1dd8ee1e3e8fd --- /dev/null +++ b/src/plugins/wp/wp.ml @@ -0,0 +1,83 @@ +(**************************************************************************) +(* *) +(* This file is part of WP plug-in of Frama-C. *) +(* *) +(* Copyright (C) 2007-2019 *) +(* CEA (Commissariat a l'energie atomique et aux energies *) +(* 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 licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +module Wp_parameters = Wp_parameters +module Ctypes = Ctypes +module Clabels = Clabels +module MemoryContext = MemoryContext +module LogicUsage = LogicUsage +module RefUsage = RefUsage +module NormatLabels = NormAtLabels +module WpPropId = WpPropId +module Mcfg = Mcfg +module Context = Context +module Warning = Warning +module Lang = Lang +module Repr = Repr +module Passive = Passive +module Splitter = Splitter +module LogicBuiltins = LogicBuiltins +module Definitions = Definitions +module Cint = Cint +module Cfloat = Cfloat +module Vset = Vset +module Cstring = Cstring +module Sigs = Sigs +module Mstate = Mstate +module Conditions = Conditions +module Filtering = Filtering +module Plang = Plang +module Pcfg = Pcfg +module Pcond = Pcond +module CodeSemantics = CodeSemantics +module LogicCompiler = LogicCompiler +module LogicSemantics = LogicSemantics +module Sigma = Sigma +module MemVar = MemVar +module MemTyped = MemTyped +module CfgCompiler = CfgCompiler +module StmtSemantics = StmtSemantics +module Factory = Factory +module Driver = Driver +module VCS = VCS +module Tactical = Tactical +module Strategy = Strategy +module Auto = Auto +module VC = VC +module Wpo = Wpo +module ProverTask = ProverTask +module Prover = Prover + + +(** For gui *) +module ProofEngine = ProofEngine +module ProofScript = ProofScript +module ProofSession = ProofSession +module ProverScript = ProverScript +module ProverSearch = ProverSearch +module WpRTE = WpRTE +module Rformat = Rformat +module WpContext = WpContext +module WpStrategy = WpStrategy +module Why3Provers = Why3Provers +module ProverWhy3 = ProverWhy3 +module Cache = Cache diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml index 448ff335f59df0604294f560f9f87b957e69a5ae..78ebfb90fbfa624d08c286714ab4428231b44781 100644 --- a/src/plugins/wp/wp_parameters.ml +++ b/src/plugins/wp/wp_parameters.ml @@ -1069,7 +1069,7 @@ let get_overflows () = Overflows.get () && active_unless_rte "-wp-overflows" let dkey = register_category "prover" -let has_out () = OutputDir.get () <> "" +let has_out () = OutputDir.get() <> "" let make_output_dir dir = if Sys.file_exists dir then @@ -1124,7 +1124,7 @@ let base_output () = | None -> let output = match OutputDir.get () with | "" -> - if !Fc_config.is_gui + if Fc_config.is_gui then make_gui_dir () else make_tmp_dir () | dir -> diff --git a/test-file b/test-file new file mode 100644 index 0000000000000000000000000000000000000000..9ab0d2c65c867e9c0ae58b3b99378f09d7c218da Binary files /dev/null and b/test-file differ diff --git a/tests/crowbar/.merlin b/tests/crowbar/.merlin deleted file mode 100644 index bad48ad47efcb83ced077e1e3644853249c968ab..0000000000000000000000000000000000000000 --- a/tests/crowbar/.merlin +++ /dev/null @@ -1,2 +0,0 @@ -PKG crowbar -REC diff --git a/tests/journal/intra.ml b/tests/journal/intra.ml index 7785c391999cf580cd9d92645b63f9a34d0f93b3..eca295d9ae6b0c28cc261de43f4277c1d5e690b6 100644 --- a/tests/journal/intra.ml +++ b/tests/journal/intra.ml @@ -1 +1 @@ -let () = Db.Main.extend (fun _ -> ignore (Sparecode.Register.get true true)) +let () = Db.Main.extend (fun _ -> ignore (Sparecode.Register.get ~select_annot:true ~select_slice_pragma:true))