mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
bb17d3f33b
* Update with new ocplib simplex API * Update opam file * Poetry * Updating docker build for fixing CI * Test * Revert "Test" This reverts commit 6246358f16ac538e90f6a2a8105b4e4ca7df11b4. * Revert "Updating docker build for fixing CI" This reverts commit 1038e105cff5605f6c343ab1f581ec171ffdad91. * Perform docker actions only on specific branches. * Prevent git to replace LF line endings by CRLF line endings on Windows * poetry * Use Fpath library to manage paths in a cross-platform manner. * Revert "Simplify the tests by using the dirname as an indicator of the expected" This reverts commit9ce98e3167. * Revert "Revert "Move tests to the new directory."" This reverts commit74c0073cd4. * Revert "Revert "Fix dublicate names"" This reverts commit961e1ff9c7. * Remove old non-regression directory (again) * Add challenge tests. * Add expected results for challenges * Gentest depends on Alt-Ergo bin. * Attempt to fix the CI using the package name for building AE * Attempt to fix the JS CI * Require dune 3 * Create a opam package for the javascript version * Add a public_name for the new executable alt-ergo-js * Remove useless functions * New opam package for js * Try OCaml 4.14 to fix js_of_ocaml * Revert "Try OCaml 4.14 to fix js_of_ocaml" This reverts commit ae9fa6a6568eec5294a9d6be6c9a08bb8a3f7c82. * Test again * Attempt to fix JS CI again * Use ocaml 4.10 for js building. * Improve the Makefile by using dune targets. * Fix release building * poetry * Rollback to Dune 2.8 * Dune 2.8 required * The flag --no-source-map is broken It seems that Dune between 2.8 and < 3 gives the flags --no-source-map to the linker of js_of_ocaml instead of the compiler. I removed it temporary. * Revert "The flag --no-source-map is broken" This reverts commit 0276ba8c4a7c5a0229d165f3b7218ca900e00bea. * poetry * Fix * Try again with Dune 3... * Revert "Try again with Dune 3..." This reverts commit 5e3072a35411739df53040fc980fbae227200dfc. * Revert "Fix" This reverts commit 3011f62df02a92591ee0b310f4750fbdaea91a94. * Revert "poetry" This reverts commit 5fa6fd7373abe1cbfe1af76f49f086439eac1f46. * Revert "Revert "The flag --no-source-map is broken"" This reverts commit ab3a00351cb091bddd007e160f0c38855a4f88bc. * Revert "The flag --no-source-map is broken" This reverts commit 0276ba8c4a7c5a0229d165f3b7218ca900e00bea. * Revert "Dune 2.8 required" This reverts commit 20fa214236c1df68bc901619b281d2e6aa27fb7c. * Revert "Rollback to Dune 2.8" This reverts commit 88464f3121cf7ee35c2b38e41a6187e3450fc9e6. * poetry by Steven :p * Fix double condition on Dune version * poetry * peotry * Attempt to fix CI by update opam repository * Update opam repository in the CI * Wrong action order * Simplify CI with opam 2.1 * Test on windows CI * Revert "Test on windows CI" This reverts commit 12083fd270d2953ccde9915ceb67fd0d7c1b9eb0. * Update cache action to the version 3 * Force update of the cache on Windows * Revert "Force update of the cache on Windows" This reverts commit 08e0ee5f2a9d26c9d934ad710867293755b61883. * Disable opam-depext in setup-ocaml action. This feature is not necessary with opam 2.1 also * Revert "Disable opam-depext in setup-ocaml action. This feature is not necessary with opam 2.1 also" This reverts commit 2149c2a830fbbd01249e845d7bde00907952c178. * Try another repository on Windows * Disable depext on Windows * Revert "Disable depext on Windows" This reverts commit af1fa301acb26d215fd76efe3075df02d6f92857. * Revert "Revert "Disable depext on Windows"" This reverts commit 4c0fe58fd911b13ed8893f628c11732f7e0c947c. * Fix windows CI * Try ocaml 4.14 on windows * Add the usual repository Co-authored-by: Steven de Oliveira <de.oliveira.steven@gmail.com>
21 lines
555 B
Plaintext
21 lines
555 B
Plaintext
type memory
|
|
type uint16
|
|
logic integer_of_uint16 : uint16 -> int
|
|
logic uint16_of_integer : int -> uint16
|
|
|
|
axiom uint16_coerce :
|
|
(forall x:int. (((0 <= x) and (x <= 65535)) ->
|
|
(integer_of_uint16(uint16_of_integer(x)) = x)))
|
|
axiom uint16_extensionality :
|
|
(forall x:uint16.
|
|
(forall y:uint16. ((integer_of_uint16(x) = integer_of_uint16(y)) ->
|
|
(x = y))))
|
|
|
|
logic is1 : uint16, memory -> prop
|
|
axiom itis : (forall m:memory. is1(uint16_of_integer(1), m))
|
|
logic ptr : memory
|
|
logic return : uint16
|
|
axiom ok : integer_of_uint16(return) = 1
|
|
|
|
goal g2 : is1(return,ptr)
|