From ec736052069a58941ab127a2ee6ebdb37b874284 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 24 Sep 2020 15:09:53 +0200
Subject: [PATCH] [wp] Update oracles
---
.../wp_acsl/oracle/chunk_typing.res.oracle | 17 ++++++++-------
.../wp_acsl/oracle/struct_fields.res.oracle | 21 ++++++++++---------
.../04c1fcb3dde99404e56f398c9d3c7b31.json | 2 ++
.../09419c3fbb6dc84c7ea4daf3841c155f.json | 2 ++
.../0af3d5135623c7629e8792c15c73e11e.json | 2 ++
.../1d2ed0d831c17546d006475b478b59c1.json | 2 ++
.../281d06f1268fc1f6bae73c9b23a370f6.json | 2 ++
.../35644610983981a71b83b5427a68f6c0.json | 2 ++
.../6367c7d1e56f1af80ad76d813e09b66a.json | 2 ++
.../675a842c7ec32528e5e21888634a1279.json | 2 ++
.../7ea33aa4c8dc9c1ed12a312a5a7b96ed.json | 2 ++
.../a76226839c540aad032cd3b9de095b89.json | 2 ++
.../bd67f73e3ff115a9f45b4244c20611fe.json | 2 ++
.../e046513e2f30f1a1946d5d6e40ef9129.json | 2 ++
.../e434135b1fa122e6a232e26709df80a5.json | 2 ++
.../e8e066b606c41e89f82b2aa3eef46a68.json | 2 ++
.../e9c784c595bc40819eff858fbcc12bab.json | 2 ++
.../efda69b6f9003dcb53f99c442ec8c4de.json | 2 ++
.../f6b163a1cc48d21b279ce315660ffd85.json | 2 ++
.../f97c74763d0222ed9be7c3fa666ce4e9.json | 2 ++
.../feca65e917b9c99c3286ceebc5a4d618.json | 2 ++
.../23316fd95fd7b645f6e7ee1ac0ec11dd.json | 2 ++
.../af1c6e5e9ad0ce51ef02350de25db7b1.json | 1 +
.../e7547aa0621803b4e7d628af9dae8742.json | 2 ++
.../0aaa8433bdd863a175c8f7aa27b5b23b.json | 1 +
.../1235102376d88a3bdb52f3e4e1c49883.json | 2 ++
.../55cf143d013d4eb3345feb58b26b90df.json | 2 ++
.../6203cf6d36b297213c87a78442bb23a3.json | 1 +
.../7d35e079640e61a3109774eff9ba7fe6.json | 1 +
.../bd22ac48c200239c37396cb5c074a071.json | 1 +
.../d3883c78b48ca2e9439df35f88b59d8c.json | 1 +
.../da21dd780a181597dd44b362df8f5670.json | 1 +
.../320f90061a8c50bf116b388e086c7897.json | 2 ++
.../28c1570cd2d3e97ddd579e328c469acf.json | 1 +
.../5bfdad2f5b18af371b905b94799e1cc0.json | 2 ++
.../7ac4f3e9696602b90e6fd7dbef86293c.json | 2 ++
.../c520b8395718f1f484266fd4e5983d1e.json | 2 ++
.../647e4705204771b6a78e805ee29cba26.json | 1 +
.../94f13affa6f3b5126e172fdc6062be2e.json | 2 ++
.../10fef2083d54144639f0b6cd94778cb5.json | 2 ++
.../52fdcb4ddd856ebb4464834c99aebae0.json | 2 ++
.../76a1b1317f2520ef9a599a12e344730d.json | 2 ++
.../786eb6ddc8b4a1c15c3182f42e302b10.json | 2 ++
.../c47ae970e7baa8aa14a744f568b77922.json | 2 ++
.../d3570f7a7a9be38c8599ac1773a618a2.json | 2 ++
.../08ff774ac6a70674d784cefe233dc1ab.json | 2 ++
.../82750bb2b6c7b7cda9f4f22eea23f1ef.json | 2 ++
.../e6bfe72a35736c49013701f4e6cc2d7c.json | 2 ++
.../152adf213328a70d06d3041ea7eca814.json | 1 +
.../cdfaa1f77a537214fe4d4d473da0c93f.json | 2 ++
.../dbca0c75b09289a0939a4568bccb8ffe.json | 2 ++
.../e3abd032ee5753e542d0c3d7701189e4.json | 2 ++
.../ce56b654edab77f40b10056e97cc5df5.json | 2 ++
.../2de8075c9ff8cf4d4f231608bed835a9.json | 2 ++
.../91244a7f80eb57f7181e1278e1172cc9.json | 2 ++
.../a59cc9b3f7f8b4a6624a1d1232662c22.json | 2 ++
.../a93f056d32a8ace3dd916b64068f94c2.json | 2 ++
.../aafe330c4b6932bf122ff6509f3fc2b0.json | 2 ++
.../0d14213263b1d1def509095c28e95ea9.json | 2 ++
.../5c04a7d9d73560b7116ff3914824c36d.json | 2 ++
.../7cf5fa10093d1ce2fd3940954cba0727.json | 2 ++
.../857d1f9981d68d1406859c8aae1b4639.json | 2 ++
.../9ad7d025e7eb0eec65fb3551668328c9.json | 2 ++
.../0ee6d92adc52cf841d8f421ae8b9d2f2.json | 2 ++
.../0f47526247a0528c7b0b8c8e945b32bd.json | 2 ++
.../3220ff8d08680b2082f90cfbabe5515c.json | 2 ++
.../3c1da17d2eb3aa57d9920fdbb8fdc9ff.json | 2 ++
.../f6d37791a1137bc07941a661f2333b7e.json | 2 ++
.../0748144945def11ea300e135d8482e4a.json | 2 ++
.../0b916424d61743046a3a8aa2d1980ca0.json | 2 ++
.../0f63fa83c61794d80fd003f133e182a7.json | 2 ++
.../1784d421c70ac778d245b285417fda0f.json | 2 ++
.../1fe4ca1fb351003ccbd8755355135f8a.json | 2 ++
.../21a3de19df739b18752521529d786b4b.json | 2 ++
.../25def53021ebb0a8629e796358a6848b.json | 2 ++
.../27bf4adc6f09a58eafeabec80e08e561.json | 2 ++
.../2ad8e6939da759ba7083da389f70b19a.json | 2 ++
.../2b04374aa95473cfa45c6abca5d0fe15.json | 2 ++
.../2de5619cd6bf8a4549f18cbf2daefbba.json | 2 ++
.../3b096d1ad2f60d27d68c9819789fceb4.json | 2 ++
.../3d5c736c9ebc4a910745c54e3f810000.json | 2 ++
.../4524f3b1a3aaeae1f14f29cffc5532b4.json | 2 ++
.../45fc8639c2e8c14a8ba57fe664c24c9d.json | 2 ++
.../4833c149c493290f7476cb694c326889.json | 2 ++
.../51225dc69fc56402c586cbf2cad99281.json | 2 ++
.../5998e90eb1b10fc1fd4ff54e6ef5689e.json | 2 ++
.../5d20435c0b8e9bb4e51ab262b3129648.json | 2 ++
.../5d3f4ea5bf6dc3f773faf7e0d63f1c76.json | 2 ++
.../6e15ce103fe14e50af7e0936d1d2a924.json | 1 +
.../75158755074596f3fba764a01a862cea.json | 2 ++
.../77066c103c80ea4e5f9b5605057d8d03.json | 2 ++
.../78c65afc8eeed0925d1f9c68b047f97a.json | 2 ++
.../7e81584b97fe9a89bed8cd913741db47.json | 2 ++
.../805d516e173e9a1980e332963ed26853.json | 2 ++
.../85bd4f374f9098d4767c14833e05b5b8.json | 2 ++
.../904dfd55419e9da26d6710c5e3bb2512.json | 2 ++
.../93d52e79f66a5fbbf8a8d577d910215e.json | 2 ++
.../9e3b12919ddd0b7f3deeaa63da75f6e5.json | 2 ++
.../a82a6af66093c860d0011d4f227136d1.json | 2 ++
.../a8e0d95eaca351657706fd30bd03bea1.json | 2 ++
.../a9311c935f353c4d4cea656ea0ab8a1e.json | 2 ++
.../b2ad64f1c1643c7dd2550c00a9074f69.json | 2 ++
.../b2ddcd489f338024c524107b6e504a00.json | 2 ++
.../bfe86eb3dc31cfbaa90471047107b2d3.json | 2 ++
.../c89d9d7df15c1516409d246b82b8c1f0.json | 2 ++
.../cf7eaa96c53ed9bc0ce7eef2ff6d4785.json | 2 ++
.../d73fc9500445fd11b1277eb233677128.json | 2 ++
.../dfb4426937ac0dd3319b8d97b1113ef1.json | 2 ++
.../e3c7c32c0e592dcd434f4f389ed60f36.json | 2 ++
.../e90a80dc6573ff3be6973ff12e676e32.json | 2 ++
.../ef4bb98ab16552a98c74ec0913047b5d.json | 2 ++
.../f6abbe317c0d2a1424b05d2fb7e4bd9b.json | 2 ++
.../f9262c0413f25f71d0ae44d4744746f0.json | 2 ++
.../1097cb045925dc7690981f0f528ee5d4.json | 2 ++
.../d89912a1e879d06f335b8d985cb804f3.json | 2 ++
.../de777917ace9bbef5272bb764ddd82c2.json | 2 ++
.../3016a12fe9f82a49a0ff618ae2acf170.json | 2 ++
.../3016a12fe9f82a49a0ff618ae2acf170.json | 2 ++
.../89c62021b110300d0866feac14bd7c45.json | 1 +
.../b602aeb805673b0805c79216c3ced563.json | 1 +
.../8d2cbdde2b0c4740b0467e8f84939e0d.json | 2 ++
121 files changed, 245 insertions(+), 18 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/04c1fcb3dde99404e56f398c9d3c7b31.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/09419c3fbb6dc84c7ea4daf3841c155f.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/0af3d5135623c7629e8792c15c73e11e.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/1d2ed0d831c17546d006475b478b59c1.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/281d06f1268fc1f6bae73c9b23a370f6.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/35644610983981a71b83b5427a68f6c0.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/6367c7d1e56f1af80ad76d813e09b66a.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/675a842c7ec32528e5e21888634a1279.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/7ea33aa4c8dc9c1ed12a312a5a7b96ed.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/a76226839c540aad032cd3b9de095b89.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/bd67f73e3ff115a9f45b4244c20611fe.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e046513e2f30f1a1946d5d6e40ef9129.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e434135b1fa122e6a232e26709df80a5.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e8e066b606c41e89f82b2aa3eef46a68.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e9c784c595bc40819eff858fbcc12bab.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/efda69b6f9003dcb53f99c442ec8c4de.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f6b163a1cc48d21b279ce315660ffd85.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f97c74763d0222ed9be7c3fa666ce4e9.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/feca65e917b9c99c3286ceebc5a4d618.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/23316fd95fd7b645f6e7ee1ac0ec11dd.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/af1c6e5e9ad0ce51ef02350de25db7b1.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/e7547aa0621803b4e7d628af9dae8742.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/0aaa8433bdd863a175c8f7aa27b5b23b.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/1235102376d88a3bdb52f3e4e1c49883.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/55cf143d013d4eb3345feb58b26b90df.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/6203cf6d36b297213c87a78442bb23a3.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/7d35e079640e61a3109774eff9ba7fe6.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/bd22ac48c200239c37396cb5c074a071.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/d3883c78b48ca2e9439df35f88b59d8c.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/da21dd780a181597dd44b362df8f5670.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.0.session/cache/320f90061a8c50bf116b388e086c7897.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/28c1570cd2d3e97ddd579e328c469acf.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/5bfdad2f5b18af371b905b94799e1cc0.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/7ac4f3e9696602b90e6fd7dbef86293c.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/c520b8395718f1f484266fd4e5983d1e.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/647e4705204771b6a78e805ee29cba26.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/94f13affa6f3b5126e172fdc6062be2e.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/10fef2083d54144639f0b6cd94778cb5.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/52fdcb4ddd856ebb4464834c99aebae0.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/76a1b1317f2520ef9a599a12e344730d.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/786eb6ddc8b4a1c15c3182f42e302b10.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/c47ae970e7baa8aa14a744f568b77922.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/cache/d3570f7a7a9be38c8599ac1773a618a2.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/08ff774ac6a70674d784cefe233dc1ab.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/82750bb2b6c7b7cda9f4f22eea23f1ef.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e6bfe72a35736c49013701f4e6cc2d7c.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/152adf213328a70d06d3041ea7eca814.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/cdfaa1f77a537214fe4d4d473da0c93f.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/dbca0c75b09289a0939a4568bccb8ffe.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/e3abd032ee5753e542d0c3d7701189e4.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.0.session/cache/ce56b654edab77f40b10056e97cc5df5.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/2de8075c9ff8cf4d4f231608bed835a9.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/91244a7f80eb57f7181e1278e1172cc9.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a59cc9b3f7f8b4a6624a1d1232662c22.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a93f056d32a8ace3dd916b64068f94c2.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/aafe330c4b6932bf122ff6509f3fc2b0.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/0d14213263b1d1def509095c28e95ea9.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/5c04a7d9d73560b7116ff3914824c36d.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/7cf5fa10093d1ce2fd3940954cba0727.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/857d1f9981d68d1406859c8aae1b4639.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/9ad7d025e7eb0eec65fb3551668328c9.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0ee6d92adc52cf841d8f421ae8b9d2f2.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0f47526247a0528c7b0b8c8e945b32bd.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3220ff8d08680b2082f90cfbabe5515c.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3c1da17d2eb3aa57d9920fdbb8fdc9ff.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/f6d37791a1137bc07941a661f2333b7e.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0748144945def11ea300e135d8482e4a.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0b916424d61743046a3a8aa2d1980ca0.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0f63fa83c61794d80fd003f133e182a7.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1784d421c70ac778d245b285417fda0f.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1fe4ca1fb351003ccbd8755355135f8a.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/21a3de19df739b18752521529d786b4b.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/25def53021ebb0a8629e796358a6848b.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/27bf4adc6f09a58eafeabec80e08e561.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2ad8e6939da759ba7083da389f70b19a.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2b04374aa95473cfa45c6abca5d0fe15.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2de5619cd6bf8a4549f18cbf2daefbba.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3b096d1ad2f60d27d68c9819789fceb4.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3d5c736c9ebc4a910745c54e3f810000.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4524f3b1a3aaeae1f14f29cffc5532b4.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/45fc8639c2e8c14a8ba57fe664c24c9d.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4833c149c493290f7476cb694c326889.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/51225dc69fc56402c586cbf2cad99281.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5998e90eb1b10fc1fd4ff54e6ef5689e.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d20435c0b8e9bb4e51ab262b3129648.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d3f4ea5bf6dc3f773faf7e0d63f1c76.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/6e15ce103fe14e50af7e0936d1d2a924.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/75158755074596f3fba764a01a862cea.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/77066c103c80ea4e5f9b5605057d8d03.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/78c65afc8eeed0925d1f9c68b047f97a.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/7e81584b97fe9a89bed8cd913741db47.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/805d516e173e9a1980e332963ed26853.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/85bd4f374f9098d4767c14833e05b5b8.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/904dfd55419e9da26d6710c5e3bb2512.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/93d52e79f66a5fbbf8a8d577d910215e.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/9e3b12919ddd0b7f3deeaa63da75f6e5.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a82a6af66093c860d0011d4f227136d1.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a8e0d95eaca351657706fd30bd03bea1.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a9311c935f353c4d4cea656ea0ab8a1e.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ad64f1c1643c7dd2550c00a9074f69.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ddcd489f338024c524107b6e504a00.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/bfe86eb3dc31cfbaa90471047107b2d3.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/c89d9d7df15c1516409d246b82b8c1f0.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/cf7eaa96c53ed9bc0ce7eef2ff6d4785.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/d73fc9500445fd11b1277eb233677128.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/dfb4426937ac0dd3319b8d97b1113ef1.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e3c7c32c0e592dcd434f4f389ed60f36.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e90a80dc6573ff3be6973ff12e676e32.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/ef4bb98ab16552a98c74ec0913047b5d.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f6abbe317c0d2a1424b05d2fb7e4bd9b.json
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f9262c0413f25f71d0ae44d4744746f0.json
create mode 100644 src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/1097cb045925dc7690981f0f528ee5d4.json
create mode 100644 src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/d89912a1e879d06f335b8d985cb804f3.json
create mode 100644 src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/de777917ace9bbef5272bb764ddd82c2.json
create mode 100644 src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json
create mode 100644 src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/89c62021b110300d0866feac14bd7c45.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/b602aeb805673b0805c79216c3ced563.json
create mode 100644 src/plugins/wp/tests/wp_store/oracle_qualif/struct.0.session/cache/8d2cbdde2b0c4740b0467e8f84939e0d.json
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index 8df080b73db..f318abf289f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
@@ -31,19 +31,20 @@ Let a_20 = a_9[shift_sint32(i32_0, i)].
Let a_21 = a_11[shift_uint32(u32_0, i)].
Let a_22 = a_13[shift_sint64(i64_0, i)].
Assume {
- Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_3) /\
- is_sint64_chunk(Mint_5) /\ is_sint8_chunk(Mchar_0) /\
- is_uint16_chunk(Mint_2) /\ is_uint32_chunk(Mint_4) /\
- is_uint64_chunk(Mint_6) /\ is_uint8_chunk(Mint_0) /\ is_sint32(i_1) /\
- is_sint16_chunk(a_5) /\ is_sint32_chunk(a_9) /\
- is_sint64_chunk(a_13) /\ is_sint8_chunk(a_1) /\ is_uint16_chunk(a_7) /\
- is_uint32_chunk(a_11) /\ is_uint64_chunk(a_15) /\ is_uint8_chunk(a_3).
+ Type: IsArray1_sint8(x) /\ is_sint16_chunk(Mint_1) /\
+ is_sint32_chunk(Mint_3) /\ is_sint64_chunk(Mint_5) /\
+ is_sint8_chunk(Mchar_0) /\ is_uint16_chunk(Mint_2) /\
+ is_uint32_chunk(Mint_4) /\ is_uint64_chunk(Mint_6) /\
+ is_uint8_chunk(Mint_0) /\ is_sint32(i_1) /\ is_sint16_chunk(a_5) /\
+ is_sint32_chunk(a_9) /\ is_sint64_chunk(a_13) /\ is_sint8_chunk(a_1) /\
+ is_uint16_chunk(a_7) /\ is_uint32_chunk(a_11) /\
+ is_uint64_chunk(a_15) /\ is_uint8_chunk(a_3).
(* Heap *)
Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
(region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
(region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
(region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
- IsArray1_sint8(x) /\ linked(Malloc_0) /\ sconst(Mchar_0).
+ linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: (0 <= i) /\ (i <= 9).
(* Initializer *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index 2e93da0b17e..0a7a16a6aca 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -216,16 +216,17 @@ end
(* use frama_c_wp.memory.Memory *)
- (* use Chunk *)
-
(* use S1_X *)
+ (* use Chunk *)
+
(* use Compound *)
goal wp_goal :
forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
- addr -> int, a:addr.
+ addr -> int, a:addr, x:S1_X.
region (base a) <= 0 ->
+ IsS1_X x ->
is_sint16_chunk t3 ->
is_sint32_chunk t4 ->
is_sint8_chunk t2 ->
@@ -240,15 +241,15 @@ end
Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 15):
Assume {
- Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0) /\
IsS1_X(Load_S1_X(p, Mchar_0, Mint_0, Mint_1)).
(* Heap *)
Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0) /\
cinits(Init_0).
- Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
- Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
(* Block In *)
Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
@@ -261,16 +262,16 @@ Prove: valid_rd(Malloc_0, p, 3).
Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 16):
Let a = Load_S1_X(p, Mchar_0, Mint_0, Mint_1).
Assume {
- Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0) /\ IsS1_X(a).
(* Heap *)
Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0) /\
cinits(Init_0).
- Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
- Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
- Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
(* Block In *)
Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/04c1fcb3dde99404e56f398c9d3c7b31.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/04c1fcb3dde99404e56f398c9d3c7b31.json
new file mode 100644
index 00000000000..bf03e943986
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/04c1fcb3dde99404e56f398c9d3c7b31.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1563,
+ "steps": 286 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/09419c3fbb6dc84c7ea4daf3841c155f.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/09419c3fbb6dc84c7ea4daf3841c155f.json
new file mode 100644
index 00000000000..15c20e5cfc0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/09419c3fbb6dc84c7ea4daf3841c155f.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0323,
+ "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/0af3d5135623c7629e8792c15c73e11e.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/0af3d5135623c7629e8792c15c73e11e.json
new file mode 100644
index 00000000000..15c20e5cfc0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/0af3d5135623c7629e8792c15c73e11e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0323,
+ "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/1d2ed0d831c17546d006475b478b59c1.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/1d2ed0d831c17546d006475b478b59c1.json
new file mode 100644
index 00000000000..79dc4338f21
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/1d2ed0d831c17546d006475b478b59c1.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0322,
+ "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/281d06f1268fc1f6bae73c9b23a370f6.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/281d06f1268fc1f6bae73c9b23a370f6.json
new file mode 100644
index 00000000000..2172e49206c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/281d06f1268fc1f6bae73c9b23a370f6.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0337,
+ "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/35644610983981a71b83b5427a68f6c0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/35644610983981a71b83b5427a68f6c0.json
new file mode 100644
index 00000000000..d226fb9296c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/35644610983981a71b83b5427a68f6c0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0377,
+ "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/6367c7d1e56f1af80ad76d813e09b66a.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/6367c7d1e56f1af80ad76d813e09b66a.json
new file mode 100644
index 00000000000..1cb9dc92527
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/6367c7d1e56f1af80ad76d813e09b66a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.138,
+ "steps": 269 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/675a842c7ec32528e5e21888634a1279.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/675a842c7ec32528e5e21888634a1279.json
new file mode 100644
index 00000000000..d05c7f00bb2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/675a842c7ec32528e5e21888634a1279.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0463,
+ "steps": 123 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/7ea33aa4c8dc9c1ed12a312a5a7b96ed.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/7ea33aa4c8dc9c1ed12a312a5a7b96ed.json
new file mode 100644
index 00000000000..fbd18991a8f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/7ea33aa4c8dc9c1ed12a312a5a7b96ed.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1203,
+ "steps": 252 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/a76226839c540aad032cd3b9de095b89.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/a76226839c540aad032cd3b9de095b89.json
new file mode 100644
index 00000000000..9749d24da27
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/a76226839c540aad032cd3b9de095b89.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1085,
+ "steps": 235 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/bd67f73e3ff115a9f45b4244c20611fe.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/bd67f73e3ff115a9f45b4244c20611fe.json
new file mode 100644
index 00000000000..9a8316dd72e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/bd67f73e3ff115a9f45b4244c20611fe.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0154,
+ "steps": 64 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e046513e2f30f1a1946d5d6e40ef9129.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e046513e2f30f1a1946d5d6e40ef9129.json
new file mode 100644
index 00000000000..cf65d980e11
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e046513e2f30f1a1946d5d6e40ef9129.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0847,
+ "steps": 184 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e434135b1fa122e6a232e26709df80a5.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e434135b1fa122e6a232e26709df80a5.json
new file mode 100644
index 00000000000..143a1e69e0b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e434135b1fa122e6a232e26709df80a5.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0129,
+ "steps": 62 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e8e066b606c41e89f82b2aa3eef46a68.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e8e066b606c41e89f82b2aa3eef46a68.json
new file mode 100644
index 00000000000..b2a493adaa4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e8e066b606c41e89f82b2aa3eef46a68.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0853,
+ "steps": 201 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e9c784c595bc40819eff858fbcc12bab.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e9c784c595bc40819eff858fbcc12bab.json
new file mode 100644
index 00000000000..ef833bf2578
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e9c784c595bc40819eff858fbcc12bab.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0314,
+ "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/efda69b6f9003dcb53f99c442ec8c4de.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/efda69b6f9003dcb53f99c442ec8c4de.json
new file mode 100644
index 00000000000..72229c47d0f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/efda69b6f9003dcb53f99c442ec8c4de.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0722,
+ "steps": 167 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f6b163a1cc48d21b279ce315660ffd85.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f6b163a1cc48d21b279ce315660ffd85.json
new file mode 100644
index 00000000000..ac1b7fec88f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f6b163a1cc48d21b279ce315660ffd85.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0881,
+ "steps": 218 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f97c74763d0222ed9be7c3fa666ce4e9.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f97c74763d0222ed9be7c3fa666ce4e9.json
new file mode 100644
index 00000000000..d3cae1db457
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f97c74763d0222ed9be7c3fa666ce4e9.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0487,
+ "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/feca65e917b9c99c3286ceebc5a4d618.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/feca65e917b9c99c3286ceebc5a4d618.json
new file mode 100644
index 00000000000..ac5ca13418a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/feca65e917b9c99c3286ceebc5a4d618.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0324,
+ "steps": 171 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/23316fd95fd7b645f6e7ee1ac0ec11dd.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/23316fd95fd7b645f6e7ee1ac0ec11dd.json
new file mode 100644
index 00000000000..ca8a4ddf594
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/23316fd95fd7b645f6e7ee1ac0ec11dd.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0096,
+ "steps": 17 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/af1c6e5e9ad0ce51ef02350de25db7b1.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/af1c6e5e9ad0ce51ef02350de25db7b1.json
new file mode 100644
index 00000000000..b8e36e2803f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/af1c6e5e9ad0ce51ef02350de25db7b1.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/e7547aa0621803b4e7d628af9dae8742.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/e7547aa0621803b4e7d628af9dae8742.json
new file mode 100644
index 00000000000..b4eff8a25e7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.0.session/cache/e7547aa0621803b4e7d628af9dae8742.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0148,
+ "steps": 21 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/0aaa8433bdd863a175c8f7aa27b5b23b.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/0aaa8433bdd863a175c8f7aa27b5b23b.json
new file mode 100644
index 00000000000..e4c3de15c1a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/0aaa8433bdd863a175c8f7aa27b5b23b.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 1. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/1235102376d88a3bdb52f3e4e1c49883.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/1235102376d88a3bdb52f3e4e1c49883.json
new file mode 100644
index 00000000000..5a95e44801c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/1235102376d88a3bdb52f3e4e1c49883.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0079,
+ "steps": 10 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/55cf143d013d4eb3345feb58b26b90df.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/55cf143d013d4eb3345feb58b26b90df.json
new file mode 100644
index 00000000000..741d4bc44f1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/55cf143d013d4eb3345feb58b26b90df.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0082,
+ "steps": 10 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/6203cf6d36b297213c87a78442bb23a3.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/6203cf6d36b297213c87a78442bb23a3.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/6203cf6d36b297213c87a78442bb23a3.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/7d35e079640e61a3109774eff9ba7fe6.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/7d35e079640e61a3109774eff9ba7fe6.json
new file mode 100644
index 00000000000..e4c3de15c1a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/7d35e079640e61a3109774eff9ba7fe6.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 1. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/bd22ac48c200239c37396cb5c074a071.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/bd22ac48c200239c37396cb5c074a071.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/bd22ac48c200239c37396cb5c074a071.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/d3883c78b48ca2e9439df35f88b59d8c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/d3883c78b48ca2e9439df35f88b59d8c.json
new file mode 100644
index 00000000000..e4c3de15c1a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/d3883c78b48ca2e9439df35f88b59d8c.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 1. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/da21dd780a181597dd44b362df8f5670.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/da21dd780a181597dd44b362df8f5670.json
new file mode 100644
index 00000000000..e4c3de15c1a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.0.session/cache/da21dd780a181597dd44b362df8f5670.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 1. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.0.session/cache/320f90061a8c50bf116b388e086c7897.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.0.session/cache/320f90061a8c50bf116b388e086c7897.json
new file mode 100644
index 00000000000..066974fb605
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.0.session/cache/320f90061a8c50bf116b388e086c7897.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0131,
+ "steps": 35 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/28c1570cd2d3e97ddd579e328c469acf.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/28c1570cd2d3e97ddd579e328c469acf.json
new file mode 100644
index 00000000000..b8e36e2803f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/28c1570cd2d3e97ddd579e328c469acf.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/5bfdad2f5b18af371b905b94799e1cc0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/5bfdad2f5b18af371b905b94799e1cc0.json
new file mode 100644
index 00000000000..2eb44ba21a5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/5bfdad2f5b18af371b905b94799e1cc0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0095,
+ "steps": 52 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/7ac4f3e9696602b90e6fd7dbef86293c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/7ac4f3e9696602b90e6fd7dbef86293c.json
new file mode 100644
index 00000000000..c9b1db9c4af
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/7ac4f3e9696602b90e6fd7dbef86293c.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0181,
+ "steps": 45 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/c520b8395718f1f484266fd4e5983d1e.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/c520b8395718f1f484266fd4e5983d1e.json
new file mode 100644
index 00000000000..a197c97ceb4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.session/cache/c520b8395718f1f484266fd4e5983d1e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.013,
+ "steps": 25 }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/647e4705204771b6a78e805ee29cba26.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/647e4705204771b6a78e805ee29cba26.json
new file mode 100644
index 00000000000..b8e36e2803f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/647e4705204771b6a78e805ee29cba26.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/94f13affa6f3b5126e172fdc6062be2e.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/94f13affa6f3b5126e172fdc6062be2e.json
new file mode 100644
index 00000000000..c9419cd7789
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.0.session/cache/94f13affa6f3b5126e172fdc6062be2e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0115,
+ "steps": 17 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/10fef2083d54144639f0b6cd94778cb5.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/10fef2083d54144639f0b6cd94778cb5.json
new file mode 100644
index 00000000000..12b29ad9f00
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/10fef2083d54144639f0b6cd94778cb5.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0189,
+ "steps": 67 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/52fdcb4ddd856ebb4464834c99aebae0.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/52fdcb4ddd856ebb4464834c99aebae0.json
new file mode 100644
index 00000000000..c438ee106b5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/52fdcb4ddd856ebb4464834c99aebae0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0118,
+ "steps": 25 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/76a1b1317f2520ef9a599a12e344730d.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/76a1b1317f2520ef9a599a12e344730d.json
new file mode 100644
index 00000000000..83bedfff027
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/76a1b1317f2520ef9a599a12e344730d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0123,
+ "steps": 27 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/786eb6ddc8b4a1c15c3182f42e302b10.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/786eb6ddc8b4a1c15c3182f42e302b10.json
new file mode 100644
index 00000000000..2de817ca705
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/786eb6ddc8b4a1c15c3182f42e302b10.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0517,
+ "steps": 92 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/c47ae970e7baa8aa14a744f568b77922.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/c47ae970e7baa8aa14a744f568b77922.json
new file mode 100644
index 00000000000..f5eb47507d0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.session/cache/c47ae970e7baa8aa14a744f568b77922.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0131,
+ "steps": 29 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/cache/d3570f7a7a9be38c8599ac1773a618a2.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/cache/d3570f7a7a9be38c8599ac1773a618a2.json
new file mode 100644
index 00000000000..3291e8fc3f1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/cache/d3570f7a7a9be38c8599ac1773a618a2.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0105,
+ "steps": 16 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/08ff774ac6a70674d784cefe233dc1ab.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/08ff774ac6a70674d784cefe233dc1ab.json
new file mode 100644
index 00000000000..7416efea8d9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/08ff774ac6a70674d784cefe233dc1ab.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0254,
+ "steps": 55 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/82750bb2b6c7b7cda9f4f22eea23f1ef.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/82750bb2b6c7b7cda9f4f22eea23f1ef.json
new file mode 100644
index 00000000000..b27f2eee4a7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/82750bb2b6c7b7cda9f4f22eea23f1ef.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0336,
+ "steps": 178 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e6bfe72a35736c49013701f4e6cc2d7c.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e6bfe72a35736c49013701f4e6cc2d7c.json
new file mode 100644
index 00000000000..f2ba5b4ebae
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/e6bfe72a35736c49013701f4e6cc2d7c.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0137,
+ "steps": 48 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/152adf213328a70d06d3041ea7eca814.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/152adf213328a70d06d3041ea7eca814.json
new file mode 100644
index 00000000000..ebb299a05a8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/152adf213328a70d06d3041ea7eca814.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.02, "steps": 54 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/cdfaa1f77a537214fe4d4d473da0c93f.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/cdfaa1f77a537214fe4d4d473da0c93f.json
new file mode 100644
index 00000000000..7cb83418252
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/cdfaa1f77a537214fe4d4d473da0c93f.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0174,
+ "steps": 54 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/dbca0c75b09289a0939a4568bccb8ffe.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/dbca0c75b09289a0939a4568bccb8ffe.json
new file mode 100644
index 00000000000..c16c4630985
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/dbca0c75b09289a0939a4568bccb8ffe.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0159,
+ "steps": 53 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/e3abd032ee5753e542d0c3d7701189e4.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/e3abd032ee5753e542d0c3d7701189e4.json
new file mode 100644
index 00000000000..084b990db48
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.session/cache/e3abd032ee5753e542d0c3d7701189e4.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0102,
+ "steps": 27 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.0.session/cache/ce56b654edab77f40b10056e97cc5df5.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.0.session/cache/ce56b654edab77f40b10056e97cc5df5.json
new file mode 100644
index 00000000000..b92d9fe95b4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.0.session/cache/ce56b654edab77f40b10056e97cc5df5.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0205,
+ "steps": 62 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/2de8075c9ff8cf4d4f231608bed835a9.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/2de8075c9ff8cf4d4f231608bed835a9.json
new file mode 100644
index 00000000000..a5593ead662
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/2de8075c9ff8cf4d4f231608bed835a9.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0297,
+ "steps": 130 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/91244a7f80eb57f7181e1278e1172cc9.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/91244a7f80eb57f7181e1278e1172cc9.json
new file mode 100644
index 00000000000..3fcfc93ffdf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/91244a7f80eb57f7181e1278e1172cc9.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.035,
+ "steps": 132 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a59cc9b3f7f8b4a6624a1d1232662c22.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a59cc9b3f7f8b4a6624a1d1232662c22.json
new file mode 100644
index 00000000000..78e22d71472
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a59cc9b3f7f8b4a6624a1d1232662c22.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0285,
+ "steps": 130 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a93f056d32a8ace3dd916b64068f94c2.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a93f056d32a8ace3dd916b64068f94c2.json
new file mode 100644
index 00000000000..ff7646a74d0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/a93f056d32a8ace3dd916b64068f94c2.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0113,
+ "steps": 23 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/aafe330c4b6932bf122ff6509f3fc2b0.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/aafe330c4b6932bf122ff6509f3fc2b0.json
new file mode 100644
index 00000000000..c4ef5983902
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.session/cache/aafe330c4b6932bf122ff6509f3fc2b0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0091,
+ "steps": 39 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/0d14213263b1d1def509095c28e95ea9.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/0d14213263b1d1def509095c28e95ea9.json
new file mode 100644
index 00000000000..e1e5a02eec2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/0d14213263b1d1def509095c28e95ea9.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0198,
+ "steps": 73 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/5c04a7d9d73560b7116ff3914824c36d.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/5c04a7d9d73560b7116ff3914824c36d.json
new file mode 100644
index 00000000000..e523147de74
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/5c04a7d9d73560b7116ff3914824c36d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0124,
+ "steps": 32 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/7cf5fa10093d1ce2fd3940954cba0727.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/7cf5fa10093d1ce2fd3940954cba0727.json
new file mode 100644
index 00000000000..1dd11313ae1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/7cf5fa10093d1ce2fd3940954cba0727.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0235,
+ "steps": 73 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/857d1f9981d68d1406859c8aae1b4639.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/857d1f9981d68d1406859c8aae1b4639.json
new file mode 100644
index 00000000000..fdfc488fd36
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/857d1f9981d68d1406859c8aae1b4639.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0164,
+ "steps": 45 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/9ad7d025e7eb0eec65fb3551668328c9.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/9ad7d025e7eb0eec65fb3551668328c9.json
new file mode 100644
index 00000000000..67801b1ad0c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.session/cache/9ad7d025e7eb0eec65fb3551668328c9.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0196,
+ "steps": 71 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0ee6d92adc52cf841d8f421ae8b9d2f2.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0ee6d92adc52cf841d8f421ae8b9d2f2.json
new file mode 100644
index 00000000000..4346351e328
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0ee6d92adc52cf841d8f421ae8b9d2f2.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0171,
+ "steps": 53 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0f47526247a0528c7b0b8c8e945b32bd.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0f47526247a0528c7b0b8c8e945b32bd.json
new file mode 100644
index 00000000000..69c84a26f33
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/0f47526247a0528c7b0b8c8e945b32bd.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0095,
+ "steps": 19 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3220ff8d08680b2082f90cfbabe5515c.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3220ff8d08680b2082f90cfbabe5515c.json
new file mode 100644
index 00000000000..635370d75fb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3220ff8d08680b2082f90cfbabe5515c.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.016,
+ "steps": 51 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3c1da17d2eb3aa57d9920fdbb8fdc9ff.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3c1da17d2eb3aa57d9920fdbb8fdc9ff.json
new file mode 100644
index 00000000000..2a821f8d129
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/3c1da17d2eb3aa57d9920fdbb8fdc9ff.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.015,
+ "steps": 53 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/f6d37791a1137bc07941a661f2333b7e.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/f6d37791a1137bc07941a661f2333b7e.json
new file mode 100644
index 00000000000..71a57ad70b2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.session/cache/f6d37791a1137bc07941a661f2333b7e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0078,
+ "steps": 50 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0748144945def11ea300e135d8482e4a.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0748144945def11ea300e135d8482e4a.json
new file mode 100644
index 00000000000..5033fa63b66
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0748144945def11ea300e135d8482e4a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0459,
+ "steps": 121 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0b916424d61743046a3a8aa2d1980ca0.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0b916424d61743046a3a8aa2d1980ca0.json
new file mode 100644
index 00000000000..4b76bff9c5a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0b916424d61743046a3a8aa2d1980ca0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0143,
+ "steps": 61 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0f63fa83c61794d80fd003f133e182a7.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0f63fa83c61794d80fd003f133e182a7.json
new file mode 100644
index 00000000000..2ee4c477e8a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/0f63fa83c61794d80fd003f133e182a7.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.112,
+ "steps": 224 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1784d421c70ac778d245b285417fda0f.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1784d421c70ac778d245b285417fda0f.json
new file mode 100644
index 00000000000..826c52aacf7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1784d421c70ac778d245b285417fda0f.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0201,
+ "steps": 76 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1fe4ca1fb351003ccbd8755355135f8a.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1fe4ca1fb351003ccbd8755355135f8a.json
new file mode 100644
index 00000000000..137bfc045d3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/1fe4ca1fb351003ccbd8755355135f8a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1581,
+ "steps": 251 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/21a3de19df739b18752521529d786b4b.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/21a3de19df739b18752521529d786b4b.json
new file mode 100644
index 00000000000..7881c7c9a45
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/21a3de19df739b18752521529d786b4b.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0427,
+ "steps": 101 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/25def53021ebb0a8629e796358a6848b.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/25def53021ebb0a8629e796358a6848b.json
new file mode 100644
index 00000000000..93a6c31f0ca
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/25def53021ebb0a8629e796358a6848b.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.027,
+ "steps": 66 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/27bf4adc6f09a58eafeabec80e08e561.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/27bf4adc6f09a58eafeabec80e08e561.json
new file mode 100644
index 00000000000..5970963a22a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/27bf4adc6f09a58eafeabec80e08e561.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 1.448,
+ "steps": 874 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2ad8e6939da759ba7083da389f70b19a.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2ad8e6939da759ba7083da389f70b19a.json
new file mode 100644
index 00000000000..7bf27258b66
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2ad8e6939da759ba7083da389f70b19a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.008,
+ "steps": 18 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2b04374aa95473cfa45c6abca5d0fe15.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2b04374aa95473cfa45c6abca5d0fe15.json
new file mode 100644
index 00000000000..1c231cee37e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2b04374aa95473cfa45c6abca5d0fe15.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0123,
+ "steps": 35 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2de5619cd6bf8a4549f18cbf2daefbba.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2de5619cd6bf8a4549f18cbf2daefbba.json
new file mode 100644
index 00000000000..e03b006e36d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/2de5619cd6bf8a4549f18cbf2daefbba.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0114,
+ "steps": 29 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3b096d1ad2f60d27d68c9819789fceb4.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3b096d1ad2f60d27d68c9819789fceb4.json
new file mode 100644
index 00000000000..7cbb165d065
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3b096d1ad2f60d27d68c9819789fceb4.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0677,
+ "steps": 169 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3d5c736c9ebc4a910745c54e3f810000.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3d5c736c9ebc4a910745c54e3f810000.json
new file mode 100644
index 00000000000..ca5bb4ea160
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/3d5c736c9ebc4a910745c54e3f810000.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1562,
+ "steps": 267 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4524f3b1a3aaeae1f14f29cffc5532b4.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4524f3b1a3aaeae1f14f29cffc5532b4.json
new file mode 100644
index 00000000000..e667529e5ba
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4524f3b1a3aaeae1f14f29cffc5532b4.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0207,
+ "steps": 82 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/45fc8639c2e8c14a8ba57fe664c24c9d.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/45fc8639c2e8c14a8ba57fe664c24c9d.json
new file mode 100644
index 00000000000..34cbd0294af
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/45fc8639c2e8c14a8ba57fe664c24c9d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0471,
+ "steps": 107 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4833c149c493290f7476cb694c326889.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4833c149c493290f7476cb694c326889.json
new file mode 100644
index 00000000000..c85fd94e357
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/4833c149c493290f7476cb694c326889.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0372,
+ "steps": 61 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/51225dc69fc56402c586cbf2cad99281.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/51225dc69fc56402c586cbf2cad99281.json
new file mode 100644
index 00000000000..b6d8db7b016
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/51225dc69fc56402c586cbf2cad99281.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0262,
+ "steps": 76 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5998e90eb1b10fc1fd4ff54e6ef5689e.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5998e90eb1b10fc1fd4ff54e6ef5689e.json
new file mode 100644
index 00000000000..df8ca8fe1a0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5998e90eb1b10fc1fd4ff54e6ef5689e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0977,
+ "steps": 179 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d20435c0b8e9bb4e51ab262b3129648.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d20435c0b8e9bb4e51ab262b3129648.json
new file mode 100644
index 00000000000..827ebad8def
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d20435c0b8e9bb4e51ab262b3129648.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.2324,
+ "steps": 210 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d3f4ea5bf6dc3f773faf7e0d63f1c76.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d3f4ea5bf6dc3f773faf7e0d63f1c76.json
new file mode 100644
index 00000000000..83e0ba8ee6f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/5d3f4ea5bf6dc3f773faf7e0d63f1c76.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0397,
+ "steps": 111 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/6e15ce103fe14e50af7e0936d1d2a924.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/6e15ce103fe14e50af7e0936d1d2a924.json
new file mode 100644
index 00000000000..b1fe562c2f1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/6e15ce103fe14e50af7e0936d1d2a924.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.02, "steps": 64 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/75158755074596f3fba764a01a862cea.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/75158755074596f3fba764a01a862cea.json
new file mode 100644
index 00000000000..32f9c5fdfe9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/75158755074596f3fba764a01a862cea.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0193,
+ "steps": 66 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/77066c103c80ea4e5f9b5605057d8d03.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/77066c103c80ea4e5f9b5605057d8d03.json
new file mode 100644
index 00000000000..60dab5b5ec2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/77066c103c80ea4e5f9b5605057d8d03.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0612,
+ "steps": 151 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/78c65afc8eeed0925d1f9c68b047f97a.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/78c65afc8eeed0925d1f9c68b047f97a.json
new file mode 100644
index 00000000000..6a103d99cdb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/78c65afc8eeed0925d1f9c68b047f97a.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0156,
+ "steps": 76 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/7e81584b97fe9a89bed8cd913741db47.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/7e81584b97fe9a89bed8cd913741db47.json
new file mode 100644
index 00000000000..83debd7e69e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/7e81584b97fe9a89bed8cd913741db47.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0206,
+ "steps": 76 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/805d516e173e9a1980e332963ed26853.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/805d516e173e9a1980e332963ed26853.json
new file mode 100644
index 00000000000..6e36003ddf4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/805d516e173e9a1980e332963ed26853.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0095,
+ "steps": 21 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/85bd4f374f9098d4767c14833e05b5b8.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/85bd4f374f9098d4767c14833e05b5b8.json
new file mode 100644
index 00000000000..a00184de1fd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/85bd4f374f9098d4767c14833e05b5b8.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0574,
+ "steps": 117 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/904dfd55419e9da26d6710c5e3bb2512.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/904dfd55419e9da26d6710c5e3bb2512.json
new file mode 100644
index 00000000000..9f1ee7872b4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/904dfd55419e9da26d6710c5e3bb2512.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0287,
+ "steps": 93 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/93d52e79f66a5fbbf8a8d577d910215e.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/93d52e79f66a5fbbf8a8d577d910215e.json
new file mode 100644
index 00000000000..e9844a57cba
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/93d52e79f66a5fbbf8a8d577d910215e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0898,
+ "steps": 195 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/9e3b12919ddd0b7f3deeaa63da75f6e5.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/9e3b12919ddd0b7f3deeaa63da75f6e5.json
new file mode 100644
index 00000000000..398e1b3eb88
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/9e3b12919ddd0b7f3deeaa63da75f6e5.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0332,
+ "steps": 95 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a82a6af66093c860d0011d4f227136d1.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a82a6af66093c860d0011d4f227136d1.json
new file mode 100644
index 00000000000..f105ad10719
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a82a6af66093c860d0011d4f227136d1.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.021,
+ "steps": 64 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a8e0d95eaca351657706fd30bd03bea1.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a8e0d95eaca351657706fd30bd03bea1.json
new file mode 100644
index 00000000000..2d135b93226
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a8e0d95eaca351657706fd30bd03bea1.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.008,
+ "steps": 19 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a9311c935f353c4d4cea656ea0ab8a1e.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a9311c935f353c4d4cea656ea0ab8a1e.json
new file mode 100644
index 00000000000..2471b919ea1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/a9311c935f353c4d4cea656ea0ab8a1e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0233,
+ "steps": 81 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ad64f1c1643c7dd2550c00a9074f69.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ad64f1c1643c7dd2550c00a9074f69.json
new file mode 100644
index 00000000000..ee56722a84b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ad64f1c1643c7dd2550c00a9074f69.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0305,
+ "steps": 90 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ddcd489f338024c524107b6e504a00.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ddcd489f338024c524107b6e504a00.json
new file mode 100644
index 00000000000..ed311aa3bf7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/b2ddcd489f338024c524107b6e504a00.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0239,
+ "steps": 64 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/bfe86eb3dc31cfbaa90471047107b2d3.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/bfe86eb3dc31cfbaa90471047107b2d3.json
new file mode 100644
index 00000000000..19937fe629e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/bfe86eb3dc31cfbaa90471047107b2d3.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.7249,
+ "steps": 586 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/c89d9d7df15c1516409d246b82b8c1f0.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/c89d9d7df15c1516409d246b82b8c1f0.json
new file mode 100644
index 00000000000..e2adf732c23
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/c89d9d7df15c1516409d246b82b8c1f0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0076,
+ "steps": 24 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/cf7eaa96c53ed9bc0ce7eef2ff6d4785.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/cf7eaa96c53ed9bc0ce7eef2ff6d4785.json
new file mode 100644
index 00000000000..453f17235fb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/cf7eaa96c53ed9bc0ce7eef2ff6d4785.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0222,
+ "steps": 73 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/d73fc9500445fd11b1277eb233677128.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/d73fc9500445fd11b1277eb233677128.json
new file mode 100644
index 00000000000..7181b9f0008
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/d73fc9500445fd11b1277eb233677128.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0677,
+ "steps": 128 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/dfb4426937ac0dd3319b8d97b1113ef1.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/dfb4426937ac0dd3319b8d97b1113ef1.json
new file mode 100644
index 00000000000..4ce8c833c8d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/dfb4426937ac0dd3319b8d97b1113ef1.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0575,
+ "steps": 133 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e3c7c32c0e592dcd434f4f389ed60f36.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e3c7c32c0e592dcd434f4f389ed60f36.json
new file mode 100644
index 00000000000..985a0441350
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e3c7c32c0e592dcd434f4f389ed60f36.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1778,
+ "steps": 240 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e90a80dc6573ff3be6973ff12e676e32.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e90a80dc6573ff3be6973ff12e676e32.json
new file mode 100644
index 00000000000..5c8499dcc7e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/e90a80dc6573ff3be6973ff12e676e32.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0143,
+ "steps": 54 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/ef4bb98ab16552a98c74ec0913047b5d.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/ef4bb98ab16552a98c74ec0913047b5d.json
new file mode 100644
index 00000000000..b480d3f35b7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/ef4bb98ab16552a98c74ec0913047b5d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0856,
+ "steps": 138 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f6abbe317c0d2a1424b05d2fb7e4bd9b.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f6abbe317c0d2a1424b05d2fb7e4bd9b.json
new file mode 100644
index 00000000000..e3e8779cbd7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f6abbe317c0d2a1424b05d2fb7e4bd9b.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0534,
+ "steps": 114 }
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f9262c0413f25f71d0ae44d4744746f0.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f9262c0413f25f71d0ae44d4744746f0.json
new file mode 100644
index 00000000000..d2cb65a7b9e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/cache/f9262c0413f25f71d0ae44d4744746f0.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0333,
+ "steps": 92 }
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/1097cb045925dc7690981f0f528ee5d4.json b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/1097cb045925dc7690981f0f528ee5d4.json
new file mode 100644
index 00000000000..1a411f445d6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/1097cb045925dc7690981f0f528ee5d4.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.023,
+ "steps": 27 }
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/d89912a1e879d06f335b8d985cb804f3.json b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/d89912a1e879d06f335b8d985cb804f3.json
new file mode 100644
index 00000000000..7b78699ea74
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/d89912a1e879d06f335b8d985cb804f3.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0131,
+ "steps": 28 }
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/de777917ace9bbef5272bb764ddd82c2.json b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/de777917ace9bbef5272bb764ddd82c2.json
new file mode 100644
index 00000000000..2d31e4969e8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.0.session/cache/de777917ace9bbef5272bb764ddd82c2.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0121,
+ "steps": 28 }
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json
new file mode 100644
index 00000000000..428a1839b17
--- /dev/null
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0102,
+ "steps": 22 }
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json
new file mode 100644
index 00000000000..f6ac3dd3d95
--- /dev/null
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.session/cache/3016a12fe9f82a49a0ff618ae2acf170.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0118,
+ "steps": 22 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/89c62021b110300d0866feac14bd7c45.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/89c62021b110300d0866feac14bd7c45.json
new file mode 100644
index 00000000000..b8e36e2803f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/89c62021b110300d0866feac14bd7c45.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/b602aeb805673b0805c79216c3ced563.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/b602aeb805673b0805c79216c3ced563.json
new file mode 100644
index 00000000000..b8e36e2803f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.0.session/cache/b602aeb805673b0805c79216c3ced563.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.0.session/cache/8d2cbdde2b0c4740b0467e8f84939e0d.json b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.0.session/cache/8d2cbdde2b0c4740b0467e8f84939e0d.json
new file mode 100644
index 00000000000..d3dcde5a175
--- /dev/null
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.0.session/cache/8d2cbdde2b0c4740b0467e8f84939e0d.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0157,
+ "steps": 35 }
--
GitLab