[kernel] Fixes the Eva run of the test very_large_integers.c

d1de54b4 · David Bühler · 1f689741 · d1de54b4 · d1de54b4 · d1de54b4
Commit d1de54b4 authored 3 years ago by David Bühler
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/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:24: User Error: 
+[kernel] tests/syntax/very_large_integers.c:23: User Error: 
  integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
-[kernel] tests/syntax/very_large_integers.c:25: User Error: 
+[kernel] tests/syntax/very_large_integers.c:24: User Error: 
  bitfield width is not a valid integer constant
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                   (9223372036854775808) )
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add

--- a/tests/syntax/oracle/very_large_integers.1.res.oracle
+++ b/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:31: User Error: 
+[kernel] tests/syntax/very_large_integers.c:30: User Error: 
  Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:31: User Error: 
+[kernel] tests/syntax/very_large_integers.c:30: User Error: 
  Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                   (9223372036854775808) )
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add

--- a/tests/syntax/oracle/very_large_integers.10.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                   (9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:86: Failure: 
+[kernel] tests/syntax/very_large_integers.c:85: Failure: 
  Invalid digit 9 in integer literal '09876543210' in base 8.
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add
  '-kernel-msg-key pp' for preprocessing command.

--- a/tests/syntax/oracle/very_large_integers.11.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.11.res.oracle
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                   (9223372036854775808) )
+[kernel:annot-error] tests/syntax/very_large_integers.c:94: Warning: 
+  Invalid slevel directive. Ignoring code annotation
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
  nondet ∈ [--..--]
-[kernel:annot-error] tests/syntax/very_large_integers.c:92: Warning: 
+[kernel:annot-error] tests/syntax/very_large_integers.c:91: Warning: 
  invalid loop unrolling parameter; ignoring
-[kernel] User Error: warning annot-error treated as fatal error.
+[kernel:annot-error] tests/syntax/very_large_integers.c:93: Warning: 
+  invalid loop unrolling parameter; ignoring
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 14 statements reached (out of 14): 100% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    0 warnings
+    by the Frama-C kernel:    0 errors    5 warnings
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
+[kernel] Warning: warning annot-error treated as deferred error. See above messages for more information.
 [kernel] Frama-C aborted: invalid user input.
--- a/tests/syntax/oracle/very_large_integers.12.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.12.res.oracle
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                   (9223372036854775808) )
-[kernel:annot-error] tests/syntax/very_large_integers.c:97: Warning: 
-  Invalid slevel directive. Ignoring code annotation
-[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] tests/syntax/very_large_integers.c:98: User Error: 
+  Invalid digit 9 in integer literal '09' in base 8.
 [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.
--- a/tests/syntax/oracle/very_large_integers.13.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.13.res.oracle
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                   (9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:101: User Error: 
-  Invalid digit 9 in integer literal '09' in base 8.
-[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.
+[kernel] tests/syntax/very_large_integers.c:103: 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;
+}
+
+
--- a/tests/syntax/oracle/very_large_integers.14.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
-[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
-  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
-  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
-                                                   (9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:106: 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;
-}
-
-
--- a/tests/syntax/oracle/very_large_integers.2.res.oracle
+++ b/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:38: User Error: 
+[kernel] tests/syntax/very_large_integers.c:37: User Error: 
  integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:38: Failure: 
+[kernel] tests/syntax/very_large_integers.c:37: 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.

--- a/tests/syntax/oracle/very_large_integers.3.res.oracle
+++ b/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:46: Failure: Case range too large
+[kernel] tests/syntax/very_large_integers.c:45: Failure: Case range too large
 [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.
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/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:51: Failure: 
+[kernel] tests/syntax/very_large_integers.c:50: 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.

--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/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:55: User Error: 
+[kernel] tests/syntax/very_large_integers.c:54: User Error: 
  INDEX initialization designator overflows
-  53    
-  54    #ifdef INIT_DESIGNATOR2
-  55    int arr3[1] = { [9999999999999999999U] = 42 };
+  52    
+  53    #ifdef INIT_DESIGNATOR2
+  54    int arr3[1] = { [9999999999999999999U] = 42 };
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  56    #endif
-  57
+  55    #endif
+  56
 [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.
--- a/tests/syntax/oracle/very_large_integers.6.res.oracle
+++ b/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:59: User Error: 
+[kernel] tests/syntax/very_large_integers.c:58: User Error: 
  integer constant too large in expression -9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:59: User Error: 
+[kernel] tests/syntax/very_large_integers.c:58: User Error: 
  integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:59: Failure: 
+[kernel] tests/syntax/very_large_integers.c:58: 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.

--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/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:63: Failure: INDEX_RANGE too large
+[kernel] tests/syntax/very_large_integers.c:62: Failure: INDEX_RANGE too large
 [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.
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/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:68: User Error: 
+[kernel] tests/syntax/very_large_integers.c:67: User Error: 
  Invalid attribute constant: 0x80000000000000000
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                   (9223372036854775808) )
 [kernel] User Error: stopping on file "tests/syntax/very_large_integers.c" that has errors. Add

--- a/tests/syntax/oracle/very_large_integers.9.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
 [kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:73: Warning: 
+[kernel] tests/syntax/very_large_integers.c:72: Warning: 
  ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                   (9223372036854775808) )
 [kernel] Failure: Cannot represent logical integer in C: 9999999999999999999

--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -12,8 +12,7 @@
   STDOPT: #"-cpp-extra-args=-DATTRIBUTE_CONSTANT"
   STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT"
   STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT_OCTAL"
-   STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva"
-   STDOPT: #"-cpp-extra-args=-DEVA_UNROLL2 -eva"
+   STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva -kernel-warn-key annot-error=error"
   STDOPT: #"-cpp-extra-args=-DCABS_DOWHILE"
   EXIT: 0
   STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
@@ -90,8 +89,6 @@ int main() {
 #ifdef EVA_UNROLL
  //@ loop unroll (-9999999999999999999); // IntLimit
  while (nondet);
-#endif
-#ifdef EVA_UNROLL2
  //@ loop unroll too_large_integer; // ExpLimit
  while (nondet);
  //@ slevel 9999999999999999999;