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_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..56148ceea37f55841cc6dfb4972e0611bdfe8ab9 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 (Integer.to_int64_exn (Integer.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 67bec896462c4c54511b01ac9f65398fb0ece194..20f5d9dcd12bca20800a00f726e1b1be03f8de59 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4506,7 +4506,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
@@ -4862,7 +4862,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
@@ -5689,7 +5689,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 =
@@ -6054,7 +6054,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
@@ -6100,7 +6100,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/libraries/stdlib/integer.ml b/src/libraries/stdlib/integer.ml
index 2b68a32bcc1570e82eaa41170d844c93c9ccdbdc..20412be44c5849c3990fca4312bc6ca45e259e49 100644
--- a/src/libraries/stdlib/integer.ml
+++ b/src/libraries/stdlib/integer.ml
@@ -97,9 +97,15 @@ 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
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index 989c259f5974d9e7c19ee9946398eb30a774a357..1c341b3a7a97c7f6a8d6f91c50664d3b3f080441 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -124,21 +124,42 @@ val of_int32 : Int32.t -> t
(**
@raise Z.Overflow if too big
- @deprecated Frama-C+dev use [to_int_opt] instead
+ @deprecated Frama-C+dev Renamed to [to_int_exn].
+ Also consider using [to_int_opt].
*)
-val to_int : t -> int
+val to_int : t -> int [@@deprecated]
(**
@raise Z.Overflow if too big
- @deprecated Frama-C+dev use [to_int64_opt] instead
+ @deprecated Frama-C+dev Renamed to [to_int64_exn].
+ Also consider using [to_int64_opt].
*)
-val to_int64 : t -> int64
+val to_int64 : t -> int64 [@@deprecated]
(**
@raise Z.Overflow if too big
- @deprecated Frama-C+dev use [to_int32_opt] instead
+ @deprecated Frama-C+dev Renamed to [to_int32_exn].
+ Also consider using [to_int32_opt].
*)
-val to_int32 : t -> int32
+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],
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 704d1a792dfa3139236a83b396a7974530d25bd9..98ed76a0cd39bb79d449c74ea5eca6509ef8cd96 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -1840,7 +1840,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 78b80a60185f378f23fe8626a61d5e9f8bb729a0..1867b8a07201ab6228366f4fb1cff4ce9c212815 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -336,7 +336,7 @@ 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"
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 ->