From 12cf9d55133b10b7b2cd19dbe6a7cd034d72e969 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 26 Mar 2020 16:07:15 +0100
Subject: [PATCH] [logic] grouping ocaml doc
---
.../ast_queries/logic_utils.ml | 33 +++++++++++--------
.../ast_queries/logic_utils.mli | 32 +++++++++++-------
2 files changed, 41 insertions(+), 24 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index ea652d98361..a77518acee2 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -263,6 +263,10 @@ let mk_cast ?(loc=Cil_datatype.Location.unknown) ?(force=false) newt t =
| _ -> mk_cast t
in aux1 t.term_type t
+(* -------------------------------------------------------------------------- *)
+(* --- Constant Conversions --- *)
+(* -------------------------------------------------------------------------- *)
+
let real_of_float s f =
{ r_literal = s ; r_nearest = f ; r_upper = f ; r_lower = f }
@@ -329,8 +333,7 @@ let numeric_coerce ltyp t =
| _ -> coerce t
(* Don't forget to keep is_zero_comparable
- and scalar_term_to_predicate in sync.
-*)
+ and scalar_term_to_predicate in sync. *)
let is_zero_comparable t =
match unroll_type t.term_type with
@@ -379,9 +382,13 @@ let scalar_term_to_boolean =
in
scalar_term_conversion conversion
+(* -------------------------------------------------------------------------- *)
+(* --- Expr Conversion --- *)
+(* -------------------------------------------------------------------------- *)
+
let rec expr_to_term ~cast e =
- let e_typ = unrollType (Cil.typeOf e) in
let loc = e.eloc in
+ let typ = unrollType (Cil.typeOf e) in
let result = match e.enode with
| Const c -> TConst (constant_to_lconstant c)
| SizeOf t -> TSizeOf t
@@ -400,7 +407,7 @@ let rec expr_to_term ~cast e =
| ( Cil_types.Lt | Cil_types.Gt | Cil_types.Le | Cil_types.Ge
| Cil_types.Eq | Cil_types.Ne| Cil_types.LAnd | Cil_types.LOr),
_ -> Some Logic_const.boolean_type
- | _, true -> Some (typ_to_logic_type e_typ)
+ | _, true -> Some (typ_to_logic_type typ)
| _, false -> None
in
let tnode = TBinOp (op,l',r') in
@@ -410,7 +417,7 @@ let rec expr_to_term ~cast e =
integer/float/pointer here, and (2) there is no implicit conversion
Boolean -> integer. *)
begin match tcast with
- | Some lt -> (mk_cast e_typ (Logic_const.term tnode lt)).term_node
+ | Some lt -> (mk_cast typ (Logic_const.term tnode lt)).term_node
| None -> tnode
end
| UnOp (op, u, _) ->
@@ -433,12 +440,12 @@ let rec expr_to_term ~cast e =
(* See comments for binop case above. *)
let tcast = match op, cast with
| Cil_types.LNot, _ -> Some Logic_const.boolean_type
- | _, true -> Some (typ_to_logic_type e_typ)
+ | _, true -> Some (typ_to_logic_type typ)
| _, false -> None
in
let tnode = TUnOp (op, u') in
begin match tcast with
- | Some lt -> (mk_cast e_typ (Logic_const.term tnode lt)).term_node
+ | Some lt -> (mk_cast typ (Logic_const.term tnode lt)).term_node
| None -> tnode
end
| AlignOfE e -> TAlignOfE (expr_to_term ~cast e)
@@ -446,14 +453,14 @@ let rec expr_to_term ~cast e =
| Lval lv -> TLval (lval_to_term_lval ~cast lv)
| Info (e,_) -> (expr_to_term ~cast e).term_node
in
- let tres = Logic_const.term ~loc result (Ctype e_typ) in
+ let tres = Logic_const.term ~loc result (Ctype typ) in
if cast then tres
else
match e.enode with
(* all immediate values keep their C type by default, and are only lifted
to integer/real if needed. *)
| Const _ | Lval _ | CastE _ -> tres
- | _ -> numeric_coerce (typ_to_logic_type e_typ) tres
+ | _ -> numeric_coerce (typ_to_logic_type typ) tres
and expr_to_term_coerce ~cast e =
let t = expr_to_term ~cast e in
@@ -497,6 +504,10 @@ and expr_to_predicate ~cast e =
"Cannot convert into predicate the C expression %a"
Cil_printer.pp_exp e
+(* ************************************************************************* *)
+(** {1 Various utilities} *)
+(* ************************************************************************* *)
+
let array_with_range arr size =
let loc = arr.eloc in
let arr = Cil.stripCasts arr in
@@ -521,10 +532,6 @@ let remove_logic_coerce t =
| TLogic_coerce(_,t) -> t
| _ -> t
-(* ************************************************************************* *)
-(** {1 Various utilities} *)
-(* ************************************************************************* *)
-
let rec remove_term_offset o =
match o with
TNoOffset -> TNoOffset, TNoOffset
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index b3a51cdf016..3853a02c250 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -157,8 +157,9 @@ val pointer_comparable: ?loc:location -> term -> term -> predicate
(** \pointer_comparable
@since Fluorine-20130401 *)
-(** {3 Conversion from exp to term}*)
-(** translates a C expression into an "equivalent" logical term.
+(** {2 Conversion from exp to term}
+
+ translates a C expression into an "equivalent" logical term.
[cast] specifies how C arithmetic operators are translated.
When [cast] is [true], the translation returns a logic [term] having the
same semantics of the C [expr] by introducing casts (i.e. the C expr [a+b]
@@ -169,6 +170,7 @@ val pointer_comparable: ?loc:location -> term -> term -> predicate
addition is translated into an addition of [real] numbers).
@plugin development guide *)
val expr_to_term : cast:bool -> exp -> term
+
(** same as {!expr_to_term}, except that if the new term has an arithmetic
type, it is automatically coerced into real (or integer for integral types).
@@ -176,13 +178,6 @@ val expr_to_term : cast:bool -> exp -> term
*)
val expr_to_term_coerce: cast:bool -> exp -> term
-val is_zero_comparable: term -> bool
-(** [true] if the given term has a type for which a comparison to 0 exists
- (i.e. scalar C types, logic integers and reals).
-
- @since Sulfur-20171101
-*)
-
val expr_to_predicate: cast:bool -> exp -> identified_predicate
(** same as {expr_to_term}, but the result is a predicate. Expressions starting
with relational operators ([==], [<=], etc) are translated directly.
@@ -194,6 +189,21 @@ val expr_to_predicate: cast:bool -> exp -> identified_predicate
@since Sulfur-20171101
*)
+val is_zero_comparable: term -> bool
+(** [true] if the given term has a type for which a comparison to 0 exists
+ (i.e. scalar C types, logic integers and reals).
+
+ @since Sulfur-20171101
+*)
+
+val scalar_term_to_boolean: term -> term
+(** Compare the given term with the constant 0 (of the appropriate type)
+ to return the result of the comparison [e <> 0] as a boolean term.
+
+ @raise Fatal error if the argument cannot be compared to 0
+ @since Frama-C+dev
+*)
+
val scalar_term_to_predicate: term -> predicate
(** Compare the given term with the constant 0 (of the appropriate type)
to return the result of the comparison [e <> 0].
@@ -216,6 +226,8 @@ val lconstant_to_constant: logic_constant-> constant
by the parser as valid floats *)
val string_to_float_lconstant: string -> logic_constant
+(** {2 Various Utilities} *)
+
(** [remove_term_offset o] returns [o] without its last offset and
this last offset. *)
val remove_term_offset :
@@ -240,8 +252,6 @@ val is_result : term -> bool
val lhost_c_type : term_lhost -> typ
-(** {2 Predicates} *)
-
(** [true] if the predicate is Ptrue.
@since Nitrogen-20111001 *)
val is_trivially_true: predicate -> bool
--
GitLab