[Eva] revert syntax from 'loop unroll full' to 'loop unroll'

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)
 

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;