projects
/
platform
/
upstream
/
gcc.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
42c54ad
)
[Ada] Adapt ghost code to maintain proof
author
Yannick Moy
<moy@adacore.com>
Tue, 4 Jan 2022 09:37:53 +0000
(10:37 +0100)
committer
Pierre-Marie de Rodat
<derodat@adacore.com>
Tue, 11 Jan 2022 13:24:47 +0000
(13:24 +0000)
gcc/ada/
* libgnat/s-expmod.adb (Exp_Modular): Add assertions.
gcc/ada/libgnat/s-expmod.adb
patch
|
blob
|
history
diff --git
a/gcc/ada/libgnat/s-expmod.adb
b/gcc/ada/libgnat/s-expmod.adb
index
61faed1
..
60d86e5
100644
(file)
--- a/
gcc/ada/libgnat/s-expmod.adb
+++ b/
gcc/ada/libgnat/s-expmod.adb
@@
-278,6
+278,7
@@
is
(Big (Result) * Big (Factor) ** (Exp - 1),
Big (Left) ** Right));
Lemma_Exp_Expand (Big (Factor), Exp - 1);
+ pragma Assert (Exp / 2 = (Exp - 1) / 2);
end if;
Lemma_Exp_Expand (Big (Factor), Exp);
@@
-286,6
+287,8
@@
is
exit when Exp = 0;
Rest := Big (Factor) ** Exp;
+ pragma Assert (Equal_Modulo
+ (Big (Result) * (Rest * Rest), Big (Left) ** Right));
Lemma_Exp_Mod (Big (Factor) * Big (Factor), Exp, Big (Modulus));
pragma Assert
((Big (Factor) * Big (Factor)) ** Exp = Rest * Rest);