From dba36ec4c468686df48d59f475e60f491a62d25d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 18 Oct 2019 12:05:58 +0200
Subject: [PATCH] [Builtin] Deals with memset 0
---
src/plugins/builtin/basic_blocks.ml | 15 +++++++++++++--
src/plugins/builtin/memset.ml | 9 ++++++++-
2 files changed, 21 insertions(+), 3 deletions(-)
diff --git a/src/plugins/builtin/basic_blocks.ml b/src/plugins/builtin/basic_blocks.ml
index 7fcab6a2b79..1e2b50afa42 100644
--- a/src/plugins/builtin/basic_blocks.ml
+++ b/src/plugins/builtin/basic_blocks.ml
@@ -210,13 +210,24 @@ and pall_elems_eq ?loc depth t1 value len =
let tind = tvar ind in
let bounds = pbounds_incl_excl ?loc (tinteger 0) tind len in
let t1_acc = taccess ?loc t1 tind in
- let eq = peq_unfold ?loc (depth+1) t1_acc value in
+ let eq = peq_unfold ?loc depth t1_acc value in
pforall ?loc ([ind], (pimplies ?loc (bounds, eq)))
+and pall_fields_eq ?loc depth t1 ci value =
+ let eq fi =
+ let lval = match t1.term_node with TLval(lv) -> lv | _ -> assert false in
+ let nlval = addTermOffsetLval (TField(fi, TNoOffset)) lval in
+ let term = term ?loc (TLval nlval) (Ctype fi.ftype) in
+ peq_unfold ?loc depth term value
+ in
+ let eqs = List.map eq ci.cfields in
+ pands eqs
and peq_unfold ?loc depth t1 value =
match t1.term_type with
| Ctype(TArray(_, Some len, _, _)) ->
let len = Logic_utils.expr_to_term ~cast:false len in
- pall_elems_eq ?loc depth t1 value len
+ pall_elems_eq ?loc (depth+1) t1 value len
+ | Ctype(TComp(ci, _, _)) ->
+ pall_fields_eq ?loc depth t1 ci value
| _ -> prel ?loc (Req, t1, value)
let pseparated_memories ?loc p1 len1 p2 len2 =
diff --git a/src/plugins/builtin/memset.ml b/src/plugins/builtin/memset.ml
index 1bd6ba655f7..631a66bd4f3 100644
--- a/src/plugins/builtin/memset.ml
+++ b/src/plugins/builtin/memset.ml
@@ -92,7 +92,9 @@ let generate_ensures e loc t ptr value len =
let content = match e, value with
| None, Some value ->
[ { (pset_len_bytes ~loc ptr value len) with pred_name } ]
- | Some 0, None -> []
+ | Some 0, None ->
+ let value = tinteger ~loc 0 in
+ [ { (pset_len_bytes ~loc ptr value len) with pred_name } ]
| Some 255, None -> []
| _ -> assert false
in
@@ -128,8 +130,13 @@ let memset_value e =
| Const(CInt64(ni, _, _)) when Integer.equal ni ff -> Some 255
| _ -> None
+let is_union_type = function
+ | TComp({ cstruct = false }, _, _) -> true
+ | _ -> false
+
let well_typed_call = function
| [ ptr ; _ ; _ ] when any_char_composed_type (type_from_arg ptr) -> true
+ | [ ptr ; _ ; _ ] when is_union_type (type_from_arg ptr) -> false
| [ _ ; value ; _ ] ->
begin match memset_value value with
| None -> false
--
GitLab