diff --git a/src/plugins/e-acsl/src/analyses/analyses_types.mli b/src/plugins/e-acsl/src/analyses/analyses_types.mli index 4a00a6fa9a2b5629c3fba2fc1e910939eaf43ef6..ea2ec78290d21a627390b476e49ef34f36767070 100644 --- a/src/plugins/e-acsl/src/analyses/analyses_types.mli +++ b/src/plugins/e-acsl/src/analyses/analyses_types.mli @@ -68,7 +68,7 @@ type annotation_kind = | Variant | RTE -(** Type of intervals infered by the interval inference *) +(** Type of intervals inferred by the interval inference *) type ival = | Ival of Ival.t | Float of fkind * float option (* a float constant, if any *) @@ -76,7 +76,8 @@ type ival = | Real | Nan -(** Type of types infered by the type inference for types representing numbers *) +(** Type of types inferred by the type inference for types representing + numbers *) type number_ty = | C_integer of ikind | C_float of fkind diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml index 78f303770149f250e3fd98ccdc61d705f72f2a71..e005bcb1db73cdb8464c4138f23885c869318ad1 100644 --- a/src/plugins/e-acsl/src/analyses/typing.ml +++ b/src/plugins/e-acsl/src/analyses/typing.ml @@ -423,7 +423,7 @@ let rec type_term | TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) -> assert (match ctx with - |None -> true + | None -> true | Some c -> Number_ty.compare c c_int >= 0); let ctx = ctx_relation ~profile t1 t2 in ignore (type_term ~use_gmp_opt:true ~ctx ~profile t1);