diff --git a/dev/git-hooks/pre-commit.sh b/dev/git-hooks/pre-commit.sh
index 4eaa0428ca6da4b9d88592ca08bc7622cdc05f4d..3f376ce71e3bb85da9bb1c3ca551bfd4905875f3 100755
--- a/dev/git-hooks/pre-commit.sh
+++ b/dev/git-hooks/pre-commit.sh
@@ -41,6 +41,6 @@ if [ "$?" != "0" ]; then
echo " They will be verified only for a 'git commit -a' command."
fi
-# Verifies the current version of files
-make lint.before-commit-a
-make check-headers.before-commit-a
+# Verifies the current version of the files
+make lint.before-commit-a || exit 1
+make check-headers.before-commit-a || exit 1
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index e0e40434a36cdf33479f24bebc5c0b75d4f2f0c5..6a7c3479324d7d851433e48913baa68d29943e4d 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -39,7 +39,7 @@ let rec possible_value_of_integral_const = function
| _ -> None
and possible_value_of_integral_expr e =
- match e.enode with
+ match (Cil.constFold true e).enode with
| Const c -> possible_value_of_integral_const c
| _ -> None
@@ -53,16 +53,20 @@ let value_of_integral_expr e =
| None -> assert false
| Some i -> i
-let rec is_null_expr e = match e.enode with
+let rec uncast e = match e.enode with
+ | CastE(_,e) -> uncast e
+ | _ -> e
+
+let is_null_expr e =
+ match (uncast (Cil.constFold true e)).enode with
| Const c when is_integral_const c ->
Integer.equal (value_of_integral_const c) Integer.zero
- | CastE(_,e) -> is_null_expr e
| _ -> false
-let rec is_non_null_expr e = match e.enode with
+let is_non_null_expr e =
+ match (uncast (Cil.constFold true e)).enode with
| Const c when is_integral_const c ->
not (Integer.equal (value_of_integral_const c) Integer.zero)
- | CastE(_,e) -> is_non_null_expr e
| _ -> false
(* ************************************************************************** *)
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index 0aa8ba37d6d88ca10c3049d78c8bdb8804905aac..047293232cb10bb13703fc8693db5aa7189e2093 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -28,12 +28,59 @@ open Cil_types
(** {2 Expressions} *)
(* ************************************************************************** *)
+(** [true] iff the constant is an integer constant
+ (i.e. neither a float nor a string). Enum tags and chars
+ are integer constants.
+*)
val is_integral_const: constant -> bool
+
+(** returns the value of the corresponding integer literal or [None]
+ if the constant is not an integer (i.e. {!is_integral_const} returns false).
+*)
val possible_value_of_integral_const: constant -> Integer.t option
+
+(** returns the value of the corresponding integer constant expression, or
+ [None] if the expression is not a constant expression or does not
+ evaluate to an integer constant.
+
+ @before Frama-C+dev the function only returned [Some v] when the
+ expression was an integer literal (i.e. [Const c]).
+*)
val possible_value_of_integral_expr: exp -> Integer.t option
+
+(** returns the value of the corresponding integer literal. It is
+ the responsability of the caller to ensure the constant is indeed
+ an integer constant. If unsure, use {!possible_value_of_integral_const}.
+*)
val value_of_integral_const: constant -> Integer.t
+
+(** returns the value of the corresponding integer constant expression. It
+ is the responsibility of the caller to ensure that the argument is indeed
+ an integer constant expression. If unsure, use
+ {!possible_value_of_integral_expr}.
+
+ @before Frama-C+dev the function would fail if the expression was not an
+ integer literal (see {!possible_value_of_integral_expr}).
+*)
val value_of_integral_expr: exp -> Integer.t
+
+(** [true] iff the expression is a constant expression that evaluates to
+ a null pointer, i.e. 0 or a cast to 0.
+
+ @before Frama-C+dev the function would return [false] as soon as the
+ expression was not an integer literal (possibly casted).
+*)
val is_null_expr: exp -> bool
+
+(** [true] iff the expression is a constant expression that evaluates to
+ a non-null pointer.
+
+ {b Warning:} note that for the purpose of this function [&x] is {i not} a
+ constant expression, hence the function will return [false] in this case.
+
+ @before Frama-C+dev the function would return [false] as soon as
+ the expression was not an integer literal (possibly casted).
+*)
val is_non_null_expr: exp -> bool
(* ************************************************************************** *)
diff --git a/tests/misc/local_array_non_literal_size.i b/tests/misc/local_array_non_literal_size.i
new file mode 100644
index 0000000000000000000000000000000000000000..c47ca9ebc4ffb0482d18de6b452c6ea766f3c4aa
--- /dev/null
+++ b/tests/misc/local_array_non_literal_size.i
@@ -0,0 +1,25 @@
+/* run.config
+ PLUGIN: @EVA_PLUGINS@
+ OPT: -eva -machdep gcc_x86_64
+*/
+
+void one_dim() {
+ int empty_array[3%1] = { };
+ int normal_array[3+1] = { 0, 1, 2, 3 };
+}
+
+void two_dim_literal() {
+ int empty_array[1][0] = { };
+ int normal_array[1][4] = { 0, 1, 2, 3 };
+}
+
+void two_dim_non_literal () {
+ int empty_array[1][3%1] = { };
+ int normal_array[1][3+1] = { 0, 1, 2, 3 };
+}
+
+int main() {
+ one_dim();
+ two_dim_literal();
+ two_dim_non_literal();
+}
diff --git a/tests/misc/oracle/local_array_non_literal_size.err.oracle b/tests/misc/oracle/local_array_non_literal_size.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/misc/oracle/local_array_non_literal_size.res.oracle b/tests/misc/oracle/local_array_non_literal_size.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6453531ae5fc4d538ebf5b79e3f1699c0fcc78d6
--- /dev/null
+++ b/tests/misc/oracle/local_array_non_literal_size.res.oracle
@@ -0,0 +1,41 @@
+[kernel] Parsing local_array_non_literal_size.i (no preprocessing)
+[kernel] local_array_non_literal_size.i:12: Warning:
+ declaration of array of 'zero-length arrays' ('int [0]`);
+ zero-length arrays are a compiler extension
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function one_dim:
+ normal_array[0] ∈ {0}
+ [1] ∈ {1}
+ [2] ∈ {2}
+ [3] ∈ {3}
+[eva:final-states] Values at end of function two_dim_literal:
+ normal_array[0][0] ∈ {0}
+ [0][1] ∈ {1}
+ [0][2] ∈ {2}
+ [0][3] ∈ {3}
+[eva:final-states] Values at end of function two_dim_non_literal:
+ normal_array[0][0] ∈ {0}
+ [0][1] ∈ {1}
+ [0][2] ∈ {2}
+ [0][3] ∈ {3}
+[eva:final-states] Values at end of function main:
+ __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 4 functions analyzed (out of 4): 100% coverage.
+ In these functions, 14 statements reached (out of 14): 100% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 0 warnings
+ by the Frama-C kernel: 0 errors 1 warning
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------