From e3f264a2ab1bc1167770b9ec39bd08d48f6be518 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 8 Jun 2021 12:52:15 +0200
Subject: [PATCH] [Kernel] Minor simplification in unroll_loops; replaces a
fatal by a warning.
---
src/kernel_internals/typing/unroll_loops.ml | 11 ++-------
.../oracle/very_large_integers.0.res.oracle | 8 +++----
.../oracle/very_large_integers.1.res.oracle | 8 +++----
.../oracle/very_large_integers.2.res.oracle | 4 ++--
.../oracle/very_large_integers.3.res.oracle | 2 +-
.../oracle/very_large_integers.4.res.oracle | 12 +++++-----
.../oracle/very_large_integers.5.res.oracle | 6 ++---
.../oracle/very_large_integers.6.res.oracle | 6 ++---
.../oracle/very_large_integers.7.res.oracle | 6 ++---
.../oracle/very_large_integers.8.res.oracle | 23 +++++++++++++++----
tests/syntax/very_large_integers.c | 2 ++
11 files changed, 48 insertions(+), 40 deletions(-)
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index e09cbae6a55..89c96fbb3a5 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/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 \
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index a13d814a1d9..d7175f1e68f 100644
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -1,11 +1,11 @@
[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
diff --git a/tests/syntax/oracle/very_large_integers.1.res.oracle b/tests/syntax/oracle/very_large_integers.1.res.oracle
index 63275ad53b5..53fe76c37f3 100644
--- a/tests/syntax/oracle/very_large_integers.1.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.1.res.oracle
@@ -1,11 +1,11 @@
[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
diff --git a/tests/syntax/oracle/very_large_integers.2.res.oracle b/tests/syntax/oracle/very_large_integers.2.res.oracle
index 9a759fcdc0c..c21f3361baa 100644
--- a/tests/syntax/oracle/very_large_integers.2.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.2.res.oracle
@@ -1,7 +1,7 @@
[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.
diff --git a/tests/syntax/oracle/very_large_integers.3.res.oracle b/tests/syntax/oracle/very_large_integers.3.res.oracle
index 0888626b749..39820b9d4cd 100644
--- a/tests/syntax/oracle/very_large_integers.3.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.3.res.oracle
@@ -1,5 +1,5 @@
[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.
diff --git a/tests/syntax/oracle/very_large_integers.4.res.oracle b/tests/syntax/oracle/very_large_integers.4.res.oracle
index cb0367c4b37..d93cd65fdee 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -1,12 +1,12 @@
[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.
diff --git a/tests/syntax/oracle/very_large_integers.5.res.oracle b/tests/syntax/oracle/very_large_integers.5.res.oracle
index bf735cd8f5c..1de406bf2a6 100644
--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -1,9 +1,9 @@
[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.
diff --git a/tests/syntax/oracle/very_large_integers.6.res.oracle b/tests/syntax/oracle/very_large_integers.6.res.oracle
index fee0f227bcf..2518a170b6f 100644
--- a/tests/syntax/oracle/very_large_integers.6.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.6.res.oracle
@@ -1,9 +1,9 @@
[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
diff --git a/tests/syntax/oracle/very_large_integers.7.res.oracle b/tests/syntax/oracle/very_large_integers.7.res.oracle
index 77ad998c981..18a61c34997 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -1,10 +1,10 @@
[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
diff --git a/tests/syntax/oracle/very_large_integers.8.res.oracle b/tests/syntax/oracle/very_large_integers.8.res.oracle
index fe4bc11e18b..9d4810ae444 100644
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -1,9 +1,22 @@
[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;
+}
+
+
diff --git a/tests/syntax/very_large_integers.c b/tests/syntax/very_large_integers.c
index 8c6bac17a68..4831ada7bc1 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -1,4 +1,5 @@
/* 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;
--
GitLab