From e7d34cb18b26d6708fb2b7a7073fab72371536ba Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 13 Feb 2023 11:26:45 +0100
Subject: [PATCH] [Kernel] remove obsolete alarm uninitialized_union
---
ivette/src/frama-c/kernel/Properties.tsx | 4 --
.../frama-c/kernel/api/properties/index.ts | 2 -
src/kernel_services/ast_data/alarms.ml | 41 ++-----------------
src/kernel_services/ast_data/alarms.mli | 1 -
src/plugins/dive/build.ml | 2 +-
src/plugins/eva/alarmset.ml | 6 ---
6 files changed, 4 insertions(+), 52 deletions(-)
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index 39813c1b131..5034f8671cc 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -97,7 +97,6 @@ const DEFAULTS: { [key: string]: boolean } = {
'alarms.special_float': true,
'alarms.float_to_int': true,
'alarms.function_pointer': true,
- 'alarms.union_initialization': true,
'alarms.bool_value': true,
'eva.priority_only': false,
'eva.data_tainted_only': false,
@@ -192,8 +191,6 @@ function filterAlarm(alarm: string | undefined): boolean {
case 'is_nan': return filter('alarms.special_float');
case 'float_to_int': return filter('alarms.float_to_int');
case 'function_pointer': return filter('alarms.function_pointer');
- case 'initialization_of_union':
- return filter('alarms.union_initialization');
case 'bool_value': return filter('alarms.bool_value');
default: return false;
}
@@ -466,7 +463,6 @@ function PropertyFilter(): JSX.Element {
<CheckField label="Differing blocks" path="alarms.differing_blocks" />
<CheckField label="Separations" path="alarms.separation" />
<CheckField label="Overlaps" path="alarms.overlap" />
- <CheckField label="Initialization of unions" path="alarms.union_initialization" />
</Section>
<Section label="Eva">
<CheckField
diff --git a/ivette/src/frama-c/kernel/api/properties/index.ts b/ivette/src/frama-c/kernel/api/properties/index.ts
index 63c04bd149e..fbbd717805e 100644
--- a/ivette/src/frama-c/kernel/api/properties/index.ts
+++ b/ivette/src/frama-c/kernel/api/properties/index.ts
@@ -215,8 +215,6 @@ export enum alarms {
is_nan = 'is_nan',
/** Pointer to a function with non-compatible type */
function_pointer = 'function_pointer',
- /** Uninitialized memory read of union */
- initialization_of_union = 'initialization_of_union',
/** Trap representation of a _Bool lvalue */
bool_value = 'bool_value',
}
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 44937937603..99658f1077b 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -63,12 +63,11 @@ type alarm =
| Is_nan_or_infinite of exp * fkind
| Is_nan of exp * fkind
| Function_pointer of exp * exp list option
- | Uninitialized_union of lval list
| Invalid_bool of lval
(* If you add one constructor to this type, make sure to add a dummy value
in the 'reprs' value below, and increase 'nb_alarms' *)
-let nb_alarm_constructors = 18
+let nb_alarm_constructors = 17
module D =
Datatype.Make_with_collections
@@ -96,7 +95,6 @@ module D =
Is_nan_or_infinite (e, FFloat);
Is_nan (e, FFloat);
Function_pointer (e, None);
- Uninitialized_union [ lv ];
Invalid_bool lv;
]
@@ -117,8 +115,7 @@ module D =
| Differing_blocks _ -> 13
| Dangling _ -> 14
| Function_pointer _ -> 15
- | Uninitialized_union _ -> 16
- | Invalid_bool _ -> 17
+ | Invalid_bool _ -> 16
let () = (* Lightweight checks *)
for i = 0 to nb_alarm_constructors - 1 do
@@ -170,17 +167,6 @@ module D =
let n = Lval.compare lv11 lv21 in
if n = 0 then Lval.compare lv12 lv22 else n
| Uninitialized lv1, Uninitialized lv2 -> Lval.compare lv1 lv2
- | Uninitialized_union llv1, Uninitialized_union llv2 ->
- let len1 = List.length llv1 in
- let len2 = List.length llv2 in
- begin
- match compare len1 len2 with
- | 0 -> List.fold_left2 (fun acc lv1 lv2 ->
- if acc <> 0 then acc
- else Lval.compare lv1 lv2
- ) 0 llv1 llv2
- | _ -> assert false
- end
| Dangling lv1, Dangling lv2 -> Lval.compare lv1 lv2
| Differing_blocks (e11, e12), Differing_blocks (e21, e22) ->
let n = Exp.compare e11 e21 in
@@ -196,7 +182,7 @@ module D =
Overflow _ | Not_separated _ | Overlap _ | Uninitialized _ |
Dangling _ | Is_nan_or_infinite _ | Is_nan _ | Float_to_int _ |
Differing_blocks _ | Function_pointer _ |
- Uninitialized_union _ | Invalid_bool _)
+ Invalid_bool _)
->
let n = nb a1 - nb a2 in
assert (n <> 0);
@@ -234,8 +220,6 @@ module D =
| Uninitialized lv -> Hashtbl.hash (nb a, Lval.hash lv)
| Dangling lv -> Hashtbl.hash (nb a, Lval.hash lv)
| Function_pointer (e, _) -> Hashtbl.hash (nb a, Exp.hash e)
- | Uninitialized_union llv ->
- Hashtbl.hash (nb a, List.map Lval.hash llv)
| Invalid_bool lv -> Hashtbl.hash (nb a, Lval.hash lv)
let structural_descr = Structural_descr.t_abstract
@@ -300,10 +284,6 @@ module D =
Format.fprintf fmt "Unspecified(@[%a@])" Lval.pretty lv
| Function_pointer (e, _) ->
Format.fprintf fmt "Function_pointer(@[%a@])" Exp.pretty e
- | Uninitialized_union llv ->
- Format.fprintf fmt "Uninitialized_union(@[[%a]@])"
- (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "; ") Lval.pretty)
- llv
| Invalid_bool lv ->
Format.fprintf fmt "Invalid_bool(@[%a@])" Lval.pretty lv
@@ -412,7 +392,6 @@ let get_name = function
| Is_nan _ -> "is_nan"
| Float_to_int _ -> "float_to_int"
| Function_pointer _ -> "function_pointer"
- | Uninitialized_union _ -> "initialization_of_union"
| Invalid_bool _ -> "bool_value"
let get_short_name = function
@@ -436,7 +415,6 @@ let get_description = function
| Is_nan _ -> "NaN floating-point value"
| Float_to_int _ -> "Overflow in float to int conversion"
| Function_pointer _ -> "Pointer to a function with non-compatible type"
- | Uninitialized_union _ -> "Uninitialized memory read of union"
| Invalid_bool _ -> "Trap representation of a _Bool lvalue"
@@ -656,19 +634,6 @@ let create_predicate ?(loc=Location.unknown) alarm =
let t = Logic_utils.expr_to_term e in
Logic_const.(pvalid_function ~loc t)
- | Uninitialized_union llv ->
- (* \initialized(lv_1) || ... || \initialized(lv_n) *)
- let make_lval_predicate lv =
- let e = Cil.mkAddrOrStartOf ~loc lv in
- let t = Logic_utils.expr_to_term e in
- Logic_const.pinitialized ~loc (Logic_const.here_label, t)
- in
- List.fold_left (fun acc lv ->
- Logic_const.por ~loc (acc, make_lval_predicate lv)
- )
- (make_lval_predicate (List.hd llv))
- (List.tl llv)
-
| Invalid_bool lv ->
let e = Cil.new_exp ~loc (Lval lv) in
let t = Logic_utils.expr_to_term ~coerce:true e in
diff --git a/src/kernel_services/ast_data/alarms.mli b/src/kernel_services/ast_data/alarms.mli
index f897a2c70f2..fdb3b567ec9 100644
--- a/src/kernel_services/ast_data/alarms.mli
+++ b/src/kernel_services/ast_data/alarms.mli
@@ -63,7 +63,6 @@ type alarm =
(** the type of the pointer is compatible with the type of the pointed
function (first argument). The second argument is the list of the
arguments of the call. *)
- | Uninitialized_union of lval list
| Invalid_bool of lval (** Trap representation of a _Bool variable. *)
include Datatype.S_with_collections with type t = alarm
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index cfb1120e5c5..6116da7e18d 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -76,7 +76,7 @@ struct
in_exp e1 @ in_exp e2
| Memory_access (lval, _) -> in_lval lval
| Not_separated _ | Overlap _
- | Uninitialized _ | Dangling _ | Uninitialized_union _ -> []
+ | Uninitialized _ | Dangling _ -> []
| Invalid_bool lv -> [lv]
end
diff --git a/src/plugins/eva/alarmset.ml b/src/plugins/eva/alarmset.ml
index 121f914f554..d902c0d852f 100644
--- a/src/plugins/eva/alarmset.ml
+++ b/src/plugins/eva/alarmset.ml
@@ -366,9 +366,6 @@ let emit_alarm kinstr alarm (status:status) =
| Alarms.Function_pointer _ ->
register_alarm "pointer to function with incompatible type"
- | Alarms.Uninitialized_union _ ->
- register_alarm "accessing uninitialized union"
-
| Alarms.Invalid_bool _ ->
register_alarm "trap representation of a _Bool lvalue"
@@ -398,8 +395,6 @@ let height_alarm = let open Eva_utils in function
| _ -> false
in
if trivial then height_expr e else height_expr e + 1
- | Alarms.Uninitialized_union llv ->
- List.fold_left max 0 (List.map height_lval llv)
let cmp a1 a2 =
Datatype.Int.compare (height_alarm (fst a1)) (height_alarm (fst a2))
@@ -456,7 +451,6 @@ let warn_alarm warn_mode = function
| Alarms.Not_separated _
| Alarms.Overlap _
| Alarms.Function_pointer _
- | Alarms.Uninitialized_union _
| Alarms.Invalid_bool _
-> warn_mode.others ()
--
GitLab