[Kernel] Minor simplification in unroll_loops; replaces a fatal by a warning.

src/kernel_internals/typing/unroll_loops.ml

@@ -50,15 +50,8 @@ let update_info global_find_init emitter info spec =
               (new Logic_utils.simplify_const_lval global_find_init) spec
           in
           let i = Logic_utils.constFoldTermToInt t in
-          match i with
-          | Some i ->
-            begin
-              match Integer.to_int_opt i with
-              | Some _ as unroll_number -> { info with unroll_number }
-              | None -> Kernel.abort ~current:true
-                          "count too large in unrolling directive: %a"
-                          (Integer.pretty ~hexa:false) i
-            end
+          match Option.bind i Integer.to_int_opt with
+          | Some _ as unroll_number -> { info with unroll_number }
           | None ->
             Kernel.warning ~once:true ~current:true
               "ignoring unrolling directive (not an understood constant \

tests/syntax/oracle/very_large_integers.0.res.oracle

 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:16: User Error: 
+[kernel] tests/syntax/very_large_integers.c:18: User Error: 
   integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
-[kernel] tests/syntax/very_large_integers.c:17: User Error: 
+[kernel] tests/syntax/very_large_integers.c:19: User Error: 
   bitfield width is not a valid integer constant
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add

tests/syntax/oracle/very_large_integers.1.res.oracle

 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:23: User Error: 
+[kernel] tests/syntax/very_large_integers.c:25: User Error: 
   invalid integer constant: 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:23: User Error: 
+[kernel] tests/syntax/very_large_integers.c:25: User Error: 
   invalid integer constant: 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add

tests/syntax/oracle/very_large_integers.2.res.oracle

 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:29: User Error: 
+[kernel] tests/syntax/very_large_integers.c:31: User Error: 
   integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:29: Failure: 
+[kernel] tests/syntax/very_large_integers.c:31: Failure: 
   Cannot understand the constants in case range
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
   '-kernel-msg-key pp' for preprocessing command.

tests/syntax/oracle/very_large_integers.3.res.oracle

 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:34: Failure: 
+[kernel] tests/syntax/very_large_integers.c:36: Failure: 
   Array length 9999999999999999999U is not a compile-time constant: no explicit initializer allowed.
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
   '-kernel-msg-key pp' for preprocessing command.

tests/syntax/oracle/very_large_integers.4.res.oracle

 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:38: User Error: 
+[kernel] tests/syntax/very_large_integers.c:40: User Error: 
   INDEX initialization designator overflows
-  36    
-  37    #ifdef INIT_DESIGNATOR2
-  38    int arr3[1] = { [9999999999999999999U] = 42 };
+  38    
+  39    #ifdef INIT_DESIGNATOR2
+  40    int arr3[1] = { [9999999999999999999U] = 42 };
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  39    #endif
-  40
+  41    #endif
+  42
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
   '-kernel-msg-key pp' for preprocessing command.
 [kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/very_large_integers.5.res.oracle

 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:42: User Error: 
+[kernel] tests/syntax/very_large_integers.c:44: User Error: 
   integer constant too large in expression -9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:42: User Error: 
+[kernel] tests/syntax/very_large_integers.c:44: User Error: 
   integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:42: Failure: 
+[kernel] tests/syntax/very_large_integers.c:44: Failure: 
   INDEX_RANGE initialization designator is not a valid constant
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
   '-kernel-msg-key pp' for preprocessing command.

tests/syntax/oracle/very_large_integers.6.res.oracle

 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:46: User Error: 
+[kernel] tests/syntax/very_large_integers.c:48: User Error: 
   Invalid attribute constant: 0x80000000000000000
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add

tests/syntax/oracle/very_large_integers.7.res.oracle

 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
-[kernel:annot-error] tests/syntax/very_large_integers.c:65: Warning: 
+[kernel:annot-error] tests/syntax/very_large_integers.c:67: Warning: 
   Invalid slevel directive. Ignoring code annotation
 [kernel] User Error: warning annot-error treated as fatal error.
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add

tests/syntax/oracle/very_large_integers.8.res.oracle

 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:51: Warning: 
+[kernel] tests/syntax/very_large_integers.c:53: Warning: 
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:71: User Error: 
-  count too large in unrolling directive: 99999999999999999999
-[kernel] Frama-C aborted: invalid user input.
+[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+  ignoring unrolling directive (not an understood constant expression)
+/* Generated by Frama-C */
+int volatile nondet;
+/*@ logic ℤ too_large_integer= 9999999999999999999;
+ */
+int main(void)
+{
+  int __retres;
+  /*@ loop pragma UNROLL 99999999999999999999; */
+  while (nondet) ;
+  __retres = 0;
+  return __retres;
+}
+
+

tests/syntax/very_large_integers.c

 /* run.config
+   PLUGIN: @EVA_PLUGINS@
    EXIT: 1
    STDOPT: #"-cpp-extra-args=-DBITFIELD"
    STDOPT: #"-cpp-extra-args=-DARRAY_DECL"
@@ -8,6 +9,7 @@
    STDOPT: #"-cpp-extra-args=-DRANGE_DESIGNATOR"
    STDOPT: #"-cpp-extra-args=-DATTRIBUTE_CONSTANT"
    STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva"
+   EXIT: 0
    STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
 */
 volatile int nondet;