From e42c989b5dd7885505162b882059f221b51e2653 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 16 Jun 2021 10:15:05 +0200
Subject: [PATCH] [Kernel] avoid another issue when parsing integers in
Cabs2cil
---
src/kernel_internals/typing/cabs2cil.ml | 2 +-
.../oracle/very_large_integers.0.res.oracle | 8 +++---
.../oracle/very_large_integers.1.res.oracle | 8 +++---
.../oracle/very_large_integers.10.res.oracle | 25 ++++++-------------
.../oracle/very_large_integers.11.res.oracle | 22 ++++++++++++++++
.../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 | 4 +--
.../oracle/very_large_integers.8.res.oracle | 6 ++---
.../oracle/very_large_integers.9.res.oracle | 6 ++---
tests/syntax/very_large_integers.c | 4 +++
14 files changed, 65 insertions(+), 50 deletions(-)
create mode 100644 tests/syntax/oracle/very_large_integers.11.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4317af5b04c..e0712af22e9 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1443,7 +1443,7 @@ let rec isCabsZeroExp e = match e.expr_node with
| SINGLE_INIT e -> isCabsZeroExp e
| NO_INIT | COMPOUND_INIT _ -> false)
| CONSTANT (CONST_INT i) ->
- Integer.is_zero (Cil.parseInt i)
+ Option.fold ~none:false ~some:Integer.is_zero (Cil.parseInt_opt i)
| _ -> false
module BlockChunk =
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index 64ae83250fe..db573af932d 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:21: User Error:
- integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
[kernel] tests/syntax/very_large_integers.c:22: User Error:
+ integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999
+[kernel] tests/syntax/very_large_integers.c:23: User Error:
bitfield width is not a valid integer constant
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: 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 4c65204b2fa..23cfa866c0b 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:28: User Error:
+[kernel] tests/syntax/very_large_integers.c:29: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:28: User Error:
+[kernel] tests/syntax/very_large_integers.c:29: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: 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.10.res.oracle b/tests/syntax/oracle/very_large_integers.10.res.oracle
index a1176c2d521..4f848474e09 100644
--- a/tests/syntax/oracle/very_large_integers.10.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
@@ -1,22 +1,11 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:85: 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;
-}
-
-
+[kernel] tests/syntax/very_large_integers.c:84: 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.
diff --git a/tests/syntax/oracle/very_large_integers.11.res.oracle b/tests/syntax/oracle/very_large_integers.11.res.oracle
new file mode 100644
index 00000000000..c352a476c8d
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.11.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
+ ignoring invalid aligned attribute: __aligned__(9223372036854775808)
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
+ ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
+ (9223372036854775808) )
+[kernel] tests/syntax/very_large_integers.c:89: 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/oracle/very_large_integers.2.res.oracle b/tests/syntax/oracle/very_large_integers.2.res.oracle
index 2c763bf0674..bb5f47fe756 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:35: User Error:
+[kernel] tests/syntax/very_large_integers.c:36: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:35: Failure:
+[kernel] tests/syntax/very_large_integers.c:36: 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 ac927237baf..ad9de534b05 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:40: Failure:
+[kernel] tests/syntax/very_large_integers.c:41: 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 403d2a65c2f..0d8599e3295 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:44: User Error:
+[kernel] tests/syntax/very_large_integers.c:45: User Error:
INDEX initialization designator overflows
- 42
- 43 #ifdef INIT_DESIGNATOR2
- 44 int arr3[1] = { [9999999999999999999U] = 42 };
+ 43
+ 44 #ifdef INIT_DESIGNATOR2
+ 45 int arr3[1] = { [9999999999999999999U] = 42 };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 45 #endif
- 46
+ 46 #endif
+ 47
[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 46e43a1bedb..1798bfe46e3 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:48: User Error:
+[kernel] tests/syntax/very_large_integers.c:49: User Error:
integer constant too large in expression -9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:48: User Error:
+[kernel] tests/syntax/very_large_integers.c:49: User Error:
integer constant too large in expression 9999999999999999999U
-[kernel] tests/syntax/very_large_integers.c:48: Failure:
+[kernel] tests/syntax/very_large_integers.c:49: 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 45af4ca2032..c531dfb15a1 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:52: User Error:
+[kernel] tests/syntax/very_large_integers.c:53: User Error:
Invalid attribute constant: 0x80000000000000000
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: 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 e34bb47c39d..75dbebc66e6 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] Failure: Cannot represent logical integer in C: 9999999999999999999
diff --git a/tests/syntax/oracle/very_large_integers.8.res.oracle b/tests/syntax/oracle/very_large_integers.8.res.oracle
index 0f63c2ee5d2..a0898661e14 100644
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] tests/syntax/very_large_integers.c:70: Failure:
+[kernel] tests/syntax/very_large_integers.c:71: 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.
diff --git a/tests/syntax/oracle/very_large_integers.9.res.oracle b/tests/syntax/oracle/very_large_integers.9.res.oracle
index 95d122b7737..9ed0fe33d85 100644
--- a/tests/syntax/oracle/very_large_integers.9.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] tests/syntax/very_large_integers.c:57: Warning:
+[kernel] tests/syntax/very_large_integers.c:58: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel:annot-error] tests/syntax/very_large_integers.c:79: Warning:
+[kernel:annot-error] tests/syntax/very_large_integers.c:80: 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/very_large_integers.c b/tests/syntax/very_large_integers.c
index 48dff8b8376..80e80299c6d 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -11,6 +11,7 @@
STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT"
STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT_OCTAL"
STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva"
+ STDOPT: #"-cpp-extra-args=-DCABS_DOWHILE"
EXIT: 0
STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
*/
@@ -79,6 +80,9 @@ int main() {
//@ slevel 9999999999999999999;
while (nondet);
#endif
+#ifdef CABS_DOWHILE
+ do { } while (09);
+#endif
#ifdef UNROLL_PRAGMA
//@ loop pragma UNROLL 99999999999999999999;
#endif
--
GitLab