Merge branch 'topic/fsf_merge_269/20251022' into 'fsf'

Synchronize with GNAT

Issue: eng/spark/spark2014#269

See merge request eng/spark/why3!99

Author: marc-adacore

.gitattributes

@@ -17,9 +17,11 @@ src/config.sh.in binary
 /.dockerignore export-ignore
 /.gitlab-ci.yml export-ignore
 /.mailmap export-ignore
+/.ocp-indent export-ignore
 /check.sh export-ignore
 
 /bench/encoding/ export-ignore
+/bench/copy_oracles.sh export-ignore
 /examples_in_progress/ export-ignore
 /misc/ export-ignore
 /opam/ export-ignore

.gitlab-ci.yml

@@ -138,9 +138,7 @@ trywhy3-extra:
   image: "debian:bullseye-slim"
   script:
     - misc/ci-trywhy3.sh
-  only:
-    variables:
-      - $NEW_TRYWHY3_EXTRA
+  when: manual
   artifacts:
     paths:
       - trywhy3

CHANGES.md

@@ -1,5 +1,32 @@
 :x: marks a potential source of incompatibility
 
+Version 1.8.2, September 16, 2025
+---------------------------
+
+Compilation
+  * compatibility with OCaml 5.4 (MR !1228)
+
+Provers
+  * fix soundness bug with floats in Alt-Ergo 2.6.x (issue #905)
+
+Sessions
+  * fix issue with file identifiers in sessions (MR !1231)
+
+Extraction
+  * restore compatibility of OCaml extraction with js_of_ocaml
+
+Version 1.8.1, June 4, 2025
+---------------------------
+
+Core
+  * fix cloning of injective records
+
+Miscellaneous
+  * fix compilation error with GCC 15
+
+Plugins
+  * resurrect the BDD-infer loop invariant generation plug-in
+
 Version 1.8.0, December 11, 2024
 --------------------------------
 
@@ -15,8 +42,9 @@ Standard library
 
 Core
   * records and range types now have some predefined symbol `foo'eq`
-    and some axiom `foo'inj` to express injectivity. See manual
-    Section "The WhyML Language Reference/Record Types".
+    and some axiom `foo'inj` to express injectivity; see Section
+    "The WhyML Language Reference/Record Types" of the manual
+    (contribution by Loïc Correnson)
 
 Transformations
   * new transformation `extensionality` to help with equality proofs
@@ -44,15 +72,18 @@ Tools
   * `why3 pp`: dropped option `--kind` :x:
 
 Extraction
-  * added support for Java, see Manual, Section "Executing WhyML Programs"
+  * added support for Java; see Section "Executing WhyML Programs" of the manual
+    (contribution by Gérald Point)
   * improved extraction to C: floating-point numbers, global variables
 
 API
-  * changed how resource limits are specified :x
-  * renamed type `effect` to `effekt` for compatibility with OCaml 5.3 :x
+  * changed how resource limits are specified :x:
+  * renamed type `effect` to `effekt` for compatibility with OCaml 5.3 :x:
 
 Miscellaneous
   * dependency on OCaml library `num` was replaced by `zarith`
+  * added support for native Windows compilation through Opam 2.2
+    (contribution by Basile Deslosges)
 
 Version 1.7.2, April 18, 2024
 -----------------------------

Makefile.in

@@ -1,12 +1,11 @@
 ####################################################################
 #                                                                  #
 #  The Why3 Verification Platform   /   The Why3 Development Team  #
-#  Copyright 2010-2024 --  Inria - CNRS - Paris-Saclay University  #
+#  Copyright 2010-2025 --  Inria - CNRS - Paris-Saclay University  #
 #                                                                  #
 #  This software is distributed under the terms of the GNU Lesser  #
 #  General Public License version 2.1, with the special exception  #
 #  on linking described in file LICENSE.                           #
-#                                                                  #
 ####################################################################
 
 .DELETE_ON_ERROR:
@@ -420,7 +419,7 @@ clean::
 ifeq (@enable_ppx@,yes)
 src/util/ppx_debug_optim$(EXE): src/util/debug_optim.ml
 	$(SHOW) 'Linking $@'
-	$(HIDE) $(OCAMLFIND) opt -package compiler-libs.common -linkpkg src/util/debug_optim.ml -o $@
+	$(HIDE) $(OCAMLFIND) opt -package ppxlib -linkpkg src/util/debug_optim.ml -o $@
 
 ifeq (@OCAML_OS_TYPE@,Win32)
 # Relative calls to executable on Windows cannot use / as path separator

bench/check-ce-bench

@@ -314,10 +314,12 @@ for file in $files; do
           ;;
       "float_div")
           skipae=yes
+          altergosteps=1000
+          altergostepsrac=$altergosteps
           ;;
       "floats")
           skipae=yes
-          altergosteps=1000
+          altergosteps=100
           altergostepsrac=$altergosteps
           cvc5stepsrac=10000
           z3steps=100000

bench/check-ce/oracles/float_div_Alt-Ergo,2.6.2_SP.oracle

@@ -1,7 +1,7 @@
 Warning: Error while checking function definition type match_mode: Function arity mismatch when interpreting
 (Function ()
   (Ssimple (Isymbol A1))
-  (Var (Qannotident (Isymbol (Sprover @a31)) (Ssimple (Isymbol A1)))))
+  (Var (Qannotident (Isymbol (Sprover @a33)) (Ssimple (Isymbol A1)))))
 with lsymbol match_mode
 Warning: Error while interpreting tqtisFinite: No variable in bound_vars matching qualified identifier (Qident (Isymbol t1))
 
@@ -14,11 +14,11 @@ Warning: Error while interpreting tqtisFinite: No variable in bound_vars matchin
   - Abstract RAC: NORMAL
 File "bench/check-ce/float_div.mlw", line 24, characters 11-25:
 Sub-goal Assertion of goal f'vc.
-Prover result is: Unknown (unknown) (245 steps).
+Prover result is: Unknown (unknown) (255 steps).
 The following counterexample model could not be verified
   (both RAC terminated because Precondition of `f` cannot be evaluated):
 File ieee_float.mlw:
-  Line 934:
+  Line 950:
     zeroF :  = <UNDEFINED>
 File float_div.mlw:
   Line 19:
@@ -28,8 +28,8 @@ File float_div.mlw:
 Warning: Error while checking function definition type match_mode: Function arity mismatch when interpreting
 (Function ()
   (Ssimple (Isymbol A1))
-  (Var (Qannotident (Isymbol (Sprover @a31)) (Ssimple (Isymbol A1)))))
-with lsymbol match_mode
+  (Var (Qannotident (Isymbol (Sprover @a33)) (Ssimple (Isymbol A1)))))
+with lsymbol match_mode1
 Warning: Error while interpreting tqtisFinite: No variable in bound_vars matching qualified identifier (Qident (Isymbol t1))
 
 <check_ce:categorization>Categorizations of models:
@@ -43,7 +43,7 @@ t'real x = (1.0 /' 4.0) as an argument)
 t'real x = (1.0 /' 4.0) as an argument)
 File "bench/check-ce/float_div.mlw", line 40, characters 11-25:
 Sub-goal Assertion of goal f'vc.
-Prover result is: Unknown (unknown) (245 steps).
+Prover result is: Unknown (unknown) (255 steps).
 The following counterexample model could not be verified
   (both RAC fatal rac error: cannot evaluate builtin mul because cannot interpret term epsilon x:t.
 t'real x = (1.0 /' 4.0) as an argument):
