diff --git a/Changelog b/Changelog
index aacc4b81d5e9f897a7bc53bc49984711c81523be..eb55a0f193c38649f62eacc08d6d786ed110d9b2 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,10 @@
Open Source Release <next-release>
###############################################################################
+-* Kernel [2025-02-13] ACSL arrays can have an arbitrary term as length,
+ provided it can be evaluated to an integer constant.
+ Fixes ##2695 and #@1413
+o! Kernel [2025-02-13] Move some functions from Logic_typing to Logic_utils
o Kernel [2025-02-05] New parameter builder `Float` for decimal
command-line parameters.
o! Kernel [2025-02-05] Remove the parameter `Functor_info` for every
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index ddcd31fd94fbc2832557e86d476d56dc10232114..63bc207ce6c3e062ed1efad68f3e8476f871a0b8 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -715,9 +715,8 @@ constant:
;
array_size:
-| INT_CONSTANT { ASinteger $1 }
-| full_identifier { ASidentifier $1 }
-| /* empty */ { ASnone }
+| lexpr {Some $1}
+| /* empty */ { None }
;
var_spec_bis:
diff --git a/src/kernel_internals/typing/unfold_loops.ml b/src/kernel_internals/typing/unfold_loops.ml
index 00acccab823e4902ae8a27076c2dd69a95cd7b1c..0803899a600f3b5e300ffd8c0c5ac6c8ce620f2d 100644
--- a/src/kernel_internals/typing/unfold_loops.ml
+++ b/src/kernel_internals/typing/unfold_loops.ml
@@ -38,7 +38,7 @@ let empty_info =
let update_info global_find_init emitter info spec =
match spec with
- | {term_type=typ} when Logic_typing.is_integral_type typ ->
+ | {term_type=typ} when Logic_utils.is_integral_type typ ->
if Option.is_some info.unroll_number && not info.ignore_unroll then begin
Kernel.warning ~once:true ~current:true
"ignoring unfolding directive (directive already defined)";
diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
index 31981c9d5f412332dc646103ebb3ea71b9924730..8016760c61ce48ba1640a5496aa5fd4438946d4b 100644
--- a/src/kernel_services/analysis/logic_deps.ml
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -369,7 +369,7 @@ let populate_zone ctx visit cil_node current_zones =
(* Dependencies of [\initialized(p)] or [\dangling(p)] are the
dependencies of [*p]. *)
if is_same_label current_label lbl then (
- let typ = Logic_typing.type_of_pointed t.term_type in
+ let typ = Logic_utils.type_of_pointed t.term_type in
let tlv = Cil.mkTermMem ~addr:t ~off:TNoOffset in
let tlv' = Logic_const.term (TLval tlv) typ in
self#do_term_lval tlv';
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 30188295ad06b52857273e6ecf26fcdc767786d4..349ef74b0b63c4bfca82d4be35759ea7c323179d 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -26,10 +26,49 @@ open Format
open Pretty_utils
open Logic_ptree
-let print_array_size fmt = function
- | ASidentifier s
- | ASinteger s -> pp_print_string fmt s
- | ASnone -> ()
+let get_relation_string = function
+ Lt -> "<" | Gt -> ">" | Le -> "<=" | Ge -> ">=" | Eq -> "==" | Neq -> "!="
+
+let get_binop_string = function
+ Badd -> "+"
+ | Bsub -> "-"
+ | Bmul -> "*"
+ | Bdiv -> "/"
+ | Bmod -> "%"
+ | Bbw_and -> "&"
+ | Bbw_or -> "|"
+ | Bbw_xor -> "^"
+ | Blshift -> "<<"
+ | Brshift -> ">>"
+
+let get_unop_string = function
+ Uminus -> "-" | Ustar -> "*" | Uamp -> "&" | Ubw_not -> "~"
+
+let getParenthLevel e =
+ match e.lexpr_node with
+ | PLnamed _ -> 95
+ | PLlambda _ | PLlet _ | PLrange _ -> 90
+ | PLforall _ | PLexists _ -> 87
+ | PLimplies _ | PLiff _ -> 85
+ | PLand _ | PLor _ | PLxor _ -> 80
+ | PLif _ -> 77
+ | PLbinop (_,(Bbw_and | Bbw_or | Bbw_xor),_) -> 75
+ | PLrepeat _ -> 72
+ | PLrel _ -> 70
+ | PLbinop (_,(Badd|Bsub|Blshift|Brshift),_) -> 60
+ | PLbinop (_,(Bmul|Bdiv|Bmod),_) -> 40
+ | PLunop ((Uamp|Uminus|Ubw_not),_) | PLcast _ | PLnot _ -> 30
+ | PLunop (Ustar,_) | PLdot _ | PLarrow _ | PLarrget _
+ | PLsizeof _ | PLsizeofE _ -> 20
+ | PLapp _ | PLold _ | PLat _
+ | PLoffset _ | PLbase_addr _ | PLblock_length _
+ | PLupdate _ | PLinitField _ | PLinitIndex _
+ | PLvalid _ | PLvalid_read _ | PLobject_pointer _ | PLvalid_function _
+ | PLinitialized _ | PLdangling _
+ | PLallocable _ | PLfreeable _ | PLfresh _
+ | PLseparated _ | PLunion _ | PLinter _ -> 10
+ | PLvar _ | PLconstant _ | PLresult | PLnull | PLtypeof _ | PLtype _
+ | PLfalse | PLtrue | PLcomprehension _ | PLempty | PLset _ | PLlist _ -> 0
let print_constant fmt = function
| IntConstant s -> pp_print_string fmt s
@@ -37,7 +76,11 @@ let print_constant fmt = function
| StringConstant s -> fprintf fmt "\"%s\"" s
| WStringConstant s -> fprintf fmt "\"%s\"" s
-let rec print_logic_type name fmt typ =
+let rec print_array_size fmt = function
+ | Some lexpr -> print_lexpr fmt lexpr
+ | None -> ()
+
+and print_logic_type name fmt typ =
let pname = match name with
| Some d -> (fun fmt -> fprintf fmt "@ %t" d)
| None -> (fun _ -> ())
@@ -90,56 +133,12 @@ let rec print_logic_type name fmt typ =
in
print_logic_type (Some pname) fmt ret
-let print_typed_ident fmt (t,s) =
+and print_typed_ident fmt (t,s) =
print_logic_type (Some (fun fmt -> pp_print_string fmt s)) fmt t
-let print_quantifiers fmt l = pp_list ~sep:",@ " print_typed_ident fmt l
-
-let get_relation_string = function
- Lt -> "<" | Gt -> ">" | Le -> "<=" | Ge -> ">=" | Eq -> "==" | Neq -> "!="
-
-let get_binop_string = function
- Badd -> "+"
- | Bsub -> "-"
- | Bmul -> "*"
- | Bdiv -> "/"
- | Bmod -> "%"
- | Bbw_and -> "&"
- | Bbw_or -> "|"
- | Bbw_xor -> "^"
- | Blshift -> "<<"
- | Brshift -> ">>"
-
-let get_unop_string = function
- Uminus -> "-" | Ustar -> "*" | Uamp -> "&" | Ubw_not -> "~"
-
-let getParenthLevel e =
- match e.lexpr_node with
- | PLnamed _ -> 95
- | PLlambda _ | PLlet _ | PLrange _ -> 90
- | PLforall _ | PLexists _ -> 87
- | PLimplies _ | PLiff _ -> 85
- | PLand _ | PLor _ | PLxor _ -> 80
- | PLif _ -> 77
- | PLbinop (_,(Bbw_and | Bbw_or | Bbw_xor),_) -> 75
- | PLrepeat _ -> 72
- | PLrel _ -> 70
- | PLbinop (_,(Badd|Bsub|Blshift|Brshift),_) -> 60
- | PLbinop (_,(Bmul|Bdiv|Bmod),_) -> 40
- | PLunop ((Uamp|Uminus|Ubw_not),_) | PLcast _ | PLnot _ -> 30
- | PLunop (Ustar,_) | PLdot _ | PLarrow _ | PLarrget _
- | PLsizeof _ | PLsizeofE _ -> 20
- | PLapp _ | PLold _ | PLat _
- | PLoffset _ | PLbase_addr _ | PLblock_length _
- | PLupdate _ | PLinitField _ | PLinitIndex _
- | PLvalid _ | PLvalid_read _ | PLobject_pointer _ | PLvalid_function _
- | PLinitialized _ | PLdangling _
- | PLallocable _ | PLfreeable _ | PLfresh _
- | PLseparated _ | PLunion _ | PLinter _ -> 10
- | PLvar _ | PLconstant _ | PLresult | PLnull | PLtypeof _ | PLtype _
- | PLfalse | PLtrue | PLcomprehension _ | PLempty | PLset _ | PLlist _ -> 0
+and print_quantifiers fmt l = pp_list ~sep:",@ " print_typed_ident fmt l
-let rec print_path_elt fmt = function
+and print_path_elt fmt = function
| PLpathField s -> fprintf fmt ".%s" s
| PLpathIndex i -> fprintf fmt "[@[%a@]]" print_lexpr i
diff --git a/src/kernel_services/ast_queries/logic_to_c.ml b/src/kernel_services/ast_queries/logic_to_c.ml
index f75aef98facc4fdf163641521c73f6a4279cdc41..e5cb96743ee445a8c322e345b2c51b013b5c5d57 100644
--- a/src/kernel_services/ast_queries/logic_to_c.ml
+++ b/src/kernel_services/ast_queries/logic_to_c.ml
@@ -128,19 +128,19 @@ and loc_to_exp ?result {term_node = lnode ; term_type = ltype; term_loc = loc} =
| Tinter _ | Tcomprehension _ -> error_lval()
| Tat ({term_node = TAddrOf (TVar _, TNoOffset)} as taddroflval, _) ->
loc_to_exp ?result taddroflval
- | TCast (true, Linteger, t) when Logic_typing.is_integral_type t.term_type ->
+ | TCast (true, Linteger, t) when Logic_utils.is_integral_type t.term_type ->
loc_to_exp ?result t
- | TCast (true, Lreal, t) when Logic_typing.is_integral_type t.term_type ->
+ | TCast (true, Lreal, t) when Logic_utils.is_integral_type t.term_type ->
List.map
(fun x -> new_exp ~loc (CastE (logic_type_to_typ Lreal, x)))
(loc_to_exp ?result t)
- | TCast (true, Lreal, t) when Logic_typing.is_arithmetic_type t.term_type ->
+ | TCast (true, Lreal, t) when Logic_utils.is_arithmetic_type t.term_type ->
loc_to_exp ?result t
| TCast (true, set, t)
when
Logic_const.is_set_type set &&
Logic_utils.is_same_type
- (Logic_typing.type_of_set_elem set) t.term_type ->
+ (Logic_utils.type_of_set_elem set) t.term_type ->
loc_to_exp ?result t
| Tnull -> [ Cil.mkCast ~newt:(Cil_const.voidPtrType) (Cil.zero ~loc) ]
@@ -167,9 +167,9 @@ let rec loc_to_lval ?result t =
a coercion to set here.
*)
| TCast (true, set, t) when
- Logic_typing.is_set_type set &&
+ Logic_utils.is_set_type set &&
Logic_utils.is_same_type
- (Logic_typing.type_of_set_elem set) t.term_type ->
+ (Logic_utils.type_of_set_elem set) t.term_type ->
loc_to_lval ?result t
| Tinter _ -> error_lval() (* TODO *)
| Tcomprehension _ -> error_lval()
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 73ffdee63447b992dbfddf48f2b05eae91215ccd..dbb92a754748fc4ca242dad1c9b3d61f2dfc2528 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -101,14 +101,6 @@ let wcharlist_of_string s =
done;
List.rev (!res)
-let type_of_list_elem t = Logic_const.type_of_list_elem (unroll_type t)
-
-let is_list_type t = Logic_const.is_list_type (unroll_type t)
-
-let type_of_set_elem t = Logic_const.type_of_element (unroll_type t)
-
-let is_set_type t = Logic_const.is_set_type (unroll_type t)
-
let plain_mk_mem ?loc t ofs = match t.term_node with
| TAddrOf lv -> Logic_const.addTermOffsetLval ofs lv
| TStartOf lv ->
@@ -586,24 +578,6 @@ let rec arithmetic_conversion ty1 ty2 =
"arithmetic conversion between non arithmetic types %a and %a"
Cil_printer.pp_logic_type ty1 Cil_printer.pp_logic_type ty2
-let plain_arithmetic_type t = Cil.isLogicArithmeticType t
-let plain_integral_type t = Cil.isLogicIntegralType t
-let plain_boolean_type t = Cil.isLogicBooleanType t
-let plain_fun_ptr t = Cil.isLogicFunPtrType t
-
-let is_arithmetic_type = plain_or_set plain_arithmetic_type
-let is_integral_type = plain_or_set plain_integral_type
-let is_fun_ptr = plain_or_set plain_fun_ptr
-
-let rec type_of_pointed t =
- match unroll_type t with
- Ctype ty when isPointerType ty -> Ctype (Cil.typeOf_pointed ty)
- | Ltype ({lt_name = "set"} as lt,[t]) ->
- Ltype(lt,[type_of_pointed t])
- | _ ->
- Kernel.fatal ~current:true "type %a is not a pointer type"
- Cil_printer.pp_logic_type t
-
let rec ctype_of_pointed t =
match unroll_type t with
Ctype ty when isPointerType ty -> Cil.typeOf_pointed ty
@@ -612,15 +586,6 @@ let rec ctype_of_pointed t =
Kernel.fatal ~current:true "type %a is not a pointer type"
Cil_printer.pp_logic_type t
-let type_of_array_elem =
- plain_or_set
- (fun t ->
- match unroll_type t with
- Ctype ty when isArrayType ty -> Ctype (Cil.typeOf_array_elem ty)
- | _ ->
- Kernel.fatal ~current:true "type %a is not an array type"
- Cil_printer.pp_logic_type t)
-
let rec ctype_of_array_elem t =
match unroll_type t with
| Ctype ty when isArrayType ty -> Cil.typeOf_array_elem ty
@@ -635,19 +600,6 @@ let mk_mem ?loc t ofs =
(type_of_pointed t.term_type))
t
-let is_plain_array_type t =
- match unroll_type t with
- | Ctype ct -> Cil.isArrayType ct
- | _ -> false
-
-let is_plain_pointer_type t =
- match unroll_type t with
- | Ctype ct -> Cil.isPointerType ct
- | _ -> false
-
-let is_array_type = plain_or_set is_plain_array_type
-let is_pointer_type = plain_or_set is_plain_pointer_type
-
module type S =
sig
val type_of_field:
@@ -1047,6 +999,26 @@ struct
with Not_found ->
C.error loc "logic label `%s' not found" l
+ let rec size_exp ctxt loc size =
+ match size.term_node with
+ | TLval (TVar ({ lv_kind = LVGlobal } as lvar), TNoOffset) ->
+ begin (* logic variable, so try to unfold its definition *)
+ match Logic_env.find_logic_cons lvar with
+ | { l_labels = [] ; l_body = (LBterm term) ; l_profile = [] } ->
+ size_exp ctxt loc term
+ | _ -> raise Not_found
+ end
+ | _ ->
+ (match (Cil.constFoldTerm size).term_node with
+ | TConst (Integer _ | LChr _ | LEnum _) ->
+ (try
+ Logic_to_c.term_to_exp size
+ with
+ | Logic_to_c.No_conversion ->
+ ctxt.error loc "size of ACSL array cannot be represented in C")
+ | _ ->
+ ctxt.error loc "size of array must be a constant")
+
let logic_type ctxt loc env t =
(* force calls to go through ctxt *)
let module [@warning "-60"] C = struct end in
@@ -1057,38 +1029,15 @@ struct
| LTint ikind -> Ctype (Cil_const.mk_tint ikind)
| LTfloat fkind -> Ctype (Cil_const.mk_tfloat fkind)
| LTarray (ty,length) ->
-
- let size = match length with
- | ASnone -> None
- | ASinteger s ->
- let t = parseInt loc s in
- (match t.term_node with
- | TConst lconst ->
- Some (new_exp ~loc (Const (lconstant_to_constant lconst)))
- | _ -> Kernel.fatal ~loc "integer literal not parsed as constant")
- | ASidentifier s ->
- let size = ctxt.type_term ctxt env
- {lexpr_node=PLvar(s);lexpr_loc=loc} in
- if size.term_type <> Linteger then
- ctxt.error loc "size of array must be an integral value";
- try
- let rec size_exp size =
- match size.term_node with
- | TConst lconst -> (* the identifier was a macro to an integer *)
- Some (new_exp ~loc (Const (lconstant_to_constant lconst)))
- | TLval (TVar( {lv_kind=LVGlobal} as lvar), TNoOffset) ->
- begin (* logic variable, so try to unfold its definition *)
- match Logic_env.find_logic_cons lvar with
- | {l_labels=[];l_body=(LBterm term);l_profile=[]} ->
- size_exp term
- | _ -> raise Not_found
- end
- | _ -> raise Not_found
- in size_exp size
- with Not_found ->
- ctxt.error loc "size of array must be an integral value";
- in Ctype (Cil_const.mk_tarray (ctype ty) size)
-
+ begin match Option.map (ctxt.type_term ctxt env) length with
+ | None -> Ctype (Cil_const.mk_tarray (ctype ty) None)
+ | Some size ->
+ match size.term_type with
+ | Linteger ->
+ let size = Some (size_exp ctxt loc size) in
+ Ctype (Cil_const.mk_tarray (ctype ty) size)
+ | _ -> ctxt.error loc "size of array must be an integral value"
+ end
| LTpointer ty -> Ctype (Cil_const.mk_tptr (ctype ty))
| LTenum e ->
(try Ctype (ctxt.find_type Enum e)
@@ -1414,7 +1363,7 @@ struct
with
| Ctype oldt, Ctype newt ->
c_mk_cast ~force e oldt newt
- | t1, Lboolean when is_integral_type t1 ->
+ | t1, Lboolean when Logic_utils.is_integral_type t1 ->
let e = mk_cast e Linteger in
Logic_const.term ~loc (TBinOp(Ne,e,lzero ~loc())) Lboolean
| Lboolean, Linteger when explicit ->
@@ -1423,11 +1372,11 @@ struct
C.error loc "invalid implicit cast from %a to %a"
Cil_printer.pp_logic_type e.term_type
Cil_printer.pp_logic_type newt
- | Lboolean, Ctype t2 when is_integral_type newt && explicit ->
+ | Lboolean, Ctype t2 when Logic_utils.is_integral_type newt && explicit ->
Logic_const.term ~loc (TCast (false, Ctype t2,e)) newt
| ty1, Ltype({lt_name="set"},[ty2])
- when is_pointer_type ty1 &&
- is_plain_pointer_type ty2 &&
+ when Logic_utils.is_pointer_type ty1 &&
+ Logic_utils.plain_pointer_type ty2 &&
isLogicCharType (type_of_pointed ty2) ->
location_to_char_ptr e
| Ltype({lt_name = "set"},[_]), Ltype({lt_name="set"},[ty2]) ->
@@ -1583,8 +1532,8 @@ struct
if overloaded then raise Not_applicable
else C.error loc "%s" s)
| t1, Ltype ({lt_name = "set"},[t2]) when
- is_pointer_type t1 &&
- is_plain_pointer_type t2 &&
+ Logic_utils.is_pointer_type t1 &&
+ Logic_utils.plain_pointer_type t2 &&
isLogicCharType (type_of_pointed t2) ->
nt, location_to_char_ptr oterm
(* can convert implicitly a singleton into a set,
@@ -1770,7 +1719,7 @@ struct
| Ltype({lt_name = "set"}, [t1]), t2 ->
let (env, ot, nt) = partial_unif ~overloaded loc term t1 t2 env in
env, make_set_type ot, make_set_type nt
- | t1,t2 when plain_boolean_type t1 && plain_boolean_type t2 ->
+ | t1,t2 when Cil.isLogicBooleanType t1 && Cil.isLogicBooleanType t2 ->
env,ot,nt
| ((Ctype _ | Linteger | Lreal | Lboolean),
(Ctype _ | Linteger | Lreal | Lboolean)) ->
@@ -2042,16 +1991,14 @@ struct
let list_conversion loc t ot nt env =
if is_same_type ot nt then ot
- else if plain_integral_type ot && plain_integral_type nt then ot
- else if plain_arithmetic_type ot && plain_arithmetic_type nt then ot
+ else if Cil.isLogicIntegralType ot && Cil.isLogicIntegralType nt then ot
+ else if Cil.isLogicArithmeticType ot && Cil.isLogicArithmeticType nt then ot
else let _,_,t = partial_unif ~overloaded:false loc t ot nt env in
t
let list_promotion typ =
- if plain_integral_type typ then
- Linteger
- else if plain_arithmetic_type typ then
- Lreal
+ if Cil.isLogicIntegralType typ then Linteger
+ else if Cil.isLogicArithmeticType typ then Lreal
else typ
let list_coercion typ t =
@@ -2322,7 +2269,7 @@ struct
term_type = type2}
in
let (toff, t_off2, opt_idx_let), ofs_type =
- let check_type typ = plain_integral_type typ
+ let check_type typ = Cil.isLogicIntegralType typ
|| C.error loc "range is only allowed for last offset"
and mk_field f = TField(f,TNoOffset),TField(f,TNoOffset),(fun x -> x)
and mk_idx idx =
@@ -3238,7 +3185,7 @@ struct
f loc op (mk_cast t1 t) (mk_cast t2 t)
in
begin match op with
- | _ when plain_arithmetic_type ty1 && plain_arithmetic_type ty2 ->
+ | _ when Cil.isLogicArithmeticType ty1 && Cil.isLogicArithmeticType ty2 ->
conditional_conversion t1 t2
| Eq | Neq when isLogicPointer t1 && isLogicNull t2 ->
let t1 = mk_logic_pointer_or_StartOf t1 in
@@ -3292,7 +3239,7 @@ struct
| TStartOf lv
| Tat ({term_node = TStartOf lv}, _) ->
f lv t
- | TAddrOf lv when is_fun_ptr t.term_type ->
+ | TAddrOf lv when Logic_utils.is_fun_ptr t.term_type ->
f lv
{ t with
term_type = type_of_pointed t.term_type;
@@ -3305,7 +3252,7 @@ struct
and term_from f t =
let check_from t =
match t.term_node with
- | TAddrOf lv when is_fun_ptr t.term_type ->
+ | TAddrOf lv when Logic_utils.is_fun_ptr t.term_type ->
f lv
{ t with
term_type = type_of_pointed t.term_type;
@@ -3387,14 +3334,14 @@ struct
and type_int_term ctxt env t =
let module [@warning "-60"] C = struct end in
let tt = ctxt.type_term ctxt env t in
- if not (plain_integral_type tt.term_type) then
+ if not (Cil.isLogicIntegralType tt.term_type) then
ctxt.error t.lexpr_loc
"integer expected but %a found" Cil_printer.pp_logic_type tt.term_type;
tt
and type_bool_term ctxt env t =
let tt = ctxt.type_term ctxt env t in
- if not (plain_boolean_type tt.term_type) then
+ if not (Cil.isLogicBooleanType tt.term_type) then
ctxt.error t.lexpr_loc "boolean expected but %a found"
Cil_printer.pp_logic_type tt.term_type;
mk_cast tt Lboolean
@@ -4528,3 +4475,17 @@ struct
(fun _ -> rollback_transaction ())
end
+
+(* deprecated functions *)
+
+let is_arithmetic_type = Logic_utils.is_arithmetic_type
+let is_integral_type = Logic_utils.is_integral_type
+let is_fun_ptr = Logic_utils.is_fun_ptr
+let is_array_type = Logic_utils.is_array_type
+let is_pointer_type = Logic_utils.is_pointer_type
+let is_set_type = Logic_utils.is_set_type
+let is_list_type = Logic_utils.is_list_type
+let type_of_set_elem = Logic_utils.type_of_set_elem
+let type_of_list_elem = Logic_utils.type_of_list_elem
+let type_of_pointed = Logic_utils.type_of_pointed
+let type_of_array_elem = Logic_utils.type_of_array_elem
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 6b13c293e9010af73077887812faea826022d616..f12b1ebd22a3cf6fb855fdecb783bfadd3b1ab86 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -41,22 +41,6 @@ val type_binop: Logic_ptree.binop -> Cil_types.binop
val unescape: string -> string
val wcharlist_of_string: string -> int64 list
-val is_arithmetic_type: Cil_types.logic_type -> bool
-val is_integral_type: Cil_types.logic_type -> bool
-val is_set_type: Cil_types.logic_type -> bool
-val is_array_type: Cil_types.logic_type -> bool
-val is_pointer_type: Cil_types.logic_type -> bool
-
-(** @since Aluminium-20160501 *)
-val is_list_type: Cil_types.logic_type -> bool
-
-(** @since Aluminium-20160501 *)
-val type_of_list_elem : logic_type -> logic_type
-
-val type_of_pointed: logic_type -> logic_type
-val type_of_array_elem: logic_type -> logic_type
-val type_of_set_elem: logic_type -> logic_type
-
val ctype_of_pointed: logic_type -> typ
val ctype_of_array_elem: logic_type -> typ
@@ -361,3 +345,50 @@ val get_importer:
builder:module_builder ->
loc:Logic_ptree.location ->
string list -> unit
+
+(** / **)
+
+(* deprecated functions only used for migration *)
+val is_arithmetic_type: Cil_types.logic_type -> bool
+[@@migrate { repl = Logic_utils.is_arithmetic_type } ]
+[@@deprecated "use Logic_utils.is_arithmetic_type, or ocamlmig for migration"]
+
+val is_integral_type: Cil_types.logic_type -> bool
+[@@migrate { repl = Logic_utils.is_integral_type } ]
+[@@deprecated "use Logic_utils.is_integral_type, or ocamlmig for migration"]
+
+val is_fun_ptr: Cil_types.logic_type -> bool
+[@@migrate { repl = Logic_utils.is_fun_ptr } ]
+[@@deprecated "use Logic_utils.is_fun_ptr, or ocamlmig for migration"]
+
+val is_array_type: Cil_types.logic_type -> bool
+[@@migrate { repl = Logic_utils.is_array_type } ]
+[@@deprecated "use Logic_utils.is_array_type, or ocamlmig for migration"]
+
+val is_pointer_type: Cil_types.logic_type -> bool
+[@@migrate { repl = Logic_utils.is_pointer_type } ]
+[@@deprecated "use Logic_utils.is_pointer_type, or ocamlmig for migration"]
+
+val is_set_type: Cil_types.logic_type -> bool
+[@@migrate { repl = Logic_utils.is_set_type } ]
+[@@deprecated "use Logic_utils.is_set_type, or ocamlmig for migration"]
+
+val is_list_type: Cil_types.logic_type -> bool
+[@@migrate { repl = Logic_utils.is_list_type } ]
+[@@deprecated "use Logic_utils.is_list_type, or ocamlmig for migration"]
+
+val type_of_set_elem: logic_type -> logic_type
+[@@migrate { repl = Logic_utils.type_of_set_elem } ]
+[@@deprecated "use Logic_utils.type_of_set_elem, or ocamlmig for migration"]
+
+val type_of_list_elem: logic_type -> logic_type
+[@@migrate { repl = Logic_utils.type_of_list_elem } ]
+[@@deprecated "use Logic_utils.type_of_list_elem, or ocamlmig for migration"]
+
+val type_of_pointed: logic_type -> logic_type
+[@@migrate { repl = Logic_utils.type_of_pointed }]
+[@@deprecated "use Logic_utils.type_of_pointed, or ocamlmig for migration"]
+
+val type_of_array_elem: logic_type -> logic_type
+[@@migrate { repl = Logic_utils.type_of_array_elem }]
+[@@deprecated "use Logic_utils.type_of_array_elem, or ocamlmig for migration"]
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index f652344a316ef66245991c1b7f5299b0d7c23d2e..6def39ffbe979ad52c59a03c08607a28bbcd3077 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -72,6 +72,51 @@ let is_instance_of vars t1 t2 =
(** {1 From C to logic}*)
(* ************************************************************************* *)
+let plain_arithmetic_type t = Cil.isLogicArithmeticType t
+let plain_integral_type t = Cil.isLogicIntegralType t
+let plain_fun_ptr t = Cil.isLogicFunPtrType t
+
+let is_arithmetic_type = plain_or_set plain_arithmetic_type
+let is_integral_type = plain_or_set plain_integral_type
+let is_fun_ptr = plain_or_set plain_fun_ptr
+
+let is_list_type t = Logic_const.is_list_type (unroll_type t)
+let type_of_list_elem t = Logic_const.type_of_list_elem (unroll_type t)
+
+let is_set_type t = Logic_const.is_set_type (unroll_type t)
+let type_of_set_elem t = Logic_const.type_of_element (unroll_type t)
+
+let plain_array_type t =
+ match unroll_type t with
+ | Ctype ct -> Cil.isArrayType ct
+ | _ -> false
+
+let plain_pointer_type t =
+ match unroll_type t with
+ | Ctype ct -> Cil.isPointerType ct
+ | _ -> false
+
+let is_array_type = plain_or_set plain_array_type
+let is_pointer_type = plain_or_set plain_pointer_type
+
+let type_of_array_elem =
+ Logic_const.transform_element
+ (fun t ->
+ match unroll_type t with
+ Ctype ty when isArrayType ty -> Ctype (Cil.typeOf_array_elem ty)
+ | _ ->
+ Kernel.fatal ~current:true "type %a is not an array type"
+ Cil_datatype.Logic_type.pretty t)
+
+let type_of_pointed =
+ Logic_const.transform_element
+ (fun t ->
+ match unroll_type t with
+ Ctype ty when isPointerType ty -> Ctype (Cil.typeOf_pointed ty)
+ | _ ->
+ Kernel.fatal ~current:true "type %a is not a pointer type"
+ Cil_datatype.Logic_type.pretty t)
+
let isLogicType f t = plain_or_set (Logic_const.isLogicCType f) t
(** true if the type is a C array (or a set of)*)
@@ -1266,15 +1311,37 @@ let is_same_pl_constant c1 c2 =
| (IntConstant _| FloatConstant _
| StringConstant _ | WStringConstant _), _ -> false
-let is_same_pl_array_size c1 c2 =
+let is_same_unop op1 op2 =
+ let open Logic_ptree in
+ match op1,op2 with
+ | Uminus, Uminus
+ | Ubw_not, Ubw_not
+ | Ustar, Ustar
+ | Uamp, Uamp -> true
+ | (Uminus | Ustar | Uamp | Ubw_not), _ -> false
+
+let is_same_binop op1 op2 =
let open Logic_ptree in
+ match op1, op2 with
+ | Badd, Badd | Bsub, Bsub | Bmul, Bmul | Bdiv, Bdiv | Bmod, Bmod
+ | Bbw_and, Bbw_and | Bbw_or, Bbw_or | Bbw_xor, Bbw_xor
+ | Blshift, Blshift | Brshift, Brshift -> true
+ | (Badd | Bsub | Bmul | Bdiv | Bmod | Bbw_and | Bbw_or
+ | Bbw_xor | Blshift | Brshift),_ -> false
+
+let is_same_relation r1 r2 =
+ let open Logic_ptree in
+ match r1, r2 with
+ | Lt, Lt | Gt, Gt | Le, Le | Ge, Ge | Eq, Eq | Neq, Neq -> true
+ | (Lt | Gt | Le | Ge | Eq | Neq), _ -> false
+
+let rec is_same_pl_array_size c1 c2 =
match c1,c2 with
- | ASnone, ASnone -> true
- | ASinteger s1, ASinteger s2
- | ASidentifier s1, ASidentifier s2 -> s1 = s2
- | (ASnone | ASinteger _| ASidentifier _), _ -> false
+ | None, None -> true
+ | Some e1, Some e2 -> is_same_lexpr e1 e2
+ | _, _ -> false
-let rec is_same_pl_type t1 t2 =
+and is_same_pl_type t1 t2 =
let open Logic_ptree in
match t1, t2 with
| LTvoid, LTvoid
@@ -1319,34 +1386,10 @@ let rec is_same_pl_type t1 t2 =
| LTunion _ | LTnamed _ | LTstruct _ | LTattribute _),_ ->
false
-let is_same_quantifiers =
- is_same_list (fun (t1,x1) (t2,x2) -> x1 = x2 && is_same_pl_type t1 t2)
-
-let is_same_unop op1 op2 =
- let open Logic_ptree in
- match op1,op2 with
- | Uminus, Uminus
- | Ubw_not, Ubw_not
- | Ustar, Ustar
- | Uamp, Uamp -> true
- | (Uminus | Ustar | Uamp | Ubw_not), _ -> false
-
-let is_same_binop op1 op2 =
- let open Logic_ptree in
- match op1, op2 with
- | Badd, Badd | Bsub, Bsub | Bmul, Bmul | Bdiv, Bdiv | Bmod, Bmod
- | Bbw_and, Bbw_and | Bbw_or, Bbw_or | Bbw_xor, Bbw_xor
- | Blshift, Blshift | Brshift, Brshift -> true
- | (Badd | Bsub | Bmul | Bdiv | Bmod | Bbw_and | Bbw_or
- | Bbw_xor | Blshift | Brshift),_ -> false
-
-let is_same_relation r1 r2 =
- let open Logic_ptree in
- match r1, r2 with
- | Lt, Lt | Gt, Gt | Le, Le | Ge, Ge | Eq, Eq | Neq, Neq -> true
- | (Lt | Gt | Le | Ge | Eq | Neq), _ -> false
+and is_same_quantifiers qs1 qs2 =
+ is_same_list (fun (t1,x1) (t2,x2) -> x1 = x2 && is_same_pl_type t1 t2) qs1 qs2
-let rec is_same_path_elt p1 p2 =
+and is_same_path_elt p1 p2 =
let open Logic_ptree in
match p1, p2 with
PLpathField s1, PLpathField s2 -> s1 = s2
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 3b30f7059955a60b217bd38ddf29fff09da98441..976924b3f1dec9cf06f8071a900c7c0a3b335918 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -75,13 +75,56 @@ val is_instance_of: string list -> logic_type -> logic_type -> bool
[true] (this is the default), C typedef will be expanded as well. *)
val unroll_type : ?unroll_typedef:bool -> logic_type -> logic_type
+(** {3 tests and extraction of element type}
+ @before Frama-C+dev these function were in {!Logic_typing}
+*)
+(** {4 tests for an individual (non set) type}
+ [plain_xxx t] returns [true] iff [t] is a [xxx]
+ @before Frama-C+dev these functions were not exported
+*)
+
+val plain_arithmetic_type: Cil_types.logic_type -> bool
+val plain_integral_type: Cil_types.logic_type -> bool
+val plain_fun_ptr: Cil_types.logic_type -> bool
+val plain_array_type: Cil_types.logic_type -> bool
+val plain_pointer_type: Cil_types.logic_type -> bool
+
+(** {4 tests for potential sets}
+ [is_xxx t] returns true iff [t] is a [xxx] _or_ a set of [xxx]
+*)
+
+val is_arithmetic_type: Cil_types.logic_type -> bool
+val is_integral_type: Cil_types.logic_type -> bool
+val is_fun_ptr: Cil_types.logic_type -> bool
+val is_array_type: Cil_types.logic_type -> bool
+val is_pointer_type: Cil_types.logic_type -> bool
+
+(** {4 sets and lists} *)
+
+val is_list_type: Cil_types.logic_type -> bool
+val is_set_type: Cil_types.logic_type -> bool
+
+(** {4 extract elements} *)
+
+val type_of_set_elem: logic_type -> logic_type
+val type_of_list_elem : logic_type -> logic_type
+
+(** returns the type of the element pointed to by the type. If the
+ source type is a set of pointers, returns a set of elements.
+*)
+val type_of_pointed: logic_type -> logic_type
+
+(** same as {!type_of_pointed} but for arrays (or set of arrays). *)
+val type_of_array_elem: logic_type -> logic_type
+
+(** {3 Predefined tests over types} *)
+
(** [isLogicType test typ] is [false] for pure logic types and the result
of test for C types.
In case of a set type, the function tests the element type.
*)
val isLogicType : (typ -> bool) -> logic_type -> bool
-(** {3 Predefined tests over types} *)
val isLogicArrayType : logic_type -> bool
val isLogicCharType : logic_type -> bool
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index 8fb37977157888468abead725b04a22bf23d1f13..b9755bab3e444cea9b7ded208caecec2917cfd56 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -24,6 +24,18 @@
(* Logic parse trees *)
+type location = Cil_types.location
+
+(** comparison operators. *)
+type relation = Lt | Gt | Le | Ge | Eq | Neq
+
+(** arithmetic and logic binary operators. *)
+type binop = Badd | Bsub | Bmul | Bdiv | Bmod | Bbw_and | Bbw_or | Bbw_xor |
+ Blshift | Brshift
+
+(** unary operators. *)
+type unop = Uminus | Ustar | Uamp | Ubw_not
+
(** logic constants. *)
type constant =
IntConstant of string (** integer constant *)
@@ -31,14 +43,13 @@ type constant =
| StringConstant of string (** string constant *)
| WStringConstant of string (** wide string constant *)
-(** size of logic array. *)
-type array_size =
- ASinteger of string (** integer constant *)
- | ASidentifier of string (** a variable or macro*)
- | ASnone (** none *)
+(** size of logic array.
+ @before Frama-C+dev was a sum type with only integer constants and variables
+*)
+type array_size = lexpr option
(** logic types. *)
-type logic_type =
+and logic_type =
| LTvoid (** C void *)
| LTboolean (** booleans *)
| LTinteger (** mathematical integers. *)
@@ -54,25 +65,13 @@ type logic_type =
| LTarrow of logic_type list * logic_type
| LTattribute of logic_type * Cil_types.attribute (* Only const and volatile can appear here *)
-type location = Cil_types.location
-
(** quantifier-bound variables *)
-type quantifiers = (logic_type * string) list
-
-(** comparison operators. *)
-type relation = Lt | Gt | Le | Ge | Eq | Neq
-
-(** arithmetic and logic binary operators. *)
-type binop = Badd | Bsub | Bmul | Bdiv | Bmod | Bbw_and | Bbw_or | Bbw_xor |
- Blshift | Brshift
-
-(** unary operators. *)
-type unop = Uminus | Ustar | Uamp | Ubw_not
+and quantifiers = (logic_type * string) list
(** logical expression. The distinction between locations, terms and
predicate is done during typing.
*)
-type lexpr = {
+and lexpr = {
lexpr_node : lexpr_node; (** kind of expression. *)
lexpr_loc : location (** position in the source code. *)
}
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 95d12ef6ad397e5dd0c7f75db75d771945098cb6..badd56eec9b45343c2662e330b4774d0b31eec09 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -746,8 +746,8 @@ let type_expr metaenv env ?tr ?current e =
let t1 = e1.term_type in
let t2 = e2.term_type in
let t =
- if Logic_typing.is_arithmetic_type t1
- && Logic_typing.is_arithmetic_type t2
+ if Logic_utils.is_arithmetic_type t1
+ && Logic_utils.is_arithmetic_type t2
then
let t = Logic_typing.arithmetic_conversion t1 t2 in
Logic_const.term
@@ -757,22 +757,22 @@ let type_expr metaenv env ?tr ?current e =
(match bop with
| Logic_ptree.Badd
when
- Logic_typing.is_integral_type t2
+ Logic_utils.is_integral_type t2
&& Logic_utils.isLogicPointerType t1 ->
Logic_const.term (TBinOp (PlusPI,e1,e2)) t1
| Logic_ptree.Bsub
when
- Logic_typing.is_integral_type t2
+ Logic_utils.is_integral_type t2
&& Logic_utils.isLogicPointerType t1 ->
Logic_const.term (TBinOp (MinusPI,e1,e2)) t1
| Logic_ptree.Badd
when
- Logic_typing.is_integral_type t1
+ Logic_utils.is_integral_type t1
&& Logic_utils.isLogicPointerType t2 ->
Logic_const.term (TBinOp (PlusPI,e2,e1)) t2
| Logic_ptree.Bsub
when
- Logic_typing.is_integral_type t1
+ Logic_utils.is_integral_type t1
&& Logic_utils.isLogicPointerType t2 ->
Logic_const.term (TBinOp (MinusPI,e2,e1)) t2
| Logic_ptree.Bsub
@@ -793,13 +793,13 @@ let type_expr metaenv env ?tr ?current e =
env, t, cond
| PUnop(Logic_ptree.Uminus,e) ->
let env,t,cond = aux env cond e in
- if Logic_typing.is_arithmetic_type t.term_type then
+ if Logic_utils.is_arithmetic_type t.term_type then
env,Logic_const.term (TUnOp (Neg,t)) Linteger,cond
else Aorai_option.abort
"Invalid operand for unary -: unexpected %a" Printer.pp_term t
| PUnop(Logic_ptree.Ubw_not,e) ->
let env,t,cond = aux env cond e in
- if Logic_typing.is_arithmetic_type t.term_type then
+ if Logic_utils.is_arithmetic_type t.term_type then
env,Logic_const.term (TUnOp (BNot,t)) Linteger,cond
else Aorai_option.abort
"Invalid operand for bitwise not: unexpected %a" Printer.pp_term t
@@ -823,7 +823,7 @@ let type_expr metaenv env ?tr ?current e =
env,
Logic_const.term
(TLval (TMem t, TNoOffset))
- (Logic_typing.type_of_pointed t.term_type),
+ (Logic_utils.type_of_pointed t.term_type),
cond
else
Aorai_option.abort "Cannot dereference term %a" Printer.pp_term t
@@ -832,19 +832,19 @@ let type_expr metaenv env ?tr ?current e =
let env, t2, cond = aux env cond e2 in
let t =
if Logic_utils.isLogicPointerType t1.term_type
- && Logic_typing.is_integral_type t2.term_type
+ && Logic_utils.is_integral_type t2.term_type
then
Logic_const.term
(TBinOp (PlusPI,t1,t2))
- (Logic_typing.type_of_pointed t1.term_type)
+ (Logic_utils.type_of_pointed t1.term_type)
else if Logic_utils.isLogicPointerType t2.term_type
- && Logic_typing.is_integral_type t1.term_type
+ && Logic_utils.is_integral_type t1.term_type
then
Logic_const.term
(TBinOp (PlusPI,t2,t1))
- (Logic_typing.type_of_pointed t2.term_type)
+ (Logic_utils.type_of_pointed t2.term_type)
else if Logic_utils.isLogicArrayType t1.term_type
- && Logic_typing.is_integral_type t2.term_type
+ && Logic_utils.is_integral_type t2.term_type
then
(match t1.term_node with
| TStartOf lv | TLval lv ->
@@ -852,20 +852,20 @@ let type_expr metaenv env ?tr ?current e =
(TLval
(Logic_const.addTermOffsetLval
(TIndex (t2, TNoOffset)) lv))
- (Logic_typing.type_of_array_elem t1.term_type)
+ (Logic_utils.type_of_array_elem t1.term_type)
| _ ->
Aorai_option.fatal
"Unsupported operation: %a[%a]"
Printer.pp_term t1 Printer.pp_term t2)
else if Logic_utils.isLogicArrayType t2.term_type
- && Logic_typing.is_integral_type t1.term_type
+ && Logic_utils.is_integral_type t1.term_type
then
(match t2.term_node with
| TStartOf lv | TLval lv ->
Logic_const.term
(TLval
(Logic_const.addTermOffsetLval (TIndex (t1, TNoOffset)) lv))
- (Logic_typing.type_of_array_elem t2.term_type)
+ (Logic_utils.type_of_array_elem t2.term_type)
| _ ->
Aorai_option.fatal
"Unsupported operation: %a[%a]"
@@ -891,7 +891,7 @@ let type_expr metaenv env ?tr ?current e =
if Logic_utils.isLogicPointerType t.term_type then begin
let off, ty =
LTyping.type_of_field loc s
- (Logic_typing.type_of_pointed t.term_type)
+ (Logic_utils.type_of_pointed t.term_type)
in
let lv = Logic_const.addTermOffsetLval off (TMem t,TNoOffset) in
env, Logic_const.term (TLval lv) ty, cond
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 045f1809d337ae24225724fe9db2a5a87ca7a039..2647a1a17b987b07f528b915d760acb4c0cdf961 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -360,7 +360,7 @@ let extract_quantifiers ~loc args =
eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers
in
let lty_noset =
- Logic_typing.type_of_pointed @@
+ Logic_utils.type_of_pointed @@
if Logic_const.is_set_type arg.term_type then
Logic_const.type_of_element arg.term_type
else
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index 72ac32a46788357e3fee60d36b7fcaa7173aa25f..e0e8e5929c58676462b4353cd6eac81ffdf3f611 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -325,7 +325,7 @@ and context_insensitive_term_to_exp_il ?inplace t =
let bop = Interlang_gen.binop bop in
let ty = Typing.get_typ ~logic_env t in
if not (Gmp_types.Z.is_t ty) && not (Gmp_types.Q.is_t ty) then
- assert (Logic_typing.is_integral_type t.term_type);
+ assert (Logic_utils.is_integral_type t.term_type);
M.return @@ IL.(Exp.of_exp_node ~origin:t @@
BinOp {ity; binop = bop; op1 = e1; op2 = e2})
| TBinOp((Lt | Gt | Le | Ge | Eq | Ne) as bop, t1, t2) ->
@@ -350,7 +350,7 @@ and context_insensitive_term_to_exp_il ?inplace t =
let ity = Typing.get_number_ty ~logic_env t in
let bop = Interlang_gen.binop binop in
if not (Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty) then
- assert (Logic_typing.is_integral_type t.term_type);
+ assert (Logic_utils.is_integral_type t.term_type);
M.return @@ IL.(Exp.of_exp_node ~origin:t @@
BinOp {ity; binop = bop; op1 = e1; op2 = e2})
| _ -> M.not_covered Printer.pp_term t
@@ -454,7 +454,7 @@ and context_insensitive_term_to_exp_old ~adata ?(inplace=false) kf env t =
let e, env = Gmp.Q.binop ~loc (Some t) bop env kf e1 e2 in
e, adata, env, Analyses_types.C_number, ""
else begin
- assert (Logic_typing.is_integral_type t.term_type);
+ assert (Logic_utils.is_integral_type t.term_type);
let e = Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)) in
e, adata, env, Analyses_types.C_number, ""
end
@@ -520,7 +520,7 @@ and context_insensitive_term_to_exp_old ~adata ?(inplace=false) kf env t =
let e, env = Gmp.Q.binop ~loc (Some t) bop env kf e1 e2 in
e, adata, env, Analyses_types.C_number, ""
else begin
- assert (Logic_typing.is_integral_type t.term_type);
+ assert (Logic_utils.is_integral_type t.term_type);
(* no guard required since RTEs are generated separately *)
let e2, adata, env = t2_to_exp adata env in
let e = Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)) in
@@ -724,7 +724,7 @@ and context_insensitive_term_to_exp_old ~adata ?(inplace=false) kf env t =
let e, env = Gmp.Z.new_var ~loc ~name env kf t mk_stmts in
e, adata, env, Analyses_types.C_number, ""
else begin
- assert (Logic_typing.is_integral_type t.term_type);
+ assert (Logic_utils.is_integral_type t.term_type);
let e1, adata, env = t1_to_exp adata env in
let e2, adata, env = t2_to_exp adata env in
let e = Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)) in
@@ -788,7 +788,7 @@ and context_insensitive_term_to_exp_old ~adata ?(inplace=false) kf env t =
let e, env = Gmp.Z.new_var ~loc ~name env kf t mk_stmts in
e, adata, env, Analyses_types.C_number, ""
else begin
- assert (Logic_typing.is_integral_type t.term_type);
+ assert (Logic_utils.is_integral_type t.term_type);
let e = Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)) in
e, adata, env, Analyses_types.C_number, ""
end
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 41cad438e9c73282b0e9a3d3ce13f8754b3c2ea3..0a645e1e49ced5a77f5e5a9b341a559fb0716e9d 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -1149,12 +1149,12 @@ let rec eval_term ~alarm_mode env t =
nothing to do, AND coercion from an integer type to a floating-point
type, that require a conversion. *)
(match Logic_const.plain_or_set Fun.id ltyp with
- | Linteger when Logic_typing.is_integral_type t.term_type
+ | Linteger when Logic_utils.is_integral_type t.term_type
|| Logic_const.is_boolean_type t.term_type -> r
| Ctype typ when Cil.isIntegralOrPointerType typ -> r
| Lreal ->
let eover =
- if Logic_typing.is_integral_type t.term_type
+ if Logic_utils.is_integral_type t.term_type
then V.cast_int_to_float Fval.Real r.eover
else V.cast_float_to_float Fval.Real r.eover
in
@@ -1164,7 +1164,7 @@ let rec eval_term ~alarm_mode env t =
empty = r.empty }
| ltyp ->
if Logic_const.is_boolean_type ltyp
- && Logic_typing.is_integral_type t.term_type
+ && Logic_utils.is_integral_type t.term_type
then cast_to_bool r
else if Logic_utils.is_same_type ltyp t.term_type then
(* coercion from singleton to set *)
diff --git a/src/plugins/wp/AssignsCompleteness.ml b/src/plugins/wp/AssignsCompleteness.ml
index 26faf49539775c73889972887f37be70b5763d83..3d02cf58c8a21234d6374b437337245c8f51ecec 100644
--- a/src/plugins/wp/AssignsCompleteness.ml
+++ b/src/plugins/wp/AssignsCompleteness.ml
@@ -127,7 +127,7 @@ let check_assigns kf assigns =
else acc
in
let vfrom acc = function
- | t, FromAny when Logic_typing.is_pointer_type t.it_content.term_type ->
+ | t, FromAny when Logic_utils.is_pointer_type t.it_content.term_type ->
incomplete acc
begin fun _kf ->
Wp_parameters.warning ~wkey:wkey_pedantic
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index f57fd630a5c5eb46781a6d21be88d3e5a54a6c35..1af43c04595fa5f057a01c983b58ff8d308ab7a4 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -501,8 +501,8 @@ let map_logic f = function
| Lset ls -> Lset (List.map (map_sloc f) ls)
let plain lt e =
- if Logic_typing.is_set_type lt then
- let te = Logic_typing.type_of_set_elem lt in
+ if Logic_utils.is_set_type lt then
+ let te = Logic_utils.type_of_set_elem lt in
Vset [Vset.Set(tau_of_ltype te,e)]
else
Vexp e
@@ -831,12 +831,12 @@ struct
| Vset s -> a.vset <- List.rev_append s a.vset
| Lset s -> a.sloc <- List.rev_append s a.sloc
) vs ;
- flush (Logic_typing.is_pointer_type t) a
+ flush (Logic_utils.is_pointer_type t) a
let inter t vs =
match List.map (fun v -> Vset.concretize (vset v)) vs with
| [] ->
- if Logic_typing.is_pointer_type t
+ if Logic_utils.is_pointer_type t
then Lset [] else Vset []
| v::vs ->
let s = List.fold_left Vset.inter v vs in
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 0496a6436a04c14d101e37663f0531fdfdfb0085..b81a2ee26a7d86ab0f4d041ada91002d317bad28 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -108,8 +108,8 @@ struct
let collection_of_term env t =
let v = C.logic env t in
match v with
- | Vexp s when Logic_typing.is_set_type t.term_type ->
- let te = Logic_typing.type_of_set_elem t.term_type in
+ | Vexp s when Logic_utils.is_set_type t.term_type ->
+ let te = Logic_utils.type_of_set_elem t.term_type in
Vset [Vset.Set(tau_of_ltype te,s)]
| w -> w
@@ -364,7 +364,7 @@ struct
| _ -> None
let compare_term env vrel lrel frel a b =
- if Logic_typing.is_pointer_type a.term_type then
+ if Logic_utils.is_pointer_type a.term_type then
lrel (loc_of_term env a) (loc_of_term env b)
else match float_of_logic_type a.term_type with
| Some f -> frel f (val_of_term env a) (val_of_term env b)
@@ -393,8 +393,8 @@ struct
let arith env fint freal a b =
let va = C.logic env a in
let vb = C.logic env b in
- let ta = Logic_typing.is_integral_type a.term_type in
- let tb = Logic_typing.is_integral_type b.term_type in
+ let ta = Logic_utils.is_integral_type a.term_type in
+ let tb = Logic_utils.is_integral_type b.term_type in
if ta && tb
then fint va vb
else freal (toreal ta va) (toreal tb vb)
@@ -665,7 +665,7 @@ struct
| _ -> base
end
- | TUnOp(Neg,t) when not (Logic_typing.is_integral_type t.term_type) ->
+ | TUnOp(Neg,t) when not (Logic_utils.is_integral_type t.term_type) ->
L.map F.e_opp (C.logic env t)
| TUnOp(unop,t) -> term_unop unop (C.logic env t)
| TBinOp(binop,a,b) -> term_binop env binop a b
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index b0910d07888573c343db91b9998557052bf37e35..e9587f382c05566fa230e3d2938739d3c160e5c3 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -112,8 +112,8 @@ open Logic_const
let rec ptr_of = function
| Ctype t -> Ctype (Cil_const.mk_tptr t)
- | t when Logic_typing.is_set_type t ->
- let t = Logic_typing.type_of_set_elem t in
+ | t when Logic_utils.is_set_type t ->
+ let t = Logic_utils.type_of_set_elem t in
Logic_const.make_set_type (ptr_of t)
| _ -> assert false
@@ -226,7 +226,7 @@ let normalize ps =
List.filter (fun p -> not(Logic_utils.is_trivially_true p)) ps
let ptrset { term_type = t } =
- let open Logic_typing in
+ let open Logic_utils in
is_pointer_type t || (is_set_type t && is_pointer_type (type_of_element t))
(* -------------------------------------------------------------------------- *)
diff --git a/tests/syntax/acsl_type_expression_array.c b/tests/syntax/acsl_type_expression_array.c
new file mode 100644
index 0000000000000000000000000000000000000000..3e35f4ad30a05197e4ddacb28447823991ca7173
--- /dev/null
+++ b/tests/syntax/acsl_type_expression_array.c
@@ -0,0 +1,14 @@
+#include <stddef.h>
+typedef struct sub_type {
+ int tag;
+} sub_type;
+
+typedef struct {
+ int *ptr;
+ int foo[sizeof(sub_type)];
+} TEST_TYPE;
+
+int main(){
+ size_t test = sizeof(int[sizeof(sub_type)]);
+ /*@ assert test == sizeof(int[sizeof(sub_type)]); */
+}
diff --git a/tests/syntax/oracle/acsl_type_expression_array.res.oracle b/tests/syntax/oracle/acsl_type_expression_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..fd1712a6d474cac27832626165f9ed47ea7175a5
--- /dev/null
+++ b/tests/syntax/oracle/acsl_type_expression_array.res.oracle
@@ -0,0 +1,17 @@
+[kernel] Parsing acsl_type_expression_array.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stddef.h"
+struct sub_type {
+ int tag ;
+};
+typedef struct sub_type sub_type;
+int main(void)
+{
+ int __retres;
+ size_t test = sizeof(int [sizeof(sub_type)]);
+ /*@ assert test ≡ sizeof(int [sizeof(sub_type)]); */ ;
+ __retres = 0;
+ return __retres;
+}
+
+