From 792aeaac76c6e822df64c0428d6c7b887e6f14f1 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 23 Jun 2020 19:44:18 +0200
Subject: [PATCH] [logic] fix some missing ~keep_empty:false
---
src/kernel_internals/typing/allocates.ml | 2 +-
src/plugins/aorai/aorai_visitors.ml | 5 ++++-
2 files changed, 5 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/allocates.ml b/src/kernel_internals/typing/allocates.ml
index 7b732f4edf8..21d04239663 100644
--- a/src/kernel_internals/typing/allocates.ml
+++ b/src/kernel_internals/typing/allocates.ml
@@ -35,7 +35,7 @@ let add_allocates_loop stmt =
let all_default = Annotations.fold_code_annot all_default stmt true in
if all_default then
let ca = AAllocation ([], FreeAlloc ([], [])) in
- Annotations.add_code_annot Emitter.kernel stmt
+ Annotations.add_code_annot ~keep_empty:false Emitter.kernel stmt
(Logic_const.new_code_annotation ca)
let add_allocates_nothing_funspec kf =
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 004941db674..7ce63778b53 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -272,7 +272,10 @@ let update_loop_assigns kf stmt state vi code_annot =
(AAssigns (bhvs, Logic_utils.concat_assigns old_assigns assigns))
| _ -> Aorai_option.fatal "Expecting an assigns clause here"
in
- Annotations.add_code_annot Aorai_option.emitter ~kf stmt new_assigns
+ (* we're putting the annotation on a new statement, with an empty
+ loop assigns by construction. Don't keep_empty *)
+ Annotations.add_code_annot
+ ~keep_empty:false Aorai_option.emitter ~kf stmt new_assigns
let get_action_post_cond kf ?init_trans return_states =
let to_consider pre_state int_states =
--
GitLab