Skip to content
Snippets Groups Projects
Commit 79fba679 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[kernel] documentation for Ast_info functions related to integer constant expr

and update is_null_expr and is_non_null_expr in a similar manner as the other ones
parent ec19fdd8
No related branches found
No related tags found
No related merge requests found
......@@ -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
(* ************************************************************************** *)
......
......@@ -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
(* ************************************************************************** *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment