diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 24cb1bec294007d4810c5d91f7379608dcbc9168..4317af5b04cbe11e8f1e95f0b8557a28c842efb5 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5310,7 +5310,7 @@ and doType (ghost:bool) isFuncArg
Attr("arraylen", [ la ]) :: static
with NotAnAttrParam _ -> begin
Kernel.warning ~once:true ~current:true
- "Cannot represent the length '%a'of array as an attribute"
+ "Cannot represent the length '%a' of array as an attribute"
Cil_printer.pp_exp l
;
static (* Leave unchanged *)
@@ -5999,7 +5999,14 @@ and doExp local_env
| Cabs.CONSTANT ct -> begin
match ct with
| Cabs.CONST_INT str -> begin
- let res = parseIntExp ~loc str in
+ let res =
+ try parseIntExp ~loc str
+ with Cil.ParseIntError msg ->
+ Kernel.error ~current:true "%s" msg;
+ (* assign an arbitrary expression,
+ since we must return something *)
+ Cil.one ~loc
+ in
finishExp [] (unspecified_chunk empty) res (typeOf res)
end
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 406439f82cb2ba342c29dd9988a3e9b299f976b7..67bec896462c4c54511b01ac9f65398fb0ece194 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3240,11 +3240,12 @@ let parseIntAux (str:string) =
let doAcc what =
if Integer.ge what base
then
- Kernel.fatal ~current:true
- "Invalid digit %a in integer constant '%s' in base %a."
- (Integer.pretty ~hexa:false) what
- str
- (Integer.pretty ~hexa:false) base;
+ raise (ParseIntError
+ (Format.asprintf
+ "Invalid digit %a in integer literal '%s' in base %a."
+ (Integer.pretty ~hexa:false) what
+ str
+ (Integer.pretty ~hexa:false) base));
let acc' =
Integer.add what (Integer.mul base acc) in
toInt base acc' (idx + 1)
@@ -3261,7 +3262,8 @@ let parseIntAux (str:string) =
doAcc (Integer.of_int (10 + Char.code ch - Char.code 'A'))
else
raise (ParseIntError
- (Format.asprintf "Invalid integer constant: %s" str))
+ (Format.asprintf
+ "Invalid character %c in integer literal: %s" ch str))
in
let i =
if octalhexbin && l >= 2 then
@@ -3278,45 +3280,37 @@ let parseIntAux (str:string) =
i,kinds
let parseInt s =
- try
- fst (parseIntAux s)
- with ParseIntError msg ->
- Kernel.fatal ~current:true "%s" msg
+ fst (parseIntAux s)
+
+let parseInt_opt str =
+ try Some (parseInt str)
+ with ParseIntError _ -> None
let parseIntLogic ~loc str =
- try
- let i,_= parseIntAux str in
- { term_node = TConst (Integer (i,Some str)) ; term_loc = loc;
- term_name = []; term_type = Linteger;}
- with ParseIntError msg ->
- Kernel.fatal ~current:true "%s" msg
+ let i,_= parseIntAux str in
+ { term_node = TConst (Integer (i,Some str)) ; term_loc = loc;
+ term_name = []; term_type = Linteger;}
+
+let parseIntLogic_opt ~loc str =
+ try Some (parseIntLogic ~loc str)
+ with ParseIntError _ -> None
let parseIntExp ~loc repr =
- try
- let i,kinds = parseIntAux repr in
- let rec loop = function
- | k::rest ->
- if fitsInInt k i then (* i fits in the current type. *)
- kinteger64 ~loc ~repr ~kind:k i
- else loop rest
- | [] ->
- Kernel.fatal ~source:(fst loc) "Cannot represent the integer %s" repr
- in
- loop kinds
- with ParseIntError msg ->
- Kernel.fatal ~current:true "%s" msg
+ let i,kinds = parseIntAux repr in
+ let rec loop = function
+ | k::rest ->
+ if fitsInInt k i then (* i fits in the current type. *)
+ kinteger64 ~loc ~repr ~kind:k i
+ else loop rest
+ | [] ->
+ raise (ParseIntError
+ (Format.asprintf "Cannot represent the integer %s" repr))
+ in
+ loop kinds
let parseIntExp_opt ~loc repr =
try
- let i,kinds = parseIntAux repr in
- let rec loop = function
- | k::rest ->
- if fitsInInt k i then (* i fits in the current type. *)
- Some (kinteger64 ~loc ~repr ~kind:k i)
- else loop rest
- | [] -> None
- in
- loop kinds
+ Some (parseIntExp loc repr)
with ParseIntError _ -> None
let mkStmtCfg ~before ~(new_stmtkind:stmtkind) ~(ref_stmt:stmt) : stmt =
@@ -4129,13 +4123,9 @@ and alignOfField (fi: fieldinfo) =
and intOfAttrparam (a:attrparam) : int option =
let rec doit a : int =
match a with
- | AInt(n) ->
- begin
- match Integer.to_int_opt n with
- | Some n' -> n'
- | None ->
- raise (SizeOfError ("Overflow in integer attribute.", voidType))
- end
+ | AInt(n) ->
+ Extlib.the ~exn:(SizeOfError ("Overflow in integer attribute.", voidType))
+ (Integer.to_int_opt n)
| ABinOp(PlusA, a1, a2) -> doit a1 + doit a2
| ABinOp(MinusA, a1, a2) -> doit a1 - doit a2
| ABinOp(Mult, a1, a2) -> doit a1 * doit a2
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 62c5bfbf255c7c1b72b5a52c5dba5b6cdc3695e9..82868ebd4ca11c52eb4be00611ab286c99e2b446 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1036,20 +1036,47 @@ val typeOf_array_elem : typ -> typ
val is_fully_arithmetic: typ -> bool
(** Returns [true] whenever the type contains only arithmetic types *)
-(** Convert a string representing a C integer literal to an expression.
+(** Exception raised by several parseInt* functions.
+ @since Frama-C+dev
+*)
+exception ParseIntError of string
+
+(** Convert a string representing a C integer literal to an Integer.
Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL.
+ @raise ParseIntError if there is an error parsing the string
+ (e.g. invalid characters).
+ @modify Frama-C+dev now raises ParseIntError.
*)
val parseInt: string -> Integer.t
+
+(** Like [parseInt], but returns [None] in case of failure.
+ @since Frama-C+dev
+*)
+val parseInt_opt: string -> Integer.t option
+
+(** Like [parseInt], but converts to an expression.
+ @raise ParseIntError if the string cannot be converted
+ (e.g., too large, or contains invalid characters).
+ @modify Frama-C+dev now raises ParseIntError.
+*)
val parseIntExp: loc:location -> string -> exp
-val parseIntLogic: loc:location -> string -> term
(** Like [parseIntExp], but returns [None] in case of failure.
@since Frama-C+dev
*)
val parseIntExp_opt: loc:location -> string -> exp option
-(** Convert a string representing a C integer literal to an expression.
- Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL *)
+(** Like [parseInt], but converts to a logic term.
+ @raise ParseIntError if there is an error parsing the string
+ (e.g. invalid characters).
+ @modify Frama-C+dev now raises ParseIntError.
+*)
+val parseIntLogic: loc:location -> string -> term
+
+(** Like [parseIntLogic], but returns [None] in case of failure.
+ @since Frama-C+dev
+*)
+val parseIntLogic_opt: loc:location -> string -> term option
val appears_in_expr: varinfo -> exp -> bool
(** @return true if the given variable appears in the expression. *)
diff --git a/tests/syntax/oracle/invalid_constant.res.oracle b/tests/syntax/oracle/invalid_constant.res.oracle
index b4b0da647d4313161e9561d38aa1b02bb4c8dfff..cfd2c2ad290eea43ed3087eb2ca5e4f59de38ac2 100644
--- a/tests/syntax/oracle/invalid_constant.res.oracle
+++ b/tests/syntax/oracle/invalid_constant.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/invalid_constant.i (no preprocessing)
-[kernel] tests/syntax/invalid_constant.i:6: Failure:
- Invalid digit 8 in integer constant '0123456789' in base 8.
+[kernel] tests/syntax/invalid_constant.i:6: User Error:
+ Invalid digit 8 in integer literal '0123456789' in base 8.
[kernel] User Error: stopping on file "tests/syntax/invalid_constant.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.1.res.oracle b/tests/syntax/oracle/very_large_integers.1.res.oracle
index 53fe76c37f3be3de790eaf9a496c2a1896db9416..43f59ecb36a0bf51cd45b43e9d3ca7cae94cd35a 100644
--- a/tests/syntax/oracle/very_large_integers.1.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.1.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
[kernel] tests/syntax/very_large_integers.c:25: User Error:
- invalid integer constant: 99999999999999999999U
+ Cannot represent the integer 99999999999999999999U
[kernel] tests/syntax/very_large_integers.c:25: User Error:
- invalid integer constant: 99999999999999999999U
+ Cannot represent the integer 99999999999999999999U
[kernel] tests/syntax/very_large_integers.c:53: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
[kernel] tests/syntax/very_large_integers.c:53: Warning: