From 4df1b92ccdd2fe8e7219cc91d259d3021f8a5cf1 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 19 Jun 2020 09:22:02 +0200
Subject: [PATCH] [tests] refine test case for insertion of loop assigns
---
tests/spec/loop_assigns_generated.ml | 26 ++++++++++++++++++++++++++
1 file changed, 26 insertions(+)
diff --git a/tests/spec/loop_assigns_generated.ml b/tests/spec/loop_assigns_generated.ml
index 30d64b3ffeb..7ac50e360b1 100644
--- a/tests/spec/loop_assigns_generated.ml
+++ b/tests/spec/loop_assigns_generated.ml
@@ -29,6 +29,16 @@ let add_allocates e kf stmt v =
(AAllocation([],FreeAlloc ([],[id_v]))));
Filecheck.check_ast ("after insertion of loop allocates " ^ v.vname )
+let check_only_one f =
+ let seen = ref false in
+ fun _ a ->
+ if f a then begin
+ assert (not !seen);
+ seen := true
+ end
+
+let filter_category f _ a acc = if f a then a :: acc else acc
+
let main () =
Ast.compute();
let kf = Globals.Functions.find_by_name "f" in
@@ -45,6 +55,22 @@ let main () =
add_assigns e2 kf s k;
add_allocates e1 kf s p;
add_allocates e2 kf s q;
+ Annotations.iter_code_annot (check_only_one Logic_utils.is_assigns) s;
+ Annotations.iter_code_annot (check_only_one Logic_utils.is_allocation) s;
+ let lassigns =
+ Annotations.fold_code_annot (filter_category Logic_utils.is_assigns) s []
+ in
+ assert (List.length lassigns = 1);
+ let lalloc =
+ Annotations.fold_code_annot (filter_category Logic_utils.is_allocation) s []
+ in
+ assert (List.length lalloc = 1);
+ ignore
+ (Property_status.get
+ (Property.ip_of_code_annot_single kf s (List.hd lassigns)));
+ ignore
+ (Property_status.get
+ (Property.ip_of_code_annot_single kf s (List.hd lalloc)));
File.pretty_ast ()
let () = Db.Main.extend main
--
GitLab