diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index adc50617d82bd56443b06f145ad8c8a8848dcd25..65586e0f0fc56fd39fc130fbfc7c36cb0ee9ffe2 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -5,7 +5,7 @@ stages:
frama-c-external:
stage: frama_c_and_plugins
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c-external --base-branch stable/phosphorus
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c-external --base-branch stable/phosphorus
tags:
except:
- tags
@@ -13,23 +13,23 @@ frama-c-external:
frama-c:
stage: frama_c_and_plugins
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c
tags:
except:
- tags
-
+
frama-c-ocaml-4.03:
stage: distrib_and_compatibility
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --ocaml 4.03 --camlp4 4.03 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --ocaml 4.03 --camlp4 4.03 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c
tags:
except:
- tags
-
+
frama-c-ocaml-4.04:
stage: distrib_and_compatibility
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --ocaml 4.04 --camlp4 4.04 --lablgtk 4bbd5cf1990aa8b775cf247fbfe5be321e13cc61 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --ocaml 4.04 --camlp4 4.04 --lablgtk 4bbd5cf1990aa8b775cf247fbfe5be321e13cc61 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c
tags:
except:
- tags
@@ -37,7 +37,7 @@ frama-c-ocaml-4.04:
frama-c-ocaml-4.05:
stage: distrib_and_compatibility
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --ocaml 4.05 --camlp4 4.05 --lablgtk 4bbd5cf1990aa8b775cf247fbfe5be321e13cc61 --camomile 3f4d657d50c17213f3338ca75efb30d728704df3 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --ocaml 4.05 --camlp4 4.05 --lablgtk 4bbd5cf1990aa8b775cf247fbfe5be321e13cc61 --camomile 3f4d657d50c17213f3338ca75efb30d728704df3 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c
tags:
except:
- tags
@@ -47,7 +47,7 @@ frama-c-ocaml-4.05:
frama-c-internal:
stage: distrib_and_compatibility
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c-internal
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c-internal
tags:
only:
- master
@@ -58,7 +58,7 @@ frama-c-internal:
frama-c-distrib:
stage: distrib_and_compatibility
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c-distrib
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c-distrib
tags:
except:
- tags
@@ -67,15 +67,15 @@ frama-c-distrib:
Genassigns:
stage: frama_c_and_plugins
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Genassigns --base-branch stable/phosphorus
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Genassigns --base-branch stable/phosphorus
tags:
except:
- tags
-
+
Mthread:
stage: frama_c_and_plugins
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Mthread --base-branch stable/phosphorus
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Mthread --base-branch stable/phosphorus
tags:
except:
- tags
@@ -83,7 +83,7 @@ Mthread:
a3export:
stage: frama_c_and_plugins
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME a3export --base-branch stable/phosphorus
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME a3export --base-branch stable/phosphorus
tags:
except:
- tags
@@ -91,7 +91,7 @@ a3export:
PathCrawler:
stage: frama_c_and_plugins
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME PathCrawler --base-branch stable/phosphorus
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME PathCrawler --base-branch stable/phosphorus
tags:
except:
- tags
@@ -99,7 +99,7 @@ PathCrawler:
Security:
stage: frama_c_and_plugins
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Security --base-branch stable/phosphorus
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Security --base-branch stable/phosphorus
tags:
except:
- tags
@@ -107,7 +107,7 @@ Security:
E-ACSL:
stage: frama_c_and_plugins
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME E-ACSL --base-branch stable/phosphorus
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME E-ACSL --base-branch stable/phosphorus
tags:
except:
- tags
@@ -116,7 +116,15 @@ E-ACSL:
context-from-precondition:
stage: frama_c_and_plugins
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME context-from-precondition --base-branch stable/phosphorus
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME context-from-precondition --base-branch stable/phosphorus
+ tags:
+ except:
+ - tags
+
+ACSL-importer:
+ stage: frama_c_and_plugins
+ script:
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME ACSL-importer --base-branch stable/phosphorus
tags:
except:
- tags
@@ -126,4 +134,4 @@ context-from-precondition:
# - "echo \"Parameters: commit is $CI_BUILD_REF, branch is $CI_BUILD_REF_NAME\""
# tags:
# except:
-# - tags
\ No newline at end of file
+# - tags
diff --git a/Changelog b/Changelog
index f986d8ac476ce16e1a099ec44266b0b82dff93d7..42e2b5c84f07b319d143b6f137163828744eda17 100644
--- a/Changelog
+++ b/Changelog
@@ -22,6 +22,8 @@ Open Source Release <next-release>
Open Source Release Phosphorus-20170501
#######################################
+-* Kernel [2017/05/08] Fix various typos in source code and user messages.
+ Patch by Debian. Fixes #2323
-* Eva [2017/05/08] Fix widening in the gauges domain, in particular with
nested loops and pointers that change base address through
iterations
diff --git a/Makefile b/Makefile
index 0d834964c898ce359a8730c85a81574264e2c90a..e98014520c585569a078c9a842b00b0b929c633d 100644
--- a/Makefile
+++ b/Makefile
@@ -231,6 +231,7 @@ DISTRIB_FILES:=\
VERSION $(wildcard licenses/*) \
$(LIBC_FILES) \
$(wildcard share/emacs/*.el) share/autocomplete_frama-c \
+ share/_frama-c \
share/configure.ac \
share/Makefile.config.in share/Makefile.common \
share/Makefile.generic \
@@ -1531,7 +1532,7 @@ install:: install-lib
$(wildcard share/*.c share/*.h) \
share/Makefile.dynamic share/Makefile.plugin.template share/Makefile.kernel \
share/Makefile.config share/Makefile.common share/Makefile.generic \
- share/configure.ac share/autocomplete_frama-c \
+ share/configure.ac share/autocomplete_frama-c share/_frama-c \
$(FRAMAC_DATADIR)
$(MKDIR) $(FRAMAC_DATADIR)/emacs
$(CP) $(wildcard share/emacs/*.el) $(FRAMAC_DATADIR)/emacs
diff --git a/configure.in b/configure.in
index e69581569f00cf14de9621a8f67de78134ff186c..2144a54b58164afe13af258597cb3b71a0c6c87c 100644
--- a/configure.in
+++ b/configure.in
@@ -883,7 +883,8 @@ if ($OCAMLOPT -shared -linkall -o test_dynlink.cmxs test_dynlink.ml) \
then
AC_MSG_RESULT([native dynlink works fine. Great.])
else
- AC_MSG_ERROR([native dynlink does not work.])
+ AC_MSG_WARN([Native dynlink does not work, disabling native compilation.])
+ OCAMLBEST=byte
fi
rm -f test_dynlink.*
diff --git a/headers/headache_config.txt b/headers/headache_config.txt
index c3cebe95c2de5206b7d59f12ae408cba1763a50b..46c5c602eb3359a579d4305ad5703219d670a13a 100644
--- a/headers/headache_config.txt
+++ b/headers/headache_config.txt
@@ -34,6 +34,8 @@
#################
| ".*\.sh" -> frame open:"#" line:"#" close:"#"
| "autocomplete_frama-c" -> frame open: "#" line: "#" close: "#"
+| "_frama-c" -> frame open: "#" line: "#" close: "#"
+| ".*_frama-c" -> skip match:"#compdef.*"
################
# Perl scripts #
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 8cda3ea0889caae39c052bf311d92408687ca9d7..6107763c0778154fd54bf1bc3898b7bb4b9056e7 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -108,6 +108,7 @@ opam/opam: .ignore
ptests/.gitignore: .ignore
ptests/.merlin: .ignore
ptests/ptests.ml: CEA_LGPL
+share/_frama-c: CEA_LGPL
share/autocomplete_frama-c: CEA_LGPL
share/Makefile.clean: CEA_LGPL
share/Makefile.common: CEA_LGPL
diff --git a/man/frama-c.1 b/man/frama-c.1
index fac74bcdbeb0706d72c9df0349fbf55c2402c8d4..5801d7b53d3c22890ac3bb6896b587324ed6670f 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -404,14 +404,14 @@ alias of
.TP
.B -print-plugin-path
outputs the directory where Frama-C searches its plugins
-(can be overidden by the
+(can be overridden by the
.B FRAMAC_PLUGIN
variable and the
.B -add-path
option)
.TP
.B -print-share-path
-outputs the directory where Frama-C stores its data (can be overidden by the
+outputs the directory where Frama-C stores its data (can be overridden by the
.B FRAMAC_SHARE
variable)
.TP
diff --git a/share/Makefile.dynamic b/share/Makefile.dynamic
index fbdd26a5cf855d1d08dc78544a5f998b59ae1103..c12e946d6137fab54f399800628fc9c288fbf0c7 100644
--- a/share/Makefile.dynamic
+++ b/share/Makefile.dynamic
@@ -188,14 +188,18 @@ $(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
TARGETS := $(TARGET_META) $(TARGET_CMI)
TARGETS_TOP := $(TARGET_TOP_CMO) $(TARGET_TOP_CMX) \
$(TARGET_TOP_CMA) $(TARGET_TOP_CMXS)
-TARGETS_GUI := $(TARGET_GUI_CMI) $(TARGET_GUI_CMO) \
- $(TARGET_GUI_CMX) $(TARGET_GUI_CMXS)
+TARGETS_GUI_BYTE := $(TARGET_GUI_CMI) $(TARGET_GUI_CMO)
+TARGETS_GUI := $(TARGETS_GUI_BYTE) $(TARGET_GUI_CMX) $(TARGET_GUI_CMXS)
TARGETS_BYTE:= $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMO) $(TARGET_TOP_CMA)
TARGETS_OPT:= $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMX) $(TARGET_TOP_CMXS)
byte:: $(TARGETS_BYTE)
opt:: $(TARGETS_OPT)
+ifeq ($(OCAMLBEST),byte)
+gui:: $(TARGETS_GUI_BYTE)
+else
gui:: $(TARGETS_GUI)
+endif
# do not define additional targets if you come from the Frama-C Makefile
ifneq ($(FRAMAC_INTERNAL),yes)
diff --git a/share/_frama-c b/share/_frama-c
index 9ae7aae8e22a73956bacc29136048a19daae1e28..51ac788669e9b56fb1aab86996a02cc53df5eb2f 100644
--- a/share/_frama-c
+++ b/share/_frama-c
@@ -1,4 +1,25 @@
#compdef frama-c frama-c-gui frama-c.byte frama-c-gui.byte
+##########################################################################
+# #
+# 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). #
+# #
+##########################################################################
# zsh completion for Frama-C
# ==========================
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index c23460a1440d8431d65e576457847acd11496968..1c789137ad35794b5831805a830d2d30d3a7403e 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -543,7 +543,7 @@ and varinfo = {
(**
- For global variables, true iff the variable or function
is defined in the file.
- - For local variables, true iff the variable is explicitely initialized
+ - For local variables, true iff the variable is explicitly initialized
at declaration time.
- Unused for formals variables and logic variables.
*)
diff --git a/src/plugins/scope/dpds_gui.ml b/src/plugins/scope/dpds_gui.ml
index c7b2a0164ff1fefdaf004ebf2250f3a09ad86324..82cb8680aff3abfa150886c472c307d17642bb08 100644
--- a/src/plugins/scope/dpds_gui.ml
+++ b/src/plugins/scope/dpds_gui.ml
@@ -379,7 +379,7 @@ let help (main_ui:Design.main_window_extension_points) =
^"and the data is the one that is selected if any, "
^"or it can be given via a popup.\n"
^"\tIf the text given in the popup is empty, or 'Cancel' is chosen, "
- ^"the selection of the command is reseted.");
+ ^"the selection of the command is reset.");
add (ShowDef.help);
add (Zones.help);
add (DataScope.help);
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 20b772b14830e256932201d5220b015dc6acb1bd..5ccfc99b13b65c355737c7265fa916cc0def1161 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -460,11 +460,11 @@ module G = struct
(* Widen [i1] and [i2]. The number of iterations is widened only if
[widen_nb] holds. *)
- let widen stmt ~widen_nb i1 i2 =
+ let widen _stmt ~widen_nb i1 i2 =
let nb =
if widen_nb then
let threshold =
- if false then LoopAnalysis.Loop_analysis.get_bounds stmt else None
+ None (* LoopAnalysis.Loop_analysis.get_bounds _stmt *)
in
let threshold = Extlib.opt_map Integer.of_int threshold in
let (min, max as w) = Bounds.widen ?threshold i1.nb i2.nb in
diff --git a/src/plugins/wp/GuiProver.ml b/src/plugins/wp/GuiProver.ml
index 6706138076b9570ca9539dc1126a1857ce5d485e..3804a1e996bbc927e4774b5a595496a98580ed2d 100644
--- a/src/plugins/wp/GuiProver.ml
+++ b/src/plugins/wp/GuiProver.ml
@@ -165,7 +165,7 @@ class prover ~(console:Wtext.text) ~prover =
Pretty_utils.ksfprintf self#set_label "%a" VCS.pp_prover prover ;
| VCS.Computing signal ->
self#set_status `EXECUTE ;
- self#set_action ~tooltip:"Interrrupt Prover" ~icon:`STOP ~callback:signal () ;
+ self#set_action ~tooltip:"Interrupt Prover" ~icon:`STOP ~callback:signal () ;
Pretty_utils.ksfprintf self#set_label "%a (...)" VCS.pp_prover prover ;
| VCS.Valid | VCS.Checked ->
self#set_status ok_status ;
diff --git a/src/plugins/wp/Strategy.ml b/src/plugins/wp/Strategy.ml
index 008b61cad7543c14498751ec9b0f1dbea76d5855..d4a01882c615a4cdc8e4a54a7703598dd4e1264e 100644
--- a/src/plugins/wp/Strategy.ml
+++ b/src/plugins/wp/Strategy.ml
@@ -131,7 +131,7 @@ let registry = ref Tmap.empty
let register s =
let id = s#id in
if Tmap.mem id !registry then
- Wp_parameters.error "Strategy #%s already registered (skiped)" id
+ Wp_parameters.error "Strategy #%s already registered (skipped)" id
else
registry := Tmap.add id (s :> heuristic) !registry
diff --git a/src/plugins/wp/Tactical.ml b/src/plugins/wp/Tactical.ml
index 1afdf92f09711111138d6e5c8c4f0ed914d44be8..273f82cbc9199dd1430524088b2d63524adf9cdc 100644
--- a/src/plugins/wp/Tactical.ml
+++ b/src/plugins/wp/Tactical.ml
@@ -53,7 +53,7 @@ let rec insert_group cc = function
let add_composer (c : #composer) =
let id = c#id in
if Tmap.mem id !composers then
- Wp_parameters.error "Composer #%s already registered (skiped)" id
+ Wp_parameters.error "Composer #%s already registered (skipped)" id
else
begin
composers := Tmap.add id (c :> composer) !composers ;
@@ -404,7 +404,7 @@ let tacticals = ref Tmap.empty
let register t =
let id = t#id in
if Tmap.mem id !tacticals then
- Wp_parameters.error "Tactical #%s already registered (skiped)" id
+ Wp_parameters.error "Tactical #%s already registered (skipped)" id
else
tacticals := Tmap.add id (t :> t) !tacticals
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 1fb99f9c876c78252f1d6ecbfefdfdccfa4fc8e5..82a4998a0ec110ba58fe86dbac441a3884999014 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -276,7 +276,7 @@ module SplitDepth =
let option_name = "-wp-split-depth"
let default = 0
let arg_name = "p"
- let help = "Set depth of exploration for spliting conjunctions into sub-goals.\n\
+ let help = "Set depth of exploration for splitting conjunctions into sub-goals.\n\
Value `-1` means an unlimited depth."
end)
@@ -681,7 +681,7 @@ module TruncPropIdFileName =
let option_name = "-wp-filename-truncation"
let default = 60
let arg_name = "n"
- let help = "Truncate basename of proof obligation files after <n> characters. Since numbers can be added as suffixes to make theses names unique, filename lengths can be highter to <n>. No truncation is performed when the value equals to zero (defaut: 60)."
+ let help = "Truncate basename of proof obligation files after <n> characters. Since numbers can be added as suffixes to make theses names unique, filename lengths can be highter to <n>. No truncation is performed when the value equals to zero (default: 60)."
end)