diff --git a/bin/migration_scripts/vanadium2chromium.sh b/bin/migration_scripts/vanadium2chromium.sh
new file mode 100755
index 0000000000000000000000000000000000000000..0e9694a828a3e09844ebd1460b75d9e342d6a532
--- /dev/null
+++ b/bin/migration_scripts/vanadium2chromium.sh
@@ -0,0 +1,166 @@
+#!/bin/bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2021 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+#
+# Converts a Frama-C plugin from Frama-C 23 Vanadium to Frama-C 24 Chromium,
+# on a best-efforts basis (no guarantee that the result is fully compatible).
+#
+# known missing features:
+# - doesn't follow symbolic links to directories
+
+DIR=
+
+# verbose on by default
+VERBOSE="v"
+
+# test once if sed supports -i (BSD/macOS does not)
+SED_HAS_I=$(sed --help 2>/dev/null | grep '\-i' 2>/dev/null)
+
+# [sedi file expressions] runs 'sed -i expressions' on the specified file;
+# if '-i' is not supported, creates a temporary file and overwrites the
+# original, like '-i' does.
+sedi ()
+{
+ file="$1"
+ shift
+ if [ -n "$SED_HAS_I" ]; then
+ sed -i "$@" "$file"
+ else
+ # option '-i' is not recognized by sed: use a tmp file
+ new_temp=`mktemp /tmp/frama-c.XXXXXXX` || exit 1
+ sed "$@" "$file" > "$new_temp"
+ mv -f "$new_temp" "$file"
+ fi
+}
+
+dirs ()
+{
+ if [ -z "$DIR" ]; then
+ DIR=.
+ fi
+}
+
+# [safe_goto d1 d2 cmd] goes to d1, runs cmd, and returns to d2
+safe_goto ()
+{
+ dir="$1"
+ cd "$dir"
+ $3
+ cd "$2"
+}
+
+goto ()
+{
+ if [ -d "$1" ]; then
+ safe_goto "$1" "$2" "$3"
+ else
+ echo "Directory '$1' does not exist. Omitted."
+ fi
+}
+
+process_file ()
+{
+ file="$1"
+ if [ "$VERBOSE" ]; then
+ echo "Processing file $file"
+ fi
+ sedi "$file" \
+ -e 's/Integer\.to_int\b/Integer.to_int_exn/g' \
+ -e 's/Integer\.to_int32/Integer.to_int32_exn/g' \
+ -e 's/Integer\.to_int64/Integer.to_int64_exn/g' \
+ # this line left empty on purpose
+}
+
+apply_one_dir ()
+{
+ if [ "$VERBOSE" ]; then
+ echo "Processing directory `pwd`"
+ fi
+ for f in $(find . -maxdepth 1 -type f -name "*.ml*" 2> /dev/null); do
+ process_file "$f"
+ done
+}
+
+apply_recursively ()
+{
+ apply_one_dir
+ while IFS= read -r -d $'\0' d; do
+ if [ "$d" = "." ]; then
+ continue
+ fi
+ safe_goto "$d" .. apply_recursively
+ done < <(find . -maxdepth 1 -type d -print0)
+}
+
+applying_to_list ()
+{
+ dirs
+ tmpdir=`pwd`
+ for d in $DIR; do
+ goto "$d" "$tmpdir" "$1"
+ done
+}
+
+help ()
+{
+ echo "Usage: $0 [options | directories]
+
+Options are:
+ -r | --recursive Check subdirectories recursively
+ -h | --help Display help message
+ -q | --quiet Quiet mode (i.e. non-verbose mode)
+ -v | --verbose Verbose mode (default)"
+ exit 0
+}
+
+error ()
+{
+ echo "$1.
+Do \"$0 -h\" for help."
+ exit 1
+}
+
+FN="apply_one_dir"
+
+parse_arg ()
+{
+ case $1 in
+ -r | --recursive) FN="apply_recursively";;
+ -h | -help ) help; exit 0;;
+ -q | --quiet ) VERBOSE=;;
+ -v | --verbose ) VERBOSE="v";;
+ -* ) error "Invalid option $1";;
+ * ) DIR="$DIR $1";;
+ esac
+}
+
+cmd_line ()
+{
+ for s in "$@"; do
+ parse_arg "$s"
+ done
+ applying_to_list $FN
+}
+
+cmd_line "$@"
+exit 0
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 7a47b2372ac463babda41ffa1acc5d37227c1bca..81ea66623889de33690c7d2cfd92aa261053deb6 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -42,6 +42,7 @@ bin/migration_scripts/sulfur2chlorine.sh: CEA_LGPL
bin/migration_scripts/chlorine2argon.sh: CEA_LGPL
bin/migration_scripts/potassium2calcium.sh: CEA_LGPL
bin/migration_scripts/titanium2vanadium.sh: CEA_LGPL
+bin/migration_scripts/vanadium2chromium.sh: CEA_LGPL
bin/sed_get_binutils_version: .ignore
bin/sed_get_make_major: .ignore
bin/sed_get_make_minor: .ignore
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 0b61835de9da9df88b181312f3c676ef0c4018af..000480d8dc808bd8737ae15fd25cd11940d13827 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1191,6 +1191,22 @@ end
let constFoldType (t:typ) : typ =
visitCilType constFoldTypeVisitor t
+let to_integer i =
+ match Integer.to_int_opt i with
+ | Some i -> i
+ | None ->
+ Kernel.error ~current:true "integer too large: %a"
+ (Integer.pretty ~hexa:true) i;
+ -1
+
+let constFoldToInteger e =
+ try Option.map Integer.to_int (Cil.constFoldToInt e)
+ with Z.Overflow ->
+ Kernel.error ~current:true
+ "integer constant too large in expression %a"
+ Cil_printer.pp_exp e;
+ None
+
let get_temp_name ghost () =
let undolist = ref [] in
let data = CurrentLoc.get() in
@@ -1427,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)
+ Result.fold ~error:(fun _ -> false) ~ok:Integer.is_zero (Cil.parseIntRes i)
| _ -> false
module BlockChunk =
@@ -3348,7 +3364,7 @@ let rec setOneInit this o preinit =
let idx, (* Index in the current comp *)
restoff (* Rest offset *) =
match o with
- | Index({enode = Const(CInt64(i,_,_))}, off) -> Integer.to_int i, off
+ | Index({enode = Const(CInt64(i,_,_))}, off) -> to_integer i, off
| Field (f, off) ->
(* Find the index of the field *)
let rec loop (idx: int) = function
@@ -3427,8 +3443,7 @@ let rec collectInitializer
match leno with
| Some len -> begin
match constFoldToInt len with
- | Some ni when Integer.ge ni Integer.zero ->
- (Integer.to_int ni), false
+ | Some ni when Integer.ge ni Integer.zero -> to_integer ni, false
| _ ->
Kernel.fatal ~current:true
"Array length %a is not a compile-time constant: \
@@ -4949,11 +4964,12 @@ and doAttr ghost (a: Cabs.attribute) : attribute list =
end
| Cabs.CONSTANT (Cabs.CONST_STRING s) -> AStr s
| Cabs.CONSTANT (Cabs.CONST_INT str) -> begin
- match (parseIntExp ~loc str).enode with
- | Const (CInt64 (v64,_,_)) ->
+ match parseIntExpRes ~loc str with
+ | Ok {enode = Const (CInt64 (v64,_,_)) } ->
AInt v64
| _ ->
- Kernel.fatal ~current:true "Invalid attribute constant: %s" str
+ Kernel.error ~current:true "Invalid attribute constant: %s" str;
+ AInt Integer.one
end
| Cabs.CONSTANT (Cabs.CONST_FLOAT str) ->
ACons ("__fc_float", [AStr str])
@@ -5295,7 +5311,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 *)
@@ -5491,7 +5507,7 @@ and makeCompType ghost (isstruct: bool)
match isIntegerConstant ghost w with
| None ->
Kernel.error ~source
- "bitfield width is not an integer constant";
+ "bitfield width is not a valid integer constant";
(* error does not immediately stop execution.
Hence, we return a placeholder here.
*)
@@ -5699,11 +5715,7 @@ and getIntConstExp ghost (aexp) : exp =
and isIntegerConstant ghost (aexp) : int option =
match doExp (ghost_local_env ghost) CMayConst aexp (AExp None) with
- | (_, c, e, _) when isEmpty c -> begin
- match Cil.constFoldToInt e with
- | Some n -> (try Some (Integer.to_int n) with Z.Overflow -> None)
- | _ -> None
- end
+ | (_, c, e, _) when isEmpty c -> constFoldToInteger e
| _ -> None
(* Process an expression and in the process do some type checking,
@@ -5988,7 +6000,15 @@ and doExp local_env
| Cabs.CONSTANT ct -> begin
match ct with
| Cabs.CONST_INT str -> begin
- let res = parseIntExp ~loc str in
+ let res =
+ match parseIntExpRes ~loc str with
+ | Ok e -> e
+ | Error 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
@@ -8467,7 +8487,13 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
let doidx = add_reads ~ghost idxe'.eloc r doidx in
match constFoldToInt idxe', isNotEmpty doidx with
- | Some x, false -> Integer.to_int x, doidx
+ | Some x, false ->
+ begin
+ match Integer.to_int_opt x with
+ | Some x' -> x', doidx
+ | None -> abort_context
+ "INDEX initialization designator overflows"
+ end
| _ ->
abort_context
"INDEX initialization designator is not a constant"
@@ -8504,11 +8530,11 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
if isNotEmpty doidxs || isNotEmpty doidxe then
Kernel.fatal ~current:true "Range designators are not constants";
let first, last =
- match constFoldToInt idxs', constFoldToInt idxe' with
- | Some s, Some e -> Integer.to_int s, Integer.to_int e
+ match constFoldToInteger idxs', constFoldToInteger idxe' with
+ | Some s, Some e -> s, e
| _ ->
Kernel.fatal ~current:true
- "INDEX_RANGE initialization designator is not a constant"
+ "INDEX_RANGE initialization designator is not a valid constant"
in
if first < 0 || first > last then
Kernel.error ~once:true ~current:true
@@ -10061,8 +10087,8 @@ and doStatement local_env (s : Cabs.statement) : chunk =
Kernel.error ~once:true ~current:true
"Case statement with a non-constant";
let il, ih =
- match constFoldToInt el', constFoldToInt eh' with
- | Some il, Some ih -> Integer.to_int il, Integer.to_int ih
+ match constFoldToInteger el', constFoldToInteger eh' with
+ | Some il, Some ih -> il, ih
| _ ->
Kernel.fatal ~current:true
"Cannot understand the constants in case range"
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index c60b1bb3b5a46aa9c4d125df8c79cf05d8de77db..89c96fbb3a542cb595dd29918779d84587c6ce5e 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -50,8 +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 -> { info with unroll_number = Some (Integer.to_int i) }
+ 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/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index c975b3ae78b8220b9190bdcd9a93547307a30811..c74c632fd471157741a88db11e59716d6860bd08 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -390,7 +390,7 @@ let cardinal_less_than t n =
| Some min, Some max -> Int.succ ((Int.e_div (Int.sub max min) t.modu))
in
if Int.le c (Int.of_int n)
- then Int.to_int c (* This is smaller than the original [n] *)
+ then Int.to_int_exn c (* This is smaller than the original [n] *)
else raise Not_less_than
let cardinal_zero_or_one t =
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 333d647b333a567117e91cc6790f3d6613e5531e..a3f2835ab6e091eddb0077dfcf7e6ff05fc02ee2 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -65,7 +65,7 @@ let zero_or_one = [| Int.zero ; Int.one |]
let inject_singleton e = [| e |]
let inject_periodic ~from ~period ~number =
- let l = Int.to_int number in
+ let l = Int.to_int_exn number in
let s = Array.make l Int.zero in
let v = ref from in
let i = ref 0 in
@@ -578,7 +578,7 @@ let complement_under ~min ~max set =
let card = Int.succ (Int.sub e b) in
if Int.(le card zero) then `Bottom
else if Int.le card (Int.of_int !small_cardinal)
- then `Set (Array.init (Int.to_int card) (fun i -> Int.add b (Int.of_int i)))
+ then `Set (Array.init (Int.to_int_exn card) (fun i -> Int.add b (Int.of_int i)))
else `Top (b, e, Int.one)
(* ------------------------------ Arithmetics ------------------------------- *)
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index 961bc56607173c1681c0ae81bd5a3f5db4f24de4..4c80214648e968ee8d0133f1fae77032438483e3 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -279,7 +279,7 @@ let cardinal_less_than v n =
| Itv i -> Extlib.the ~exn:Not_less_than (Int_interval.cardinal i)
in
if Int.le c (Int.of_int n)
- then Int.to_int c (* This is smaller than the original [n] *)
+ then Int.to_int_exn c (* This is smaller than the original [n] *)
else raise Not_less_than
let cardinal_is_less_than v n =
@@ -556,14 +556,14 @@ let create_all_values ~signed ~size =
let cast_int_to_int ~size ~signed value =
if equal top value
- then create_all_values ~size:(Int.to_int size) ~signed
+ then create_all_values ~size:(Int.to_int_exn size) ~signed
else
let result =
match value with
| Itv i -> inject_itv (Int_interval.cast ~size ~signed i)
| Set s ->
let all =
- create_all_values ~size:(Int.to_int size) ~signed
+ create_all_values ~size:(Int.to_int_exn size) ~signed
in
if is_included value all
then value
@@ -587,7 +587,7 @@ let all_values ~size = function
(Int.length mn mx)
end
| Set s as v ->
- let siz = Int.to_int size in
+ let siz = Int.to_int_exn size in
Int_set.cardinal s >= 1 lsl siz &&
equal
(cast_int_to_int ~size ~signed:false v)
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 48ec817fbb345852be98e235e867435995355ca7..21c4c92c52becd11f44f1fb5b5e901e84f3fe363 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -66,14 +66,14 @@ module Type : Type = struct
let inject_singleton e =
if Int.le Int.zero e && Int.le e Int.thirtytwo
- then small_nums.(Int.to_int e)
+ then small_nums.(Int.to_int_exn e)
else Int (Int_val.inject_singleton e)
let inject_int i =
try
let e = Int_val.project_int i in
if Int.le Int.zero e && Int.le e Int.thirtytwo
- then small_nums.(Int.to_int e)
+ then small_nums.(Int.to_int_exn e)
else Int i
with Int_val.Not_Singleton ->
if Int_val.(equal top i) then top else Int i
@@ -245,7 +245,7 @@ let inject_interval ~min ~max ~rem ~modu =
let subdivide ~size = function
| Bottom -> raise Can_not_subdiv
| Float fval ->
- let fkind = match Integer.to_int size with
+ let fkind = match Integer.to_int_exn size with
| 32 -> Fval.Single
| 64 -> Fval.Double
| _ -> raise Can_not_subdiv (* see Value/Value#105 *)
@@ -1043,11 +1043,11 @@ let reinterpret_as_float kind i =
let open Floating_point in
match kind with
| Cil_types.FDouble ->
- let conv v = Fval.F.of_float (Int64.float_of_bits (Int.to_int64 v)) in
+ let conv v = Fval.F.of_float (Int64.float_of_bits (Int.to_int64_exn v)) in
reinterpret
64 Fval.Double conv bits_of_most_negative_double bits_of_max_double
| Cil_types.FFloat ->
- let conv v = Fval.F.of_float(Int32.float_of_bits (Int.to_int32 v)) in
+ let conv v = Fval.F.of_float(Int32.float_of_bits (Int.to_int32_exn v)) in
reinterpret
32 Fval.Single conv bits_of_most_negative_float bits_of_max_float
| Cil_types.FLongDouble ->
diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml
index 99d9d1d00194abcf84301dea84d472b04902121d..05113200c9874e6c1788f18d98e131a062b16627 100644
--- a/src/kernel_services/analysis/bit_utils.ml
+++ b/src/kernel_services/analysis/bit_utils.ml
@@ -271,7 +271,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
if Integer.le new_start new_stop then
let new_bfinfo = match field.fbitfield with
| None -> Other
- | Some i -> Bitfield (Integer.to_int64 (Integer.of_int i))
+ | Some i -> Bitfield (Int64.of_int i)
in
let new_align =
Integer.e_rem (Integer.sub align start_o) env.rh_size
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index b7b405e03e22bcdb0f427db5397751fcfa38cc61..e40b51a88db810af67d5bbcdc17dbfe36bf3861d 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3233,21 +3233,21 @@ let parseIntAux (str:string) =
(* Convert to integer. To prevent overflow we do the arithmetic
* on Big_int and we take care of overflow. We work only with
* positive integers since the lexer takes care of the sign *)
- let rec toInt base (acc: Integer.t) (idx: int) : Integer.t =
+ let rec toInt base (acc: Integer.t) (idx: int) =
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;
- let acc' =
- Integer.add what (Integer.mul base acc) in
- toInt base acc' (idx + 1)
+ Error (Format.asprintf
+ "Invalid digit %a in integer literal '%s' in base %a."
+ (Integer.pretty ~hexa:false) what
+ str
+ (Integer.pretty ~hexa:false) base)
+ else
+ let acc' = Integer.add what (Integer.mul base acc) in
+ toInt base acc' (idx + 1)
in
if idx >= l - suffixlen then begin
- acc
+ Ok acc
end else
let ch = String.get str idx in
if ch >= '0' && ch <= '9' then
@@ -3257,7 +3257,8 @@ let parseIntAux (str:string) =
else if ch >= 'A' && ch <= 'F' then
doAcc (Integer.of_int (10 + Char.code ch - Char.code 'A'))
else
- Kernel.fatal ~current:true "Invalid integer constant: %s" str
+ Error (Format.asprintf
+ "Invalid character %c in integer literal: %s" ch str)
in
let i =
if octalhexbin && l >= 2 then
@@ -3273,24 +3274,36 @@ let parseIntAux (str:string) =
in
i,kinds
-let parseInt s = fst (parseIntAux s)
+let parseIntRes s = fst (parseIntAux s)
+
+let parseInt s =
+ match parseIntRes s with
+ | Ok i -> i
+ | Error msg -> Kernel.fatal ~current:true "%s" msg
let parseIntLogic ~loc str =
- let i,_= parseIntAux str in
+ let i = parseInt str in
{ term_node = TConst (Integer (i,Some str)) ; term_loc = loc;
term_name = []; term_type = Linteger;}
+let parseIntExpRes ~loc repr =
+ let i, kinds = parseIntAux repr in
+ Result.bind i
+ (fun i ->
+ let rec loop = function
+ | k::rest ->
+ if fitsInInt k i then (* i fits in the current type. *)
+ Ok (kinteger64 ~loc ~repr ~kind:k i)
+ else loop rest
+ | [] ->
+ Error (Format.asprintf "Cannot represent the integer %s" repr)
+ in
+ loop kinds)
+
let parseIntExp ~loc repr =
- 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
+ match parseIntExpRes ~loc repr with
+ | Ok e -> e
+ | Error msg -> Kernel.fatal ~current:true "%s" msg
let mkStmtCfg ~before ~(new_stmtkind:stmtkind) ~(ref_stmt:stmt) : stmt =
let new_ = { skind = new_stmtkind;
@@ -4102,7 +4115,9 @@ and alignOfField (fi: fieldinfo) =
and intOfAttrparam (a:attrparam) : int option =
let rec doit a : int =
match a with
- | AInt(n) -> Integer.to_int n
+ | 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
@@ -4410,9 +4425,9 @@ and bitsSizeOf t =
Const(CInt64(l,_,_)) ->
let sz = Integer.mul (Integer.of_int (bitsSizeOf bt)) l in
let sz' =
- try
- Integer.to_int sz
- with Z.Overflow ->
+ match Integer.to_int_opt sz with
+ | Some i -> i
+ | None ->
raise
(SizeOfError
("Array is so long that its size can't be "
@@ -4483,7 +4498,7 @@ and bitsOffset (baset: typ) (off: offset) : int * int =
| Index(e, off) -> begin
let ei =
match constFoldToInt e with
- | Some i -> Integer.to_int i
+ | Some i -> Integer.to_int_exn i
| None -> raise (SizeOfError ("Index is not constant", baset))
in
let bt = typeOf_array_elem baset in
@@ -4839,7 +4854,7 @@ let bitsSizeOfBitfield typlv =
match unrollType typlv with
| TInt (_, attrs) | TEnum (_, attrs) as t ->
(match findAttribute bitfield_attribute_name attrs with
- | [AInt i] -> Integer.to_int i
+ | [AInt i] -> Integer.to_int_exn i
| _ -> bitsSizeOf t)
| t -> bitsSizeOf t
@@ -5666,7 +5681,7 @@ let rec integralPromotion t = (* c.f. ISO 6.3.1.1 *)
begin match findAttribute bitfield_attribute_name a with
| [AInt size] ->
(* This attribute always fits in int. *)
- let size = Integer.to_int size in
+ let size = Integer.to_int_exn size in
let sizeofint = bitsSizeOf intType in
let attrs = remove_attributes_for_integral_promotion a in
let kind =
@@ -5996,7 +6011,10 @@ let lenOfArray64 eo =
ni
| _ -> raise LenOfArray
end
-let lenOfArray eo = Integer.to_int (lenOfArray64 eo)
+let lenOfArray eo =
+ match Integer.to_int_opt (lenOfArray64 eo) with
+ | None -> raise LenOfArray
+ | Some l -> l
(*** Make an initializer for zeroing a data type ***)
let rec makeZeroInit ~loc (t: typ) : init =
@@ -6028,7 +6046,7 @@ let rec makeZeroInit ~loc (t: typ) : init =
| TArray(bt, Some len, _, _) as t' ->
let n =
match constFoldToInt len with
- | Some n -> Integer.to_int n
+ | Some n -> Integer.to_int_exn n
| _ -> Kernel.fatal ~current:true "Cannot understand length of array"
in
let initbt = makeZeroInit ~loc bt in
@@ -6074,7 +6092,7 @@ let foldLeftCompound
| Some lene -> begin
match constFoldToInt lene with
| Some i ->
- let len_array = Integer.to_int i in
+ let len_array = Integer.to_int_exn i in
let len_init = List.length initl in
if len_array <= len_init then
default () (* enough elements in the initializers list *)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 094edf994283d3c9d53793a8298cd168929bc394..6b051a1e72eb2d5ec4b1d6a27bb80e0f12756dcc 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -606,8 +606,9 @@ val isArrayType: typ -> bool
(** True if the argument is a struct of union type *)
val isStructOrUnionType: typ -> bool
-(** Raised when {!Cil.lenOfArray} fails either because the length is [None]
- * or because it is a non-constant expression *)
+(** Raised when {!Cil.lenOfArray} fails either because the length is [None],
+ * because it is a non-constant expression, or because it overflows an int.
+*)
exception LenOfArray
(** Call to compute the array length as present in the array type, to an
@@ -1035,15 +1036,25 @@ 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.
- Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL.
-*)
+(** 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. *)
val parseInt: string -> Integer.t
+
+(** Like [parseInt], but returns [Error message] in case of failure, instead of
+ aborting Frama-C.
+ @since Frama-C+dev *)
+val parseIntRes: string -> (Integer.t, string) result
+
+(** Like [parseInt], but converts to an expression. *)
val parseIntExp: loc:location -> string -> exp
-val parseIntLogic: loc:location -> string -> term
-(** 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 [parseIntExp], but returns [Error message] in case of failure, instead
+ of aborting Frama-C.
+ @since Frama-C+dev *)
+val parseIntExpRes: loc:location -> string -> (exp, string) result
+
+(** Like [parseInt], but converts to a logic term. *)
+val parseIntLogic: loc:location -> string -> term
val appears_in_expr: varinfo -> exp -> bool
(** @return true if the given variable appears in the expression. *)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index e568ddfc6aa1980f10b3d288ff3378fd865161f2..6cc3eae47434dd59d302d80b6cf8a52ba20823af 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -275,7 +275,15 @@ let constant_to_lconstant c = match c with
LReal (real_of_float s f)
let lconstant_to_constant c = match c with
- | Integer (i,s) -> CInt64(i,Cil.intKindForValue i false,s)
+ | Integer (i,s) ->
+ begin
+ try
+ CInt64(i,Cil.intKindForValue i false,s)
+ with Cil.Not_representable ->
+ Kernel.fatal
+ "Cannot represent logical integer in C: %a"
+ (Integer.pretty ~hexa:false) i
+ end
| LStr s -> CStr s
| LWStr s -> CWStr s
| LChr s -> CChr s
diff --git a/src/libraries/stdlib/integer.ml b/src/libraries/stdlib/integer.ml
index 103b96f8acbe155e7f9a7d17cd17f17ca09ac5a7..20412be44c5849c3990fca4312bc6ca45e259e49 100644
--- a/src/libraries/stdlib/integer.ml
+++ b/src/libraries/stdlib/integer.ml
@@ -97,9 +97,20 @@ let of_int = Z.of_int
let of_int64 = Z.of_int64
let of_int32 = Z.of_int32
-let to_int = Z.to_int
-let to_int64 = Z.to_int64
-let to_int32 = Z.to_int32
+let to_int_exn = Z.to_int
+let to_int64_exn = Z.to_int64
+let to_int32_exn = Z.to_int32
+
+(* These functions are deprecated (renamed to *_exn) and will be removed
+ in a future version. *)
+let to_int = to_int_exn
+let to_int64 = to_int64_exn
+let to_int32 = to_int32_exn
+
+let wrap to_int i = try Some (to_int i) with Z.Overflow -> None
+let to_int_opt = wrap Z.to_int
+let to_int64_opt = wrap Z.to_int64
+let to_int32_opt = wrap Z.to_int32
let of_string = Z.of_string
let to_string = Z.to_string
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index 5a3019d2b082c88a077a406e04772eaa4f147005..1c341b3a7a97c7f6a8d6f91c50664d3b3f080441 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -122,9 +122,66 @@ val of_int : int -> t
val of_int64 : Int64.t -> t
val of_int32 : Int32.t -> t
-val to_int : t -> int (** @raise Z.Overflow if too big *)
-val to_int64 : t -> int64 (** @raise Z.Overflow if too big *)
-val to_int32 : t -> int32 (** @raise Z.Overflow if too big *)
+(**
+ @raise Z.Overflow if too big
+ @deprecated Frama-C+dev Renamed to [to_int_exn].
+ Also consider using [to_int_opt].
+*)
+val to_int : t -> int [@@deprecated]
+
+(**
+ @raise Z.Overflow if too big
+ @deprecated Frama-C+dev Renamed to [to_int64_exn].
+ Also consider using [to_int64_opt].
+*)
+val to_int64 : t -> int64 [@@deprecated]
+
+(**
+ @raise Z.Overflow if too big
+ @deprecated Frama-C+dev Renamed to [to_int32_exn].
+ Also consider using [to_int32_opt].
+*)
+val to_int32 : t -> int32 [@@deprecated]
+
+(**
+ @raise Z.Overflow if too big
+ @since Frama-C+dev
+*)
+val to_int_exn : t -> int
+
+(**
+ @raise Z.Overflow if too big
+ @since Frama-C+dev
+*)
+val to_int64_exn : t -> int64
+
+(**
+ @raise Z.Overflow if too big
+ @since Frama-C+dev
+*)
+val to_int32_exn : t -> int32
+
+(**
+ Returns [Some i] if the number can be converted to an [int],
+ or [None] otherwise.
+ @since Frama-C+dev
+*)
+val to_int_opt : t -> int option
+
+(**
+ Returns [Some i] if the number can be converted to an [int64],
+ or [None] otherwise.
+ @since Frama-C+dev
+*)
+val to_int64_opt : t -> int64 option
+
+(**
+ Returns [Some i] if the number can be converted to an [int32],
+ or [None] otherwise.
+ @since Frama-C+dev
+*)
+val to_int32_opt : t -> int32 option
+
val to_float : t -> float
val of_float : float -> t
diff --git a/src/libraries/utils/floating_point.ml b/src/libraries/utils/floating_point.ml
index 39461ef8d170fd2929bfe2abfb6647c32733dd9b..49be26a813e5d081869f30134b0c70c1e8357db9 100644
--- a/src/libraries/utils/floating_point.ml
+++ b/src/libraries/utils/floating_point.ml
@@ -101,7 +101,7 @@ let make_float ~num ~den ~exp ~man_size ~min_exp ~max_exp =
let rem2 = (* twice the remainder *)
Integer.shift_left rem Integer.one
in
- let man = Integer.to_int64 man in
+ let man = Integer.to_int64_exn man in
(* Format.printf "pre-round: num den man rem:@\n%a@\n@\n%a@\n@\n%Ld@\n@\n%a@."
Datatype.Integer.pretty num Datatype.Integer.pretty den
man Datatype.Integer.pretty rem; *)
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index c4c50da4b0eea223343f0fae79e8a77914cffe76..86437066d6b713ffaf8ab5bd60984cea227a78f9 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -28,7 +28,7 @@ let show_aorai_variable state fmt var_name =
let cvalue = !Db.Value.eval_expr state (Cil.evar vi) in
try
let i = Ival.project_int (Cvalue.V.project_ival cvalue) in
- let state_name = Data_for_aorai.getStateName (Integer.to_int i) in
+ let state_name = Data_for_aorai.getStateName (Integer.to_int_exn i) in
Format.fprintf fmt "%s" state_name
with Cvalue.V.Not_based_on_null | Ival.Not_Singleton_Int |
Z.Overflow | Not_found ->
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 4a40b1c088a88fbc176bdef0f27857c23cea3c3a..3d001b2524b0f7d6fd532cae5bcbdafd2f5a340f 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -1835,7 +1835,7 @@ let absolute_range loc min =
let max = find_max_value loc in
match max with
| Some { term_node = TConst(Integer (t,_)) } ->
- Interval(min,Integer.to_int t)
+ Interval(min,Integer.to_int_exn t)
| Some x ->
Bounded (min, Logic_const.term x.term_node x.term_type)
| None -> Unbounded min
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 04724d513b504014bc702496717c082f8bc61dc4..846efe7afebbcd7599027b5a183068a98c62b728 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -160,7 +160,7 @@ let join i1 i2 = match i1, i2 with
(* if the interval of integers fits into the float types, then return
this float type; otherwise return Rational *)
(try
- let to_float n = Int64.to_float (Integer.to_int64 n) in
+ let to_float n = Int64.to_float (Integer.to_int64_exn n) in
let mini, maxi = to_float min, to_float max in
let minf, maxf = match k with
| FFloat ->
@@ -224,7 +224,7 @@ let meet i1 i2 = match i1, i2 with
(* if the float type fits into the interval of integers, then return
this float type; otherwise return Rational *)
(try
- let to_float n = Int64.to_float (Integer.to_int64 n) in
+ let to_float n = Int64.to_float (Integer.to_int64_exn n) in
let mini, maxi = to_float min, to_float max in
if mini <= f && maxi >= f then Float(k, Some f) else Ival Ival.bottom
with Z.Overflow | Exit ->
@@ -243,7 +243,7 @@ let meet i1 i2 = match i1, i2 with
(* if the float type fits into the interval of integers, then return
this float type; otherwise return Rational *)
(try
- let to_float n = Int64.to_float (Integer.to_int64 n) in
+ let to_float n = Int64.to_float (Integer.to_int64_exn n) in
let mini, maxi = to_float min, to_float max in
let minf, maxf = match k with
| FFloat ->
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 5266965f380027bb921c0bc82538219872020458..448cba21c748a362471580206b36de98237956ab 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -55,7 +55,7 @@ let constant_to_exp ~loc env t c =
(* too large integer *)
Cil.mkString ~loc (Integer.to_string n), Typed_number.Str_Z
| Typing.C_float fkind ->
- Cil.kfloat ~loc fkind (Int64.to_float (Integer.to_int64 n)), C_number
+ Cil.kfloat ~loc fkind (Int64.to_float (Integer.to_int64_exn n)), C_number
| Typing.C_integer kind ->
let cast = Typing.get_cast ~lenv:(Env.Local_vars.get env) t in
match cast, kind with
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 07d9a21b6a174aa2badfe63aa534e16f4e17cb98..cc2cad5aa3d9539ff879db58b42f9e0ed6ff258a 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -261,7 +261,7 @@ let sufficiently_aligned vi algn =
(fun acc attr ->
match attr with
| Attr("align", [AInt i]) ->
- let alignment = Integer.to_int i in
+ let alignment = Integer.to_int_exn i in
if acc <> 0 && acc <> alignment then begin
(* multiple align attributes with different values *)
Options.error
diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml
index 43a3fd5b4913cfa2ccb8e7653694cbabe38e1ed2..e0f658242e3677cfa8992113cac7bb0754b04c45 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/src/plugins/loop_analysis/loop_analysis.ml
@@ -450,7 +450,7 @@ module Store(* (B:sig *)
Printer.pp_varinfo vi pretty_increment increment
else
try
- let value = (Integer.to_int (Integer.c_div bound_offset increment)) in
+ let value = (Integer.to_int_exn (Integer.c_div bound_offset increment)) in
let adjusted_value =
if (binop = Cil_types.Le && Integer.(equal remainder zero))
|| (not Integer.(equal remainder zero))
@@ -462,7 +462,7 @@ module Store(* (B:sig *)
success := true;
add_loop_bound stmt adjusted_value
end
- with Z.Overflow -> (* overflow in Integer.to_int *)
+ with Z.Overflow -> (* overflow in Integer.to_int_exn *)
()
(* TODO: check if this is useful and does not cause false alarms
else
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index f112996ac4771ed771ee90d64027b2b8fdf3b54a..ae9be58a85904f013915c8555f84bdc20da5980b 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -243,7 +243,7 @@ let translate_lval = function
let translate_constant = function
| CInt64 (i, _, _) -> begin
- try Coeff.s_of_int (Integer.to_int i) (* TODO: skip OCaml int type *)
+ try Coeff.s_of_int (Integer.to_int_exn i) (* TODO: skip OCaml int type *)
with Z.Overflow | Failure _ -> raise (Out_of_Scope "translate_constant big int")
end
| _ -> raise (Out_of_Scope "translate_constant not integer")
@@ -272,7 +272,7 @@ let rec translate_expr eval oracle expr = match expr.enode with
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
match Cil.constFoldToInt expr with
| None -> raise (Out_of_Scope "translate_expr sizeof alignof")
- | Some i -> Texpr1.Cst (Coeff.s_of_int (Integer.to_int i))
+ | Some i -> Texpr1.Cst (Coeff.s_of_int (Integer.to_int_exn i))
(* Expressions that cannot be translated by [translate_expr] are replaced
using an oracle. Of course, this oracle must be sound!. If the oracle
cannot find a suitable replacement, it can re-raise the expresssion. *)
diff --git a/src/plugins/value/domains/cvalue/builtins_print_c.ml b/src/plugins/value/domains/cvalue/builtins_print_c.ml
index 88c3a58a4fa49b19efc2fdaf53c6c7b93bc92841..d73d76bde382eb383e0563235a544ff8801e88e9 100644
--- a/src/plugins/value/domains/cvalue/builtins_print_c.ml
+++ b/src/plugins/value/domains/cvalue/builtins_print_c.ml
@@ -234,9 +234,9 @@ let offsetmap_pretty cas name print_ampamp fmt offsm =
let ek = Integer.succ ek in
if Integer.is_zero (Integer.e_rem ek Integer.eight)
then
- let step = if iso then 1 else (Integer.to_int modu) / 8 in
- let start = ref ((Integer.to_int bk) / 8) in
- let ek = Integer.to_int ek in
+ let step = if iso then 1 else (Integer.to_int_exn modu) / 8 in
+ let start = ref ((Integer.to_int_exn bk) / 8) in
+ let ek = Integer.to_int_exn ek in
let ek = ek / 8 in
if ek / step > 1_000_000 (* arbitrary limit *) then
raise Too_large_to_enumerate;
diff --git a/src/plugins/value/domains/cvalue/builtins_split.ml b/src/plugins/value/domains/cvalue/builtins_split.ml
index bcc7c2e5a68bc717203ed39264932f5ba88bdfd5..75e71fea2ebba821cb3358e22ab870da893fbf01 100644
--- a/src/plugins/value/domains/cvalue/builtins_split.ml
+++ b/src/plugins/value/domains/cvalue/builtins_split.ml
@@ -178,7 +178,7 @@ let aux_split f state = function
let states =
try
let max_card =
- Integer.to_int (Ival.project_int (V.project_ival_bottom card))
+ Integer.to_int_exn (Ival.project_int (V.project_ival_bottom card))
in
f ~warn:true lv state max_card
with V.Not_based_on_null | Ival.Not_Singleton_Int ->
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index 97bae714d07b173d5a56aac6c858e699cef058da..0d130a9fec42d9235083b8212f3382b15c2a5b0c 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -154,7 +154,7 @@ let search_offsetmap_range kind offsetmap validity ~min ~max ~v_size acc =
let size = kind.size in
(* Reads will repeat themselves every [modu] bits. *)
let modu = Integer.ppcm v_size size in
- let max_reads = Integer.(to_int (e_div modu size)) in
+ let max_reads = Integer.(to_int_exn (e_div modu size)) in
(* Performs [max_reads] consecutive reads from offsets {[min] + k[modu]},
bound by [max]. *)
let search_until ~max acc =
diff --git a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
index 2ae3ce11c47ef2a8aaf2dcf3cc877a2fa7c8e34b..be8049588a16c235f5a451f8e8237572ace8ab4c 100644
--- a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
@@ -84,9 +84,9 @@ let make_watch_value target_value = Value target_value
let make_watch_cardinal target_value =
try
let target_value = Cvalue.V.project_ival target_value in
- Cardinal (Integer.to_int (Ival.project_int target_value))
+ Cardinal (Integer.to_int_exn (Ival.project_int target_value))
with V.Not_based_on_null | Ival.Not_Singleton_Int
- | Z.Overflow (* from Integer.to_int *) ->
+ | Z.Overflow (* from Integer.to_int_exn *) ->
raise Builtins.Outside_builtin_possibilities
let () =
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ml b/src/plugins/value/domains/numerors/numerors_domain.ml
index e2afa36684c692128b90b61eed91623cce461df9..eaec32fbb9f436c37b2580dddcd6f49e080fdfa3 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ml
@@ -134,12 +134,12 @@ let reduce_cast (module Abstract: Abstractions.S) =
let ival = Cvalue.V.project_ival cvalue in
match Ival.min_and_max ival with
| Some min, Some max ->
- let min, max = Integer.to_int min, Integer.to_int max in
+ let min, max = Integer.to_int_exn min, Integer.to_int_exn max in
let prec = Numerors_utils.Precisions.of_fkind fkind in
let num = Numerors_value.of_ints ~prec min max in
set Numerors_value.key num result
| _, _ -> result
- (* Integer.to_int may fail for too big integers. *)
+ (* Integer.to_int_exn may fail for too big integers. *)
with Cvalue.V.Not_based_on_null | Z.Overflow -> result
end
| _, _ -> result
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index ac6f7ec43022ebb5850cf0e972d2d616a3b097f6..677b519020ead6dcc18e2ec04fc7fe039dccd42f 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -770,7 +770,7 @@ module Make
if nb > 3
then
let pow = Integer.power_int_positive_int in
- (subdivnb * nb) / (Integer.to_int (pow 2 (nb - 1)))
+ (subdivnb * nb) / (Integer.to_int_exn (pow 2 (nb - 1)))
else subdivnb
in
Value_parameters.result ~current:true ~once:true ~dkey
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index e4213e09f8552300a151b5ef37bf39e272247aba..1867b8a07201ab6228366f4fb1cff4ce9c212815 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -336,13 +336,11 @@ struct
let eval_exp_to_int state exp =
let _valuation, ival = evaluate_exp_to_ival state exp in
- try
- Integer.to_int (Ival.project_int ival)
+ try Integer.to_int_exn (Ival.project_int ival)
with
| Ival.Not_Singleton_Int ->
fail ~exp "this partitioning parameter must evaluate to a singleton"
- | Failure _ ->
- fail ~exp "this partitioning parameter is too big"
+ | Z.Overflow -> fail ~exp "this partitioning parameter overflows an integer"
let split_by_predicate state predicate =
let env =
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index 519e2fc02290aabc32213050079494afe4a23073..1c8dae31e042b527e8e036cf404045966d193176 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -93,11 +93,11 @@ struct
let t =
Cil.visitCilTerm (new Logic_utils.simplify_const_lval global_init) t
in
- match Logic_utils.constFoldTermToInt t with
- | Some n -> Partition.IntLimit (Integer.to_int n)
- | None ->
- try
- Partition.ExpLimit (term_to_exp t)
+ let i = Logic_utils.constFoldTermToInt t in
+ match Option.bind i Integer.to_int_opt with
+ | Some n -> Partition.IntLimit n
+ | None ->
+ try Partition.ExpLimit (term_to_exp t)
with Db.Properties.Interp.No_conversion ->
warn "loop unrolling parameters must be valid expressions; \
ignoring";
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index ec1962985575cb0ea17007b62b3b03d6dc81c09c..d954d3e4a060f50a9dee1b810a404ca471021a5d 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -142,7 +142,7 @@ module Slevel = Register (struct
| TConst (LStr "default") -> SlevelDefault
| TConst (LStr "merge") -> SlevelMerge
| TConst (LStr "full") -> SlevelFull
- | TConst (Integer (i, _)) -> SlevelLocal (Integer.to_int i)
+ | TConst (Integer (i, _)) -> SlevelLocal (Integer.to_int_exn i)
| _ -> SlevelDefault (* be kind. Someone is bound to write a visitor
that will simplify our term into something
unrecognizable... *)
@@ -288,7 +288,7 @@ module Subdivision = Register (struct
let export i = Ext_terms [Logic_const.tinteger i]
let import = function
- | Ext_terms [{term_node = TConst (Integer (i, _))}] -> Integer.to_int i
+ | Ext_terms [{term_node = TConst (Integer (i, _))}] -> Integer.to_int_exn i
| _ -> assert false
let print fmt i = Format.pp_print_int fmt i
diff --git a/src/plugins/value/utils/eval_typ.ml b/src/plugins/value/utils/eval_typ.ml
index bbd8633c2eda4f042b8857d2be1b298d2ba48f87..01c976e7a6bfba8b47117219ed521a9cc85a5746 100644
--- a/src/plugins/value/utils/eval_typ.ml
+++ b/src/plugins/value/utils/eval_typ.ml
@@ -186,7 +186,7 @@ let ik_attrs_range ik attrs =
let i_bits =
match bitfield_size_attributes attrs with
| None -> Cil.bitsSizeOfInt ik
- | Some size -> Integer.to_int size
+ | Some size -> Integer.to_int_exn size
in
{ i_bits; i_signed = Cil.isSigned ik }
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index f6fd8d3fd663c0c763a80f814b1d343015a6cabe..084c8eac252539a9d4f6f098008ee013ee8f6b75 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -129,7 +129,7 @@ let explode_range o (b, e) =
let explode o =
let r = ref o in
let aux (e, b) _ =
- r := explode_range !r (Integer.to_int e, Integer.to_int b)
+ r := explode_range !r (Integer.to_int_exn e, Integer.to_int_exn b)
in
V_Offsetmap.iter aux o;
List.rev (V_Offsetmap.fold (fun r v acc -> (r, v) :: acc) !r [])
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 0fdd5f2fea59bd6a63b227433c8c022e8b681597..777e49b571ffdd246d66d329319d75c9a2e0fdf0 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -642,7 +642,7 @@ module V = struct
else value
let shift_bits ~topify ~offset ~size v =
- let v = restrict_topint_to_size v (Integer.to_int size) in
+ let v = restrict_topint_to_size v (Integer.to_int_exn size) in
shift_left_by_integer ~topify offset v
let merge_distinct_bits ~topify ~conflate_bottom value acc =
diff --git a/src/plugins/wp/Auto.ml b/src/plugins/wp/Auto.ml
index ee0fe1759f47e01cebf45c413895292b308c2019..1acae65f1a304d5682b6e844e19e1480e14da11c 100644
--- a/src/plugins/wp/Auto.ml
+++ b/src/plugins/wp/Auto.ml
@@ -165,13 +165,13 @@ struct
let ranges rg =
Tmap.interf
(fun _ a b ->
- try Some(Integer.to_int a,Integer.to_int b)
+ try Some(Integer.to_int_exn a,Integer.to_int_exn b)
with Z.Overflow -> None
) rg.vmin rg.vmax
let small = function
| None -> None
- | Some z -> try Some(Integer.to_int z) with Z.Overflow -> None
+ | Some z -> try Some(Integer.to_int_exn z) with Z.Overflow -> None
let bounds rg =
Tmap.merge
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 0b9c00f9c279ba44ebd35381f70c86b138036d94..f658fb960d3d81374da97757d420fa320f02a569 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -177,8 +177,8 @@ let match_power2, _match_power2_minus1 =
in let hsb p =
let n = Integer.shift_right p Integer.sixteen in
Integer.of_int (if Integer.is_zero n
- then hsb (Integer.to_int p)
- else 16 + hsb (Integer.to_int n))
+ then hsb (Integer.to_int_exn p)
+ else 16 + hsb (Integer.to_int_exn n))
in let rec hsb_aux p =
let n = Integer.shift_right p Integer.thirtytwo in
if Integer.is_zero n then hsb p
diff --git a/src/plugins/wp/Filtering.ml b/src/plugins/wp/Filtering.ml
index bfa668f2ab61f0d6c9939d4df21b47a47daf2db7..e9181a34ebebd43fd3914eb8edbdc4405ec0905f 100644
--- a/src/plugins/wp/Filtering.ml
+++ b/src/plugins/wp/Filtering.ml
@@ -211,7 +211,7 @@ struct
begin match F.repr k with
| Kint z ->
let d =
- try Dindex(Integer.to_int z) with Z.Overflow -> Darray in
+ try Dindex(Integer.to_int_exn z) with Z.Overflow -> Darray in
X( x , ds @ [ d ] )
| _ ->
let ds = ds @ [ Darray ] in
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index e53e58af9be9a3735492aeeefcba76ed0faa6e54..e08946df3de2743a715726d38307fc91d6cfef70 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -242,7 +242,7 @@ struct
match F.repr a with
| L.Add es -> List.fold_left walk s es
| L.Kint z ->
- (try s + Integer.to_int z
+ (try s + Integer.to_int_exn z
with Z.Overflow -> s)
| _ -> s
in walk 0 k
@@ -345,10 +345,10 @@ struct
match F.repr a with
| L.Add es -> List.fold_left get_linear poly es
| L.Kint z ->
- (try (Integer.to_int z,F.e_one)::poly
+ (try (Integer.to_int_exn z,F.e_one)::poly
with Z.Overflow -> (1,a)::poly)
| L.Times(c,e) ->
- (try (Integer.to_int c,e)::poly
+ (try (Integer.to_int_exn c,e)::poly
with Z.Overflow -> (1,a)::poly)
| _ -> (1,a)::poly
diff --git a/src/plugins/wp/Plang.ml b/src/plugins/wp/Plang.ml
index 5f2fac2bd0077b367c7aaa3733fad26bc04b0853..71c3aecea32c9a4e7ada8df82c13f125348905aa 100644
--- a/src/plugins/wp/Plang.ml
+++ b/src/plugins/wp/Plang.ml
@@ -108,7 +108,7 @@ class engine =
method pp_int _ fmt z =
try
- let n = Integer.to_int z in
+ let n = Integer.to_int_exn z in
if -256 <= n && n <= 256 then
Format.pp_print_int fmt n
else
diff --git a/src/plugins/wp/RegionAnnot.ml b/src/plugins/wp/RegionAnnot.ml
index deab22ad92fe69838ee0ab9cf016d8826ede1435..08cf3b9e386295e0ee4a6e1b9e837c9f82432f68 100644
--- a/src/plugins/wp/RegionAnnot.ml
+++ b/src/plugins/wp/RegionAnnot.ml
@@ -67,7 +67,7 @@ type region_spec = {
let get_int e =
match Logic_utils.constFoldTermToInt e with
| None -> None
- | Some a -> Some (Integer.to_int a)
+ | Some a -> Some (Integer.to_int_exn a)
let get_int_option = function
| None -> None
diff --git a/src/plugins/wp/TacBittest.ml b/src/plugins/wp/TacBittest.ml
index e46016ae364043e6d6518bf3bbfd449bba1ae907..683746d8c39d5ccbea105b5a49a8639874f4f573 100644
--- a/src/plugins/wp/TacBittest.ml
+++ b/src/plugins/wp/TacBittest.ml
@@ -32,7 +32,7 @@ let power k = F.e_bigint (Integer.two_power_of_int k)
let lookup_int e =
let open Qed.Logic in
match F.repr e with
- | Kint z -> (try Some (Integer.to_int z) with Z.Overflow -> None)
+ | Kint z -> (try Some (Integer.to_int_exn z) with Z.Overflow -> None)
| _ -> None
let rec lookup_bittest e =
diff --git a/src/plugins/wp/TacInstance.ml b/src/plugins/wp/TacInstance.ml
index 5fe1df231753c940be0032732ae5699e2bf3108e..3592e7b15cac3e83d3782af78091c6de886d70c0 100644
--- a/src/plugins/wp/TacInstance.ml
+++ b/src/plugins/wp/TacInstance.ml
@@ -68,7 +68,7 @@ let rec complexity = function
let cardinal limit bindings =
let n = complexity bindings in
if Integer.le n (Integer.of_int limit)
- then Some (Integer.to_int n) else None
+ then Some (Integer.to_int_exn n) else None
let rec bind_exists bindings property =
match bindings with
diff --git a/src/plugins/wp/TacShift.ml b/src/plugins/wp/TacShift.ml
index 4745ccdd8d8942d671a31548b5779769b0f8d4ea..43f4f9171cc9d2d358a75a1ce299b53e4c62d897 100644
--- a/src/plugins/wp/TacShift.ml
+++ b/src/plugins/wp/TacShift.ml
@@ -45,7 +45,7 @@ let select_op f =
let select_int n =
match F.repr n with
| Qed.Logic.Kint n ->
- (try Integer.to_int n with Z.Overflow -> raise Not_found)
+ (try Integer.to_int_exn n with Z.Overflow -> raise Not_found)
| _ -> raise Not_found
class shift =
diff --git a/src/plugins/wp/Tactical.ml b/src/plugins/wp/Tactical.ml
index 036c2a3e730d35789ce956303aef770c4a6d28c3..fd61c19fe3b1fda56a35d3e3419c57d597229cf8 100644
--- a/src/plugins/wp/Tactical.ml
+++ b/src/plugins/wp/Tactical.ml
@@ -107,7 +107,7 @@ let selected = function
| Compose code -> composed code
let get_int_z z =
- try Some (Integer.to_int z) with Z.Overflow -> None
+ try Some (Integer.to_int_exn z) with Z.Overflow -> None
let get_int = function
| Empty -> None
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 493022e5bf1ee392ad205b910429c25a331ef8ca..a748662b125a457d52fe8821f12b718bf4427423 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -169,7 +169,7 @@ and get_nth_list k = function
let rewrite_nth s k =
match F.repr k with
| L.Kint z ->
- let k = try Integer.to_int z with Z.Overflow -> raise Not_found in
+ let k = try Integer.to_int_exn z with Z.Overflow -> raise Not_found in
if 0 <= k then get_nth k s else raise Not_found
| _ -> raise Not_found
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 374fda3f93978b0669ff93edbea5e4c6bad67546..37ee20c37e9de8de572e2bbd01fae890cbe9a02d 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -233,13 +233,13 @@ let f_name = f_memo (Pretty_utils.to_string pp_float)
(* --- Array Info --- *)
(* -------------------------------------------------------------------------- *)
-let char c = Integer.to_int64 (Cil.charConstToInt c)
+let char c = Integer.to_int64_exn (Cil.charConstToInt c)
let constant e =
match (Cil.constFold true e).enode with
| Const(CInt64(k,_,_)) ->
begin
- try Integer.to_int64 k
+ try Integer.to_int64_exn k
with Z.Overflow ->
Warning.error "Array size too large (%a)" (Integer.pretty ~hexa:true) k
end
@@ -247,12 +247,12 @@ let constant e =
let get_int e =
match (Cil.constFold true e).enode with
- | Const(CInt64(k,_,_)) -> Some (Integer.to_int k)
+ | Const(CInt64(k,_,_)) -> Some (Integer.to_int_exn k)
| _ -> None
let get_int64 e =
match (Cil.constFold true e).enode with
- | Const(CInt64(k,_,_)) -> Some (Integer.to_int64 k)
+ | Const(CInt64(k,_,_)) -> Some (Integer.to_int64_exn k)
| _ -> None
let dimension t =
diff --git a/tests/misc/interpreted_automata_dataflow_forward.ml b/tests/misc/interpreted_automata_dataflow_forward.ml
index 82d1b8a654c2663b5f85d66e8e26d4d38b2e7a40..4f9d2aa51ed8b031bc29afaba08158f246a7b8cd 100644
--- a/tests/misc/interpreted_automata_dataflow_forward.ml
+++ b/tests/misc/interpreted_automata_dataflow_forward.ml
@@ -34,7 +34,7 @@ struct
let rec eval v exp =
match exp.enode with
| Const (CInt64 (i,_,_)) ->
- (try Integer.to_int i with _ -> raise Not_constant)
+ (try Integer.to_int_exn i with _ -> raise Not_constant)
| Lval (Var vi, NoOffset) ->
(try Map.find vi v with Not_found -> raise Not_constant)
| SizeOf typ ->
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.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..db573af932d7288a94e547a1e729ad2581a7c585
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[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: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] 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.1.res.oracle b/tests/syntax/oracle/very_large_integers.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..23cfa866c0b1679b16c8da7e786139aeb6c49151
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.1.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:29: User Error:
+ Cannot represent the integer 99999999999999999999U
+[kernel] tests/syntax/very_large_integers.c:29: User Error:
+ Cannot represent the integer 99999999999999999999U
+[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] 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.10.res.oracle b/tests/syntax/oracle/very_large_integers.10.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4f848474e09b65819663cd76d18d5f514f53c968
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
@@ -0,0 +1,11 @@
+[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: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 0000000000000000000000000000000000000000..c352a476c8d0b1515924c1ac46c2014c9c8c1d55
--- /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
new file mode 100644
index 0000000000000000000000000000000000000000..bb5f47fe756242bc9ba320bc6435621eb289b4e1
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.2.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:36: User Error:
+ integer constant too large in expression 9999999999999999999U
+[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.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.3.res.oracle b/tests/syntax/oracle/very_large_integers.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ad9de534b05aef91ec8a722ad0b193c72ef89375
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.3.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[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.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.4.res.oracle b/tests/syntax/oracle/very_large_integers.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0d8599e32958e49f9a178eaa551bc2692388d0cb
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:45: User Error:
+ INDEX initialization designator overflows
+ 43
+ 44 #ifdef INIT_DESIGNATOR2
+ 45 int arr3[1] = { [9999999999999999999U] = 42 };
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..1798bfe46e3610238348f88b53f77a757bb82440
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:49: User Error:
+ integer constant too large in expression -9999999999999999999U
+[kernel] tests/syntax/very_large_integers.c:49: User Error:
+ integer constant too large in expression 9999999999999999999U
+[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.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.6.res.oracle b/tests/syntax/oracle/very_large_integers.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c531dfb15a1f18822fb312d21c18796860aae437
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.6.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing tests/syntax/very_large_integers.c (with preprocessing)
+[kernel] tests/syntax/very_large_integers.c:53: User Error:
+ Invalid attribute constant: 0x80000000000000000
+[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] 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.7.res.oracle b/tests/syntax/oracle/very_large_integers.7.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..75dbebc66e69abf8a3bedb63843d538f6957ce7c
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -0,0 +1,10 @@
+[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] Failure: Cannot represent logical integer in C: 9999999999999999999
+[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.8.res.oracle b/tests/syntax/oracle/very_large_integers.8.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a0898661e147feeff6bc975032c9c15c8f0f9fd0
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -0,0 +1,11 @@
+[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: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.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.9.res.oracle b/tests/syntax/oracle/very_large_integers.9.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9ed0fe33d85bcd2a4c2cbca98f244296c17a65c1
--- /dev/null
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
@@ -0,0 +1,12 @@
+[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: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
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/very_large_integers.c b/tests/syntax/very_large_integers.c
new file mode 100644
index 0000000000000000000000000000000000000000..80e80299c6dc82f3f76654a45efd9e587e1e307a
--- /dev/null
+++ b/tests/syntax/very_large_integers.c
@@ -0,0 +1,91 @@
+/* run.config
+ PLUGIN: @EVA_PLUGINS@
+ EXIT: 1
+ STDOPT: #"-cpp-extra-args=-DBITFIELD"
+ STDOPT: #"-cpp-extra-args=-DARRAY_DECL"
+ STDOPT: #"-cpp-extra-args=-DCASE_RANGE"
+ STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR"
+ STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR2"
+ STDOPT: #"-cpp-extra-args=-DRANGE_DESIGNATOR"
+ 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=-DCABS_DOWHILE"
+ EXIT: 0
+ STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
+*/
+
+volatile int nondet;
+
+#ifdef BITFIELD
+struct st {
+ int bf:(999999999999999999+9999999999999999999);
+};
+#endif
+
+#ifdef ARRAY_DECL
+int arr[9999999999999999999U+18000000000000000000U];
+char arr1[99999999999999999999U];
+#endif
+
+#ifdef CASE_RANGE
+unsigned long nondetul;
+void case_range() {
+ switch (nondetul)
+ case 0 ... 9999999999999999999U:;
+}
+#endif
+
+#ifdef INIT_DESIGNATOR
+int arr2[9999999999999999999U] = { [9999999999999999999U] = 42 };
+#endif
+
+#ifdef INIT_DESIGNATOR2
+int arr3[1] = { [9999999999999999999U] = 42 };
+#endif
+
+#ifdef RANGE_DESIGNATOR
+int arr4[1] = { [-9999999999999999999U ... 9999999999999999999U] = 42 };
+#endif
+
+#ifdef ATTRIBUTE_CONSTANT
+struct acst {
+ int a __attribute__((aligned(0x80000000000000000)));
+};
+#endif
+
+typedef struct {
+ char a;
+ int b __attribute__((aligned(0x8000000000000000)));
+ double c __attribute__((aligned(0x8000000000000000+0x8000000000000000)));
+} stt ;
+
+//@ logic integer too_large_integer = 9999999999999999999;
+
+#ifdef LOGIC_CONSTANT
+//@ type too_large_logic_array = int[9999999999999999999U];
+#endif
+
+#ifdef LOGIC_CONSTANT_OCTAL
+//@ type too_large_logic_array_octal = int[09876543210];
+#endif
+
+int main() {
+#ifdef EVA_UNROLL
+ //@ loop unroll (-9999999999999999999); // IntLimit
+ while (nondet);
+ //@ loop unroll too_large_integer; // ExpLimit
+ while (nondet);
+ //@ slevel 9999999999999999999;
+ while (nondet);
+#endif
+#ifdef CABS_DOWHILE
+ do { } while (09);
+#endif
+#ifdef UNROLL_PRAGMA
+ //@ loop pragma UNROLL 99999999999999999999;
+#endif
+ while (nondet);
+ return 0;
+}