diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in index 47549ee4316744b5cde028b18701b28aa8e33dcb..3d55dac46a5898c30486d59caa3756a590d3cc82 100644 --- a/src/plugins/wp/Makefile.in +++ b/src/plugins/wp/Makefile.in @@ -145,6 +145,10 @@ wp-qualif: ./bin/toplevel.opt ./bin/ptests.opt ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt + FRAMAC_WP_CACHE=update \ + ./bin/ptests.opt src/plugins/wp/tests -config qualif + +wp-qualif-upgrade: ./bin/toplevel.opt ./bin/ptests.opt FRAMAC_WP_CACHE=update \ FRAMAC_WP_SCRIPT=update \ ./bin/ptests.opt src/plugins/wp/tests -config qualif diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/266abf4c61d5d3612cc873cc2f658b4b.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/266abf4c61d5d3612cc873cc2f658b4b.json new file mode 100644 index 0000000000000000000000000000000000000000..3257442fbe484393c11fe772b0144d700e62be0a --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/266abf4c61d5d3612cc873cc2f658b4b.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.3682, + "steps": 535 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/f7fb102dfd74cd1e6bd6e09aae256cf0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/f7fb102dfd74cd1e6bd6e09aae256cf0.json new file mode 100644 index 0000000000000000000000000000000000000000..91ef5fe08ab0a866065d3e8625f7729d22bc0f0a --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/f7fb102dfd74cd1e6bd6e09aae256cf0.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1518, + "steps": 166 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/fd2458f07a6485f7076d5a78dc65e20c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/fd2458f07a6485f7076d5a78dc65e20c.json new file mode 100644 index 0000000000000000000000000000000000000000..638916aa4cc2ec4ad4c810e7df3ff07d00c10b84 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.session/cache/fd2458f07a6485f7076d5a78dc65e20c.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2975, + "steps": 533 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/1fe2eacd6d20f2162a4950128caf9f88.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/1fe2eacd6d20f2162a4950128caf9f88.json new file mode 100644 index 0000000000000000000000000000000000000000..c20a37b337d87214ca828be80ea66c0654129e1f --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/1fe2eacd6d20f2162a4950128caf9f88.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2665, + "steps": 536 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/4aed44fbe802edcf56fe979cb0bd1fd1.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/4aed44fbe802edcf56fe979cb0bd1fd1.json new file mode 100644 index 0000000000000000000000000000000000000000..61892a317bc62e4bab67c8924e17c340bca5da29 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/4aed44fbe802edcf56fe979cb0bd1fd1.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2204, + "steps": 567 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/756079eaf758e0a707efed015bec5bcd.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/756079eaf758e0a707efed015bec5bcd.json new file mode 100644 index 0000000000000000000000000000000000000000..82576daec3b239796971860a087e2247c1abdc54 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/756079eaf758e0a707efed015bec5bcd.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1849, + "steps": 172 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/820a9cf50a575d585badbf5e5fad83a0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/820a9cf50a575d585badbf5e5fad83a0.json new file mode 100644 index 0000000000000000000000000000000000000000..d97aaf8bcd3dfaffd021557bb5fe8d5655ab9fd7 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/820a9cf50a575d585badbf5e5fad83a0.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2162, + "steps": 539 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/875b3f59996d77e478fe981d539949d8.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/875b3f59996d77e478fe981d539949d8.json new file mode 100644 index 0000000000000000000000000000000000000000..196fb0c09e26a28855ec91923e36e12d54568a91 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/875b3f59996d77e478fe981d539949d8.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2094, + "steps": 557 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/91ab633347e34af327d794249d674722.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/91ab633347e34af327d794249d674722.json new file mode 100644 index 0000000000000000000000000000000000000000..7132886e0f0bf351cb29be1ac64e18809cad280e --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/91ab633347e34af327d794249d674722.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1185, + "steps": 172 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/96e9a571319248796e554e1be068f1be.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/96e9a571319248796e554e1be068f1be.json new file mode 100644 index 0000000000000000000000000000000000000000..355e0961e4d7dcabc2be053b86c8ad6953c87591 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/96e9a571319248796e554e1be068f1be.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2524, + "steps": 531 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b359768fc97ed1575e1a9ded31e7ed01.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b359768fc97ed1575e1a9ded31e7ed01.json new file mode 100644 index 0000000000000000000000000000000000000000..65cfdd122a303afa078d9be8a0903b608e8ff9a8 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b359768fc97ed1575e1a9ded31e7ed01.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1041, + "steps": 168 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b77d1b117413691fad797c4a48f3c372.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b77d1b117413691fad797c4a48f3c372.json new file mode 100644 index 0000000000000000000000000000000000000000..cfff7d15506a8c2c48c0f62988b486513d76aa6e --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/b77d1b117413691fad797c4a48f3c372.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.212, + "steps": 535 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e0e8f7dccfbbe2f7426617215706e998.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e0e8f7dccfbbe2f7426617215706e998.json new file mode 100644 index 0000000000000000000000000000000000000000..321e3eb3df3bbd8ea9be7b21b821c5a9ae2970b4 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e0e8f7dccfbbe2f7426617215706e998.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2572, + "steps": 543 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e494b53ac5e3154be1b7ff4d30fa7d19.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e494b53ac5e3154be1b7ff4d30fa7d19.json new file mode 100644 index 0000000000000000000000000000000000000000..70b6dd4b59f67cd5cba430c107df33ac6002742b --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/e494b53ac5e3154be1b7ff4d30fa7d19.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1663, + "steps": 172 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/ea44cea51e17f5beecd3c6e0bcaf6860.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/ea44cea51e17f5beecd3c6e0bcaf6860.json new file mode 100644 index 0000000000000000000000000000000000000000..6d53ae41f7bb89519dfc53139ab9be39dbd1bce3 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/ea44cea51e17f5beecd3c6e0bcaf6860.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2533, + "steps": 535 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f2e6496b5434869ba3461731001ad294.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f2e6496b5434869ba3461731001ad294.json new file mode 100644 index 0000000000000000000000000000000000000000..b5d00d2a037788f05702b8ec47c452bb2ee3eb32 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f2e6496b5434869ba3461731001ad294.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1092, + "steps": 172 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f7426a5e9d31ceb59b7fe847195704e8.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f7426a5e9d31ceb59b7fe847195704e8.json new file mode 100644 index 0000000000000000000000000000000000000000..b104977442f336d6b799a2a1f672712165364850 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.session/cache/f7426a5e9d31ceb59b7fe847195704e8.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.1496, + "steps": 172 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/034d72d9106e3380325aa1d67bc6e530.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/034d72d9106e3380325aa1d67bc6e530.json new file mode 100644 index 0000000000000000000000000000000000000000..0f49cd7ae20cebd6b9e18357cc5d0e5611ffa95d --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/034d72d9106e3380325aa1d67bc6e530.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2325, + "steps": 551 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/0c30085628a552390ece72f72470887c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/0c30085628a552390ece72f72470887c.json new file mode 100644 index 0000000000000000000000000000000000000000..d58edca46154b8c56712d6def5bb5e66812c2355 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/0c30085628a552390ece72f72470887c.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 1.0112, + "steps": 1546 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/45b3f3bcc0160bd4b82742281bb0a056.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/45b3f3bcc0160bd4b82742281bb0a056.json new file mode 100644 index 0000000000000000000000000000000000000000..92b1aa4a0b5761a53a63699d5c78151e01b23c18 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/45b3f3bcc0160bd4b82742281bb0a056.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2302, + "steps": 551 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/70562eac8dc02df9552e2f42b8fcfda0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/70562eac8dc02df9552e2f42b8fcfda0.json new file mode 100644 index 0000000000000000000000000000000000000000..fc9a077e63d7a225ecf3a9f0539b61f12c035d1b --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/70562eac8dc02df9552e2f42b8fcfda0.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2867, + "steps": 551 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/abb1bf9b1f3597182f3034fa7e127544.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/abb1bf9b1f3597182f3034fa7e127544.json new file mode 100644 index 0000000000000000000000000000000000000000..9fa2b35d47fb3580e589588b6e01d36fac5b0b46 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/abb1bf9b1f3597182f3034fa7e127544.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2475, + "steps": 551 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/bb473069cb6de4ddb4a17759af940d2f.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/bb473069cb6de4ddb4a17759af940d2f.json new file mode 100644 index 0000000000000000000000000000000000000000..8cf12f5ed4abd27761b6ec7dc4ac853c4897d06b --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/bb473069cb6de4ddb4a17759af940d2f.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2696, + "steps": 551 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f749942d7589b216b3eadf0150d9a3d4.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f749942d7589b216b3eadf0150d9a3d4.json new file mode 100644 index 0000000000000000000000000000000000000000..06bed841ac0720281421fa53fb038e70d9694fb4 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f749942d7589b216b3eadf0150d9a3d4.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.5142, + "steps": 1727 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f8d02d3f4932587b1ff1da126702b1ab.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f8d02d3f4932587b1ff1da126702b1ab.json new file mode 100644 index 0000000000000000000000000000000000000000..91c90a9142cd09f48c781c975f97a4c124bb493a --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/f8d02d3f4932587b1ff1da126702b1ab.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.2995, + "steps": 551 } diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.0.session/cache/b1a18aa2a86a77a0d31483dd0650660d.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.0.session/cache/b1a18aa2a86a77a0d31483dd0650660d.json new file mode 100644 index 0000000000000000000000000000000000000000..a6d1470d0c451f2e83c1d1ef32c71fad62db460a --- /dev/null +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.0.session/cache/b1a18aa2a86a77a0d31483dd0650660d.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.3396, + "steps": 558 } diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.session/cache/f3d86f6d80e0586d0adc5d348ad0441e.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.session/cache/f3d86f6d80e0586d0adc5d348ad0441e.json new file mode 100644 index 0000000000000000000000000000000000000000..f4fa6591e63fb21a78394b4386d440604198631e --- /dev/null +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.session/cache/f3d86f6d80e0586d0adc5d348ad0441e.json @@ -0,0 +1 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "stepout", "steps": 50 } diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.session/cache/eb64f61fbab15570bb76ae4d71d1de91.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.session/cache/eb64f61fbab15570bb76ae4d71d1de91.json new file mode 100644 index 0000000000000000000000000000000000000000..40c36c96271264cb81ce83e34c573c534b96a880 --- /dev/null +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.session/cache/eb64f61fbab15570bb76ae4d71d1de91.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "valid", "time": 0.0239, + "steps": 57 } diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.session/cache/a1d76edfd7bcf43834cdac624ff86d0a.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.session/cache/a1d76edfd7bcf43834cdac624ff86d0a.json new file mode 100644 index 0000000000000000000000000000000000000000..213923a36bfee9505e19afbd2c4624d7783b054d --- /dev/null +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.session/cache/a1d76edfd7bcf43834cdac624ff86d0a.json @@ -0,0 +1 @@ +{ "prover": "Alt-Ergo:2.3.0", "verdict": "timeout", "time": 10. }