@@ -90,23 +90,29 @@ File ieee_float.mlw:
       t
       ->
       t = (fun _arg_06 _arg_16 -> {t'real => Apply(infix /, 1.0 4.0)})
-  Line 194:
+  Line 161:
+    plus_infinity : t = {t'real => Apply(infix /, 1.0 4.0)}
+  Line 164:
+    minus_infinity : t = {t'real => Apply(infix /, 1.0 4.0)}
+  Line 167:
+    not_a_number : t = {t'real => Apply(infix /, 1.0 4.0)}
+  Line 210:
     of_int :
       mode
       ->
       int
       ->
       t = (fun _arg_05 _arg_15 -> {t'real => Apply(infix /, 1.0 4.0)})
-  Line 280:
+  Line 296:
     from_real :
       mode
       ->
       real
       ->
       t = (fun _arg_04 _arg_14 -> {t'real => Apply(infix /, 1.0 4.0)})
-  Line 678:
+  Line 694:
     is_int : t -> bool = [|_ => true|]
-  Line 934:
+  Line 950:
     zeroF : t = {t'real => Apply(infix /, 1.0 4.0)}
 File float_div.mlw:
   Line 35:

bench/check-ce/oracles/float_div_Alt-Ergo,2.6.2_WP.oracle

@@ -1,7 +1,7 @@
 Warning: Error while checking function definition type match_mode: Function arity mismatch when interpreting
 (Function ()
   (Ssimple (Isymbol A1))
-  (Var (Qannotident (Isymbol (Sprover @a31)) (Ssimple (Isymbol A1)))))
+  (Var (Qannotident (Isymbol (Sprover @a33)) (Ssimple (Isymbol A1)))))
 with lsymbol match_mode
 Warning: Error while interpreting tqtisFinite: No variable in bound_vars matching qualified identifier (Qident (Isymbol t1))
 
@@ -14,11 +14,11 @@ Warning: Error while interpreting tqtisFinite: No variable in bound_vars matchin
   - Abstract RAC: NORMAL
 File "bench/check-ce/float_div.mlw", line 24, characters 11-25:
 Sub-goal Assertion of goal f'vc.
-Prover result is: Unknown (unknown) (245 steps).
+Prover result is: Unknown (unknown) (255 steps).
 The following counterexample model could not be verified
   (both RAC terminated because Precondition of `f` cannot be evaluated):
 File ieee_float.mlw:
-  Line 934:
+  Line 950:
     zeroF :  = <UNDEFINED>
 File float_div.mlw:
   Line 19:
@@ -28,8 +28,8 @@ File float_div.mlw:
 Warning: Error while checking function definition type match_mode: Function arity mismatch when interpreting
 (Function ()
   (Ssimple (Isymbol A1))
-  (Var (Qannotident (Isymbol (Sprover @a31)) (Ssimple (Isymbol A1)))))
-with lsymbol match_mode
+  (Var (Qannotident (Isymbol (Sprover @a33)) (Ssimple (Isymbol A1)))))
+with lsymbol match_mode1
 Warning: Error while interpreting tqtisFinite: No variable in bound_vars matching qualified identifier (Qident (Isymbol t1))
 
 <check_ce:categorization>Categorizations of models:
@@ -43,7 +43,7 @@ t'real x = (1.0 /' 4.0) as an argument)
 t'real x = (1.0 /' 4.0) as an argument)
 File "bench/check-ce/float_div.mlw", line 40, characters 11-25:
 Sub-goal Assertion of goal f'vc.
-Prover result is: Unknown (unknown) (245 steps).
+Prover result is: Unknown (unknown) (255 steps).
 The following counterexample model could not be verified
   (both RAC fatal rac error: cannot evaluate builtin mul because cannot interpret term epsilon x:t.
 t'real x = (1.0 /' 4.0) as an argument):
@@ -90,23 +90,29 @@ File ieee_float.mlw:
       t
       ->
       t = (fun _arg_06 _arg_16 -> {t'real => Apply(infix /, 1.0 4.0)})
-  Line 194:
+  Line 161:
+    plus_infinity : t = {t'real => Apply(infix /, 1.0 4.0)}
+  Line 164:
+    minus_infinity : t = {t'real => Apply(infix /, 1.0 4.0)}
+  Line 167:
+    not_a_number : t = {t'real => Apply(infix /, 1.0 4.0)}
+  Line 210:
     of_int :
       mode
       ->
       int
       ->
       t = (fun _arg_05 _arg_15 -> {t'real => Apply(infix /, 1.0 4.0)})
-  Line 280:
+  Line 296:
     from_real :
       mode
       ->
       real
       ->
       t = (fun _arg_04 _arg_14 -> {t'real => Apply(infix /, 1.0 4.0)})
-  Line 678:
+  Line 694:
     is_int : t -> bool = [|_ => true|]
-  Line 934:
+  Line 950:
     zeroF : t = {t'real => Apply(infix /, 1.0 4.0)}
 File float_div.mlw:
   Line 35: