diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml index 7ba7cc2f97a77ed84d2c7cf939bcfe41e7ed3bc7..600a28b386b1a43bc6db77eda4d9c015471fa0bd 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 9bb04019ce3f87a6493d2887ae17b9c281c0735d..45afe10c853eafb7a0ed3895537aa6f8612572b7 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;