From af67d277a87af781dfd76d524f18a8c001cecd5d Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 15 Sep 2020 15:57:29 +0200
Subject: [PATCH] [Eva] revert syntax from 'loop unroll full' to 'loop unroll'
---
src/plugins/value/utils/eva_annotations.ml | 8 ++++----
tests/value/partitioning-annots.c | 6 ++++--
2 files changed, 8 insertions(+), 6 deletions(-)
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index 7ba7cc2f97a..600a28b386b 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -178,7 +178,7 @@ module Unroll = Register (struct
let is_loop_annot = true
let parse ~typing_context = function
- | [{lexpr_node = PLvar "full"}] -> UnrollFull
+ | [] -> UnrollFull
| [t] ->
let open Logic_typing in
UnrollAmount
@@ -186,16 +186,16 @@ module Unroll = Register (struct
| _ -> raise Parse_error
let export = function
- | UnrollFull -> Ext_terms [Logic_const.tstring "full"]
+ | UnrollFull -> Ext_terms []
| UnrollAmount t -> Ext_terms [t]
let import = function
- | Ext_terms [{term_node=TConst (LStr "full")}] -> UnrollFull
+ | Ext_terms [] -> UnrollFull
| Ext_terms [t] -> UnrollAmount t
| _ -> assert false
let print fmt = function
- | UnrollFull -> Format.pp_print_string fmt "full"
+ | UnrollFull -> ()
| UnrollAmount t -> Printer.pp_term fmt t
end)
diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c
index 9bb04019ce3..45afe10c853 100644
--- a/tests/value/partitioning-annots.c
+++ b/tests/value/partitioning-annots.c
@@ -40,10 +40,12 @@ void test_unroll()
// At the end, we must have both arrays a and b to be fully initialized at 42
- // Small loops can be unrolled with the annotation "unroll full".
+ // Small loops can be unrolled without giving an unroll amount.
// The actual limit of the number of iterations can be overriden with
// the option -eva-default-loop-unroll
- //@ loop unroll full;
+ // Here -eva-default-loop-unroll is set to a value not high enough to
+ // completely unroll the loop thus a warning should be emitted.
+ //@ loop unroll;
for (int i = 0 ; i < 2*N ; i++)
c[i] = i % 2;
--
GitLab