From 061b5aa8f62e66dbc5d953fb4e7eca10dcfb865e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 15 Jan 2021 14:03:47 +0100
Subject: [PATCH] [rte] fatal error if accessing an object whose type is an
undefined union
---
src/plugins/rte/rte.ml | 15 +++++++++------
1 file changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index 94464139655..e2ff580f144 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -111,15 +111,18 @@ let lval_initialized_assertion ~remove_trivial:_ ~on_alarm lv =
| NoOffset ->
begin
match typ with
- | TComp({cstruct = false; cfields} ,_,_) ->
+ | TComp({cstruct = false; cfields; cname} ,_,_) ->
(match cfields with
- | Some [] | None -> () (* empty union, supported by gcc with size 0.
- Trivially initialized. *)
- | _ ->
+ | None ->
+ Options.fatal
+ "Access to an object of undefined union %a"
+ Printer.pp_varname cname
+ | Some [] -> () (* empty union, supported by gcc with size 0.
+ Trivially initialized. *)
+ | Some l ->
let llv =
List.map
- (fun fi -> Cil.addOffsetLval (Field (fi, NoOffset)) lv)
- (Option.get cfields)
+ (fun fi -> Cil.addOffsetLval (Field (fi, NoOffset)) lv) l
in
if default then
on_alarm ~invalid:false (Alarms.Uninitialized_union llv))
--
GitLab