diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml index 52c110ee0e55659eee21fb931dcca15defccbd22..6a7c3479324d7d851433e48913baa68d29943e4d 100644 --- a/src/kernel_services/ast_queries/ast_info.ml +++ b/src/kernel_services/ast_queries/ast_info.ml @@ -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..a82013636f9aa445ce2a675229e150f3a9bfd123 100644 --- a/src/kernel_services/ast_queries/ast_info.mli +++ b/src/kernel_services/ast_queries/ast_info.mli @@ -28,12 +28,46 @@ 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 constant +*) 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 + [None] if the expression is not a constant expression or does not + evaluate to an integer constant. +*) 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} +*) 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. *) 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. +*) val is_non_null_expr: exp -> bool (* ************************************************************************** *)