diff --git a/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle index 1af0a4978ea76984ab04a079184ecaa68cc9f61c..29c9c66f579e875d06ee174d2c67109ac9dd0506 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp/sharing.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle index 13b5a090e324472be712d4732fd5b278e6d4cc62..ee7e3d8c42bb797918eae2acffced0f9b937cab3 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp/stmtcompiler_test.i (no preprocessing) [kernel] tests/wp/stmtcompiler_test.i:136: Warning: Body of function if_assert falls-through. Adding a return statement diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle index 23141b87e966b27e9d81d6feeec83fdabf24c317..2867ef1ce9fac2398e511c7b2daaddba89f5b162 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp/stmtcompiler_test_rela.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle index 8ef82489efb80a0b5a3bc45ed959a8781414c934..e7058249e0382a76ed77d2d61f82540675ecff40 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp [...] +# frama-c -wp -wp-timeout 1 [...] [kernel] Parsing tests/wp/wp_behav.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle index 5f62257e35df9f7486ce5e9014d03c72e861fe8c..3cd8c9dc87ef1fecab861c4a376920f4b9ef4b5a 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp/wp_behav.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle index da92bd060d15c52022f318aa3661baed6105fb70..ef2759505d0f467a32589a8044f365c13b5c479f 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle index f52504145b9fc163aaf39a9866281cefde1009d1..bdf16d02cb822648ab909aaf2cb644ae3a2b0bc7 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp/wp_eqb.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle index 38dfb47769eeb1b9d12d6e16f6ea3038caced551..e0fba0eeebb5307fb82cf55a12fd2c2e16573800 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Hoare' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Hoare' [...] [kernel] Parsing tests/wp/wp_strategy.c (with preprocessing) [rte] annotating function bts0513 [rte] annotating function bts0513_bis diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle index 181bf2a9fbc801af1b7c5c180d9c588ce3664f70..c423c72e13275ee12e1bdb02d896209543471042 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/arith.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle index 22512c43596e59f57a7705dd602bcb75262e4cf8..e6f6bea9c6837fbe4e1acf05de0816079a05e4d9 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/arith.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle index a532ef8d1cf5f449215c792de3edbfe8cdaa43c7..26d8e212c80f0473f2c48a77399cc126f5bef18f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assign_array.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle index 36a8e376b7408fea0f930f27b25d8136d8d71244..97318c56ec4ac5f12cc340cddbaff42b4b941a02 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assigns_path.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle index 64c7d444dc045b089f594634841e43b7f2788ba4..db587673eacdddb3440b7b8425edaf73d39783ea 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle index 64e97d8799e637cf957808bd06d8e7f3eeb7217d..740d097ec798cbd2d89caf8208b429bcce99090c 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle index 736e31a325f5fe26f4c6d63955528caff10fed60..a3493e036614f668d01b6b95a1002daeeadc1c45 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/axioms.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle index 1af5465d13154a5483b11d033f0559997d780615..0ce1be644f70ca422444f04aeaae79657bc9ef53 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/base_offset.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle index bcb6ca0c309bce06e75c6a2cb14755c8276fc028..23321ffd00c9408ab3d574a7d35bde27b552c618 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/bitwise.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle index 48fb4714a1f9e26815faeff51fb4f090a88f56f9..c76035e0829a7223ddc7e12af46569768e18b708 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/bitwise2.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle index cf0946ede61699d19535943cacdfac9b59bcd40f..e4be1fdb79ccfe9502fe242b015f23b500c1ce33 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/block_length.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle index bf4efdc83af91b0df0b941fec22ca0391dc3a19a..a6187ffba8d271b4d3bcf2909f86ea99967f9282 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 5 [...] +# frama-c -wp -wp-steps 5 [...] [kernel] Parsing tests/wp_acsl/checks.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle index c4b1a1c2873fa09e1c505ff9995670f712850a1c..cfee3c57e18aa4132b2f2988923bcc530e4e2961 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle index b9250d09987006efcb9071ccdfde0f38903b725c..1c0f3f3f388045d820787e6f640a6480a9742c5d 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle index 0162e0980a3e712138d309ac460ef90a84ee9ced..7ddef8f6c1163e7ec87114454f625be52a78fe2f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle index 6c52f44f79d5903f974c160d9c930c4d105cbcb0..96ac43f85256d5d1199e0cd7f65fc6b699e5e656 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/cnf.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle index 28838da6b6bf90e3686624a9eecf7e0745fea9f8..98b954ee53146f9cd5c34796c9663f6f5ee9292f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/ctor.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle index 129596332719e69acdb8b69587b890364126cd9c..fe8628eb6a8133631411fb58b3daf5d73348eb8d 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle index 92c78b1d82867cf7a86825f82d7416236d1e1fe9..3b1a448537a55b7456126c7507f6869579f89f91 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle index b0357286139124d289affbd8a1cfbb96cb586d17..90d4a24c060502e14ac081e29d432198699961a8 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/div_mod.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle index a8ae2141cef39017e807d4c8e8f0f805bfd447ec..8a4506b88c4a87d8e13a03c7e04048e9fa5b3b67 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/e_imply.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle index 33fc1d116f1788f68acc4287368217261f4794a4..44350c644f69765746b27c877f44e83609fe27f7 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/equal.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle index 221c3d19676482e436c62cdb72ddac35ad214815..d4667be0f775c7c7cb950e02ab0ad5ef4916f0ad 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle index bdbccbefae2dc1d36143ee499d4df726b3f31ba2..c77722b1f2eef4a7176512ab01afbe8a9bc04105 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_acsl/funvar_inv.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle index 9623ee6b44e66705547a0bfbec2404db511a80be..c8fc8cbcd728e8755a88b9e67d175cb07f2ee5b5 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/implicit_enum_cast.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle index 9e580ba61f011754b8d6b9490e4514b540f27bd4..b287d5db2dcd64db87e829c6d96f04cb1e8f74ed 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/init_label.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle index 8e07203beb342c7e94c6952f4a32eb84ecea1a6c..32404156c7eb17d85dcfa3361748de3405ebe715 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle index 8a569a28b306946259357fa9a5f801ca4555f325..d448c6b3d8f9a82d4b152a996130a390d98f411a 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/init_value.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle index 519128a270eb42f08122a8b30e7f79af7e3fa19c..46b74f8ec7075f532ea44274b60247e65329b1da 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/init_value_mem.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle index 65099e7692bbd9ee01f239c49af97914ed4ca9b7..0185197bcefb8378d37866f7c7ca70cfc3ee5b7a 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/intbool.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle index cf4c863ff128b2ddc33e1da0a9fac6d138b01675..5d5625435246e5fe972f5410a7fb34b07cbfe082 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/label_escape.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle index f80035a90951a4ccddeffbb25a4668ff842c36b0..876ff1d2ac0b070d51b22d26f22c0ca756c3ac3e 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/label_escape.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle index 8351bc41d1447a9f839ace58671e8d9855d542d7..68a296dd46dbd97ec6b6cfe215de2c1a76f2a45b 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/logic.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle index e382296ef4659598f2f04c2aad341883dab4b19c..2410421196075407c564baeb1a827c8694077563 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/looplabels.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle index b5788d4ee54512314f2b7e8fc5534d60567eafce..f0976611dcc0e19acde3048476db2c4f3ee0d10b 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/null.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle index 7c110cb79dfc4f4bee8218a36d1cc681bb9a7d66..3638dce1955a4a1e48b6bb9237273cc1e6f39f75 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_acsl/pointer.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle index 205d8ead9ed263acf0de6837793376e9ebbc9015..9d969ebd5f4bdf3fd4692d79f7e8fb2dccb5657d 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/pointer.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle index 5ab98f1194f58b1e337fba22e51d2b34b94f636e..de5309578551a504b2adc8cfd99786a20cc2183a 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/post_result.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle index 627cd3b588edbaaa492f369db0c98e0d60c804ba..f834bdff41e501342d70558f49388212a63d2df2 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/precedence.i (no preprocessing) [kernel:annot-error] tests/wp_acsl/precedence.i:90: Warning: unexpected token ';' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle index 14de3dc9b9971cbe838ada5d33d0b82302b24d23..ccc22350c9f1603f24f41856ea07e37191374e86 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/precedence.i (no preprocessing) [kernel:annot-error] tests/wp_acsl/precedence.i:90: Warning: unexpected token ';' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle index 8dc5e9a29d334ee81f52fe481c67d4e12e88f8df..e4a282e1d29b0a4e56f064a7ae5ee2c8dad95856 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/range.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle index a5a0d165b2fcc5e4407cc78023da2acb7191884d..23f22eec01d795099982854a854e3feee8a1b598 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/reads.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle index c40c87ec26c562b10a814447525a01bcd96dc71b..5d02297a0fa5979f13297e3f703bbfcf16fe7e3e 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/reads.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle index 54d7726924e42e3fa643a2f44fad0ccb13ac1143..9871b438a59866e9ef6750ea63f66395effab7b8 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/record.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle index 1132c478b4b53d0eb424cf3990ff7bd18e191eef..e503585628857667622ce4428d71bdd27acd821a 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/record.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle index 384bd75e15532b9f91c12bd7c7e4ebe703d2590a..1ffb95b1d5eedc17adfce94425529a197de8fe27 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/simpl_is_type.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle index 498f74657dc77b70ba8f42508ead5d6e541a1dc6..8c9276a68e7cd532699f57d5ff1744c882c1e493 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/sizeof.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle index da7fdb385c1caa6a7a18b1470ce1181936ce9d75..074954472b7d674670a9feb82dfa40bb94731dcc 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' [...] [kernel] Parsing tests/wp_acsl/struct_use_case.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle index 5313181afd3f7ced8c164c6b67d6d2c960405094..628c2eb2f84538cc4b72501f9beac24804ac3dd0 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/struct_use_case.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle index 12b3d155f8be29268fc07f0449de0efc646f4725..8de21842d8fbb97d1358643df647726d2fe518c2 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/tset.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle index ddfbb1e23486e6e15b1108799cfb77b10b103c1c..66fb81dadf2992751cbdff88a688fe9a0f4d3658 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/type_guard.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle index 09fd140cec8f65b106dad00ba0d4cc8469bc500f..ca7c410e823e8a0387fd7c273d8747376a537d87 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/type_guard.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle index 36e568d169f61b9ce5600e94b3a8cb1f9c430ca0..9c8efdfa48e60242dceff85de5b16dc6a0a14ff8 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/unit_bit_test.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle index 48b1444f5eea6b9f51fedb4cf936092cfa4688e5..a457770ae98a1c44a65a2ccac90ec9cdefb6119a 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/unit_bool.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle index c8becb7fc24765bed7959648be700b5b5a0828ff..3eb2f63b434bb900e407f1fb6dbe81c157f68a59 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_acsl/user_def_type_guard.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle index 384654b8407866cd3e6a8ad7086ce4a63a34871f..d5a3dd35879fe81ed58b5a1bc72ff5466cb466e7 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_acsl/user_def_type_guard.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle index 92e03a00f08112f410963af62be988bc9e6e8d60..f84001a741b81c764034372d35bdefbf903406f3 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-rte [...] +# frama-c -wp -wp-rte -wp-steps 50 [...] [kernel] Parsing tests/wp_bts/issue_141.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle index aff0d060520798f8cd9f66eaa293c58cf6489b98..4be131e60409c2020a842bdd0ae2ab01fa35cf0b 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts0708.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle index 33b4eab16620e6aebad92ab88de54117828e0be5..6ade8dc8e47d7d62db7bc92fceb4ac95519e0ca2 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts0843.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle index 4282d2c325ed9f4a51cfffdffcf7bd90f8710d10..e3c50082e0ac7d4a71ad71723b5dc8159bc6063b 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-rte -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_bts/bts779.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle index 1215384b9c189e02cbab664bff0b7103c5a5291b..5cd9ede34c1da3c9383ae83555f4ff3673995c65 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_bts/bts788.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle index f28391971bd4ddecae9032b80d400cc2994db4a0..360961ac42c3def5b5c22ba3cdfe5a435aee1185 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_bts/bts986.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle index 374c06fec66e57309d74321eb49662b61147354d..4de546639bdce94817bb66c119bd9dd11ea8bb1e 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Real)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Real)' [...] [kernel] Parsing tests/wp_bts/bts_1174.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle index 6a39dfa841d142c2718620cb1567b07330b19d84..746589ddd94348aec7cc86e69d150da525fbe387 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_bts/bts_1176.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle index 61ff3d4d143239a6c98a5675e9d92e75f879c72a..710eb3051e1cd6e1dbdc94c374cb9236ea4e233c 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-rte -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_bts/bts_1360.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle index d45f3ec09d3b0122e557e3b2b910a6fecd942f93..eb31be8a44ffba5eb0b43cb007262a89be0dfbee 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1462.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle index 722fea991544c5bda4ca295a89e6aa4231ee5788..ce7b8a4fe68ac48060a4b00f9f5d6d6d2b916fe2 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1586.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle index d3080fe82353c5930f7b03cdb1c457dc321de053..55913b62c703f179534e696b2cf9deb9b0ccd523 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1588.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle index d121feba83671afe3403b57c1f1680a09a400bdd..eeccda7e270c592e753c1d0429a739688b6aef55 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1601.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle index cccf36bcb811a33aad6db7974ad8b997b88eefd3..99bc35317b0c035e229adecc85911840f4de0657 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_1828.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle index 7855fdce2b682ade757aa28766716c738e323b0f..8434a188aab590de1c135d9d6b42e879b9281425 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_bts/bts_1828.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle index 1c2fe17584e25389eabc964a263ad5aa6e7ef2ba..4d4b554f999735ad1765a76f7962b5e40cc0141d 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2040.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle index 40b78670f5ecb93d9d8ffb7a344292208a1ed931..d4b8e198b08346e06d4cf6f685de7d40b02e427e 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2079.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle index 79511ba17200cdf6d780424e63b96a5eec1edf7c..f241129fe79416eb622e6e08a9a0382ae2c20860 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2159.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle index 9f89e1687a37d3daebda3ed5de1544568b1271db..e0de6d5f1e0f840efc616420df58ba5df14897ba 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/ergo_typecheck.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle index 4231e564c8c7761d3b20cbc6b67ed871a8d7aa65..42d8ba9e5b75175e08864dd5d58147c5acdb2982 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue-364.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle index 341cbfc3a200bd063b6f76628c03074d47be937b..e3ee19b027bad6735968cefd342c5cafa24922b0 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle index 5809812ed6884f8379efb13e39220c370b7d41bf..6985b4d2e2f79547295f3d204986459fe4b042e5 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle index 020e138a0e7dfdc7abc0c2c612f7ad8a6b7c0017..feee3c9109990d2eebec4549db1f994cd3b95c2f 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle index 740bb8ea13f1704edbe9a73b46b88a36d8170360..e9bc0c7109c1f4fcb013f7f3a1586a9cbcedf86d 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle index 377e3ee717a2a10acaeeac0a449e40549feb62b6..f391d02b573f44e30cbcd5fbfad230fe371fe8e0 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_198.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle index 06085822d33f851a729a86c4879786dfd6aa9ffb..f9611321b0c07ecc9cd0cd6a62b5fd80c99f8ad4 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_447.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle index 5c91074b9d16dd1af773f8e70f375031623fabc2..a1ec9480bb7bf24cd58d799150e56fb4bac9071e 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_453.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle index cf0252e05e8ef594e2b3a7929f5ad0a924178968..592d4a5f61330d27a4ab5382dc872b9f212dff89 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_494.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle index 62d996fcf99309c0a209120b5f0bfcf882c0c507..565ebf75c772f30336b80a9a15332fd752615d91 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/issue_508.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle index f5969a63fa8a537593bd936c02243ac3ee4c8a4a..bfdf15d4931fd44e05f315d8ddcd4ca2a4516749 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/nupw-bcl-bts1120.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle index b12a5179d4c23014d11aedb8ef7d40f82b89841c..4aa305f3c58224b6a063e5ea5469de67bc6af1d1 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 -warn-unsigned-overflow [...] +# frama-c -wp -warn-unsigned-overflow [...] [kernel] Parsing tests/wp_gallery/binary-multiplication-without-overflow.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle index 8bb2f2aa48ea3cbc255177e1045da19274c25a64..42de806ba95e3bdf08b0418a6ef801e25fc89e39 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...] +# frama-c -wp -wp-timeout 90 [...] [kernel] Parsing tests/wp_gallery/binary-multiplication.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle index 650002bfa46b9f86b1f1595fb3526edf99be9908..3d750b31c6924c9d1666b8dd25f1a34f2f52a7f0 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_gallery/frama_c_exo1_solved.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle index c0bfb08ca3b50875c885f9c27608b26cba945941..deaba47c54d9188bab890c5eaddf280739a5b0f0 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_gallery/frama_c_exo2_solved.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle index dc1ca6605e834de70c1aad21315ba2111899f361..c74a9513362d1aeb26482ce4c48f074ef3c5e2ac 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.old.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle index d28a3f0f2f2e06514de6f54968037e101b5054af..4476cb8738de23963295cfc67b47ed296d44a87d 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.old.v2.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle index 86b8662c59195f595d4a2841bd9693bb8d8d3611..5c40a1cfb36666e92516c004b8d45ec445061215 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_gallery/frama_c_exo3_solved.simplified.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle index a89aa37dc9e87d333b0dfed181a9ec8b633e7648..a551c80874c5dc909fbc66b4c6143d3a0e826539 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_gallery/frama_c_hashtbl_solved.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle index 725c096960479d6f80a10937322a69ccc1ff865b..5f587e1a5d0eb36d6ee3b553999873d8d23a04fb 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_gallery/loop-statement.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle index 26633fe44659c00f8ff75155e449fa90a45569ef..185df39d3ab0baa7dcf76c3829444e2c583ab47f 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_hoare/byref.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle index 90e3b2a65808346eb24e680eeb77fabc9c135ef9..a4876a5fd53d3927efc6098ecc8dcbfb5d5d33db 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/byref.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle index 8988bb2d21ba66ffe402fb47d67b3dc7fe25c76e..82582e12b00c8c44d24ba4744f269cebeca8210e 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/dispatch_var.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle index 585e9038dc75a2172fd6dbcaf2954671743522c1..16765c955e3a3c90e2e267ec7fade38c9535b95d 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-no-let -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' -wp-no-let [...] [kernel] Parsing tests/wp_hoare/dispatch_var2.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle index 750611233e6b6dcfc967034f9b14632b8b5e72f4..5757c0013bdfd8d594402d25a8b0c063c53388b5 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/dispatch_var2.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle index f4bbe476b3eb98c8b99b52fc0e915c59269be4b9..435a2090821eaa33049f181910c159a92d93038d 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/isHoare.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle index 4a3a8203b8cce59494795db9a73e5b6439e01730..ab5a5a62ec3ed9f0b8802c3227965dde57e121a6 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_hoare/logicarr.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle index 06c19d356c80224193f34110936db2574dffa189..084f416c0a5c907c739b824e6f2e2a3628ba5251 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/logicref.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle index 11f09dc4fe7cfa677a6c0bdbed0dc4bcfe4226c3..8a276ac051f9454e9344f2949407d60fba994155 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/logicref_simple.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle index 974bff5d6c4ab589faf9b16964868f184ac614a2..604da7253962730f81a47a06e85c2a95c26cc177 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/reference.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle index dba3f12ed283527f0f62f7300a814d8d8fc3e887..8980ef3f8b50487ff654448b52da3c09749d5f10 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/reference_and_struct.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle index 19d23d6357938cca885c1adf99e7b4466ac3553e..9ccbcce0d1f0527e0f79c7f637c0cda62141b311 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/reference_array.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle index c4971ab52e2157a9e2831ab30da39c555dc02430..78b38ba1195b50e9f5ff97b9a4c6d45a7da58aac 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/reference_array_simple.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle index 1bef150b691a095304a330ec28cd024e22fcb4f2..4f3725c5bb2c930e420db1cec44484b989ca2daa 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_hoare/refguards.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle index df1f35bd569a09d119bf536e99dc4f69615c5aba..a4c3d2bc111137836ddce0acca61c839f0687a1e 100644 --- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle +++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_manual/manual.i (no preprocessing) [kernel] Parsing tests/wp_manual/working_dir/swap.c (with preprocessing) [kernel] Parsing tests/wp_manual/working_dir/swap1.h (with preprocessing) diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle index 39ecdb3048af5a4c01b827814846b46d10077584..5897a7cede15c1f0b21e79bc4b2686ab13793875 100644 --- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle +++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-rte -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_manual/manual.i (no preprocessing) [kernel] Parsing tests/wp_manual/working_dir/swap.c (with preprocessing) [kernel] Parsing tests/wp_manual/working_dir/swap2.h (with preprocessing) diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle index 83a1077be56d572bce041153e6f50235bb16f792..cad3da72c7dcfc78c9447a6695165eb34eec0a44 100644 --- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle +++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-rte -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-rte [...] [rte] annotating function swap ------------------------------------------------------------- Functions WP Alt-Ergo Total Success diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle index 3be28fd7c30ec04da6d7e8a1a33ed4b14aa58c9b..266bc9673625f68473a544c9d518f470b5b7e9f2 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/abs.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle index bee639e5bedba2217eb554615f780b278e3aee82..4b9063d0f178130732921868959b1cc8bf2afca3 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/abs.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle index 5ff11df22997fe2251b4e42d0ef8c36046e2d9f7..c56a75a74f2900e6ff2ab6b0b7f26d96cb053126 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/abs.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle index 4737abaddafdf4b9fe82fde1ebb402cf0e08afc6..b7c278753cf17af36dd6ea1e994bb81b13ee1d73 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/asm.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle index 40432fecac9796bf6a8309e254f86d77942b22df..93c9d28b2329d3ec978a1ec326c31b3a5cb0f82b 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/bit_test.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle index 7edd3815e32b6afc8c24d3642212bc6be9b51419..cf4825d1b682fab9f601434a2ac7b74b366b9df0 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-no-let -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-no-let [...] [kernel] Parsing tests/wp_plugin/bool.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle index e58dd159662b31d042d3b6b0b81e344cb50fd5af..d663290a72fbe304f0409c6cfc07c0f8db78dea1 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/copy.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle index 3a2e135ecdeea288f12d98f0b59a8ccacec55500..7fdb8a52676fac4bfcee9da841bcfb4aab010d13 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/dynamic.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle index b60e1d430a69f0c5fff4abd75613d0805f71d97c..424e076b6068d9251c7ace2c47755f79ff19762c 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp [...] +# frama-c -wp -wp-timeout 1 [...] [kernel] Parsing tests/wp_plugin/flash.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle index c711d65adab2c7627884e9744ca2f2f4b867cdcc..29dde40a08d80b5a59d453c35479a2a6362fd40c 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/flash.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle index 1712b1e0c1871091ed0ad097bfcb8b3d756b47df..803faf1078bd49153e3508f0b7812aeefcd67ee2 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/flash.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle index 3e525c780366ac1535c5a41df8d0faf756c4226e..8f2da577ae2b91e982e22236096af9b0387f36cf 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning: Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle index dff0921f02e5a5d5791bb1656a780c8aa34df18e..9f87d54d4ed370a5490dfc6b41b9a0f9e81abe2d 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning: Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle index 1aef24e167aae8bd72bca9cc4b0b1141851fe3a0..2230d173868d3de4a87b2ea35b6a238d9a296e24 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp [...] +# frama-c -wp -wp-timeout 1 [...] [kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning: Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle index 31633324320eef03e7772dceca65bbceb3df7683..00476c270d854358a93114ab4b8798d2638dc444 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Real)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Real)' [...] [kernel] Parsing tests/wp_plugin/float_real.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_plugin/float_real.i:19: Warning: Floating-point constant 1e-5 is not represented exactly. Will use 0x1.4f8b588e368f1p-17. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle index 43d07c8326c0f546f7e97d6dd7d21eb12e9ebe5f..82e758381388a01df4390cf51c8ab9a9c1a7e9fb 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed' [...] [kernel] Parsing tests/wp_plugin/float_real.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_plugin/float_real.i:19: Warning: Floating-point constant 1e-5 is not represented exactly. Will use 0x1.4f8b588e368f1p-17. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle index 773b4122b041c1fa129091f5d7ce9dd086acb56c..8247a946f2452f3d7ad4fabe8e4d679ba797ac4a 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/frame.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle index 4341a8387fac517ae66ea4980de6d8928a9704d1..f5f790a0cff2610ddeabcc70c7a3855eb8078f1a 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/ground_real.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle index e58fc4777e8012604626ae376347f60bb26cf998..58f1a2f1d9209618e89faafebbc1c4254004245b 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 240 -wp-steps 1500 [...] +# frama-c -wp -wp-timeout 240 [...] [kernel] Parsing tests/wp_plugin/inductive.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle index f719ce191c98e10950e3f51bc336b6b54413be44..bc0a1b82ce3a7624d46f2f2f0ff7acbad2150cbf 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/init_const.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle index 74fbe6265909520852af9cb5ba3bcf0c7d32a8a0..c2c2e3ceccba326c240a62e8d27eee2feb2e024f 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/init_const_guard.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle index 8fee97c8110c7ffd2ed80f7e0cb00e502bf15b68..1538d48fe05df12b2ea5f031f48fbd0da3d4dae4 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/init_extern.i (no preprocessing) [kernel] Parsing tests/wp_plugin/init_linker.i (no preprocessing) [wp] Running WP plugin... diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle index 9a9e12457487933fcf9ae2ef4a740e0a4e13cd0e..c303e914f2a206dd6e1eba7f310e49a73fa1fa2f 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/init_valid.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle index 06ab6be80f469b8c42f674f693cf1837eeef0cbe..3e092c0517374eaa9ac8ec3aa51825fbbd923925 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/initarr.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle index 09a1441179746ce863839cbdcc68f7ec44ed9d37..21e508fd59198c77d1bad1ec5d77b40c922fffef 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/injector.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle index 8e07c7e303008a3472678de0979ddb2f1a619885..b4667f759fafe214bf078668e22afba5bef27309 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_plugin/injector.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle index c73a0cad6ce48aeeb1ca1992948d20285693caf3..84704dba34e66dd794e4d8d57af1205cc56fb6f9 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/loop.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle index 887d7f68708dc1a848a60aa321059b337190c26e..1243a954f859f9d6e03ac990ddc16b4057a46b5c 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/loopcurrent.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle index 190504de364ff5fd3eb30cca5941465b89c01540..73078e24dae3e5475cfbef86b24ae6139e281755 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/loopentry.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle index be03eb0c54595ad6b793cc867b569f7268407899..61bff7f94a53987b34e56f173cf691bf19b4c5ba 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/loopextra.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle index 80f261630b6e9f3ed59ea6ccdfc2e159d55d9840..85ae2cc2fcd0da78deff5a45841fd0485d9fd3d7 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/mask.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle index 7af20aa463349c08e99a3756ab5764bb22622264..fb561d0e65eea8dc3d908d4512eafe5ea289295d 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp [...] +# frama-c -wp -wp-timeout 1 -wp-steps 50 [...] [kernel] Parsing tests/wp_plugin/math.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle index 51b0b773d0db71ce840809567ecf91a75f260867..6117c36a1ed9e8201c05943529493aeac4879fa4 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp [...] +# frama-c -wp -wp-timeout 1 [...] [kernel] Parsing tests/wp_plugin/math.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle index 9fbeaeadf91429555fdf9f669b578fe91df55c8a..e643d4c567daf51c79055402f3cf01f7a869227e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/nowp.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle index e86cc65ef01943ade9b9d4597d5293ac746f53dc..e4b76ba866985e3b93dbc7338d2fc9a4765a1187 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 -wp-depth 16 [...] +# frama-c -wp -wp-depth 16 [...] [kernel] Parsing tests/wp_plugin/nth.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle index 0815def0020a7db6e8c38ed38a666140849c8555..c243d5abbdce640da88552357ce524252e8e4522 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 -wp-depth 16 [...] +# frama-c -wp -wp-depth 16 [...] [kernel] Parsing tests/wp_plugin/nth.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle index f3b60ab008961fb5341fbf9554a81aa247ac721a..9fed766a89f00383277a2a549628fe1988cb5d97 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/overarray.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle index 75b57c96bb52e19213403b8e9b1b9b459cfef807..b8758ed7581120597f270c9f128dd8ede4528a5e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/overassign.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle index 472834ac035cc5379ae493d77fc563e45edc9b8b..281d6f5ec593145eee51ba16a07b40ea4e666729 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/params.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle index d77ba62ed0b65f94f7be90e9ff932d807b89b8f3..cda0cfc000b9642c5a5edff2a217b690624b503e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/plet.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle index 001d2294e71948b34e2b7db7c6f80712c55640d2..aa3a09060e6a2af9016f5c23e2d7440c8cf61624 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/polarity.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle index 5caef16184fc1ec7b8995dad9dace72f0b53110f..bbe0916d104b0e192bcec9ae4f751a9fcf06cb06 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/prenex.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle index 3a7456bff6c60d9788a9e55f3e41e125ca441471..eb995af1813c90479e30ad40638cd16e38a41128 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/repeat.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle index ac262be90812cecb6917673e5050d63a3296fdce..417ba94b1f097942359616890a1021290140bec0 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-rte -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-rte [...] [kernel] Parsing tests/wp_plugin/rte.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle index c2817aedca9085f5f44158f0d53162e6d5aa1b61..555a56a8bda7f06ab309b2c970f7831ab120c304 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 -wp-depth 16 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' -wp-depth 16 [...] [kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle index 60d453b63fce576ea6d8f13808e8726606e9ea2e..23a0acbb4ed0c9f7c0e5cc41b1221d5413a3aae0 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 -wp-depth 16 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' -wp-depth 16 [...] [kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle index c637752ab865f76a65a39b925f46ab5253e3bd37..4c1eec778b0b570e3eb81f6583304940983e2c8d 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 50 -wp-depth 16 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' -wp-steps 50 -wp-depth 16 [...] [kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle index a27557f5d76d40812e9fbba0827875b36c140e77..5db0c6c63cd4bb28e87aefff871a797438fa3bf6 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle index 13f3d7def48d65c2d6945c2d8d50c3e48e6a97b7..e1033c3097e5418ab115e472bfebcf0f2f637bf1 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/struct.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle index fdcbde2330850ff9a650eaec6caf4d70feafb0c0..e372635af1201315b88338298b4674d4044faeb2 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/struct_hack.i (no preprocessing) [kernel] tests/wp_plugin/struct_hack.i:46: Warning: parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle index 87dc894abd202f89644685e3ccdb72c8042c452d..b9adc00779472dcb6c6b07e3e4bf43a0fa835bd9 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/subset.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle index 26b6ff968acc1c8c7d6e0ff57e07e27a18383f4d..6c887c02728915d1e379da10f538f9d2e7f48253 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/subset_fopen.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle index acc077c487728454faf2e382a93d4f058533b8d9..e53872ad04a782f50d7e7d0a15550246fae5b5dc 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/trig.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle index bf1a7e953c79bc6f24fb32d5a8c0a8ffd86b2ebe..c077b5a44c1a4c38af7d11b03e83cc6fa1917e77 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unroll.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle index 81ae9d616c3ffd01a094c00b44111b4dad2b9a8a..61a5c555291a5cba3e8360456dc7325908eff2a1 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unsafe-arrays.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle index 65756a3d261611f45290ed81b457928767c00b37..42aeee4e9a9e690d98379fdc278b77ba3b46149a 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unsigned.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle index 8fa3b75a019bd11d31d5954436d43c7ebff7ec86..bd4a0fcd4acdcc479dfa27c686bb400cd8d1db58 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_plugin/unsupported_init.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle index 486277148c2b615ac8884661930b44f25fa8f070..688dc734ded0d204998132a54fd180a5385cce31 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_store/array.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle index 4a6c59025d9d5eac465ef05f4729ba60f51023bb..df7d99285199c8506fdeb1d8aead575571546e80 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_store/natural.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle index 4f2da7d33510743596cc85d000d7250dde13f9a1..308c618c46da5c2fc1d2ba33d2bbeda73c3c341f 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_store/nonaliasing.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle index 244af382e0549870f08fbbd8a8959dedc8987a0a..359493b38c24ecff90aeac5f806afc645c613163 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 50 [...] +# frama-c -wp -wp-steps 50 [...] [kernel] Parsing tests/wp_store/nonaliasing.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle index 162e249c284a25103bf26b39b83ed4aecd79fa96..02c96c873c8b9d70dd945e2c7951531a09814a2f 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_store/struct.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle index 4ebd433885c3414987c5b00fd15954cef872be65..a189a671dc8975ceed01fa53b61b5bc60867a5ca 100644 --- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle +++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_tip/tac_split_quantifiers.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle index d71cbec20ec2ba57e2f9136a547de6c412bd7bd7..bad51ba3f9b0a8390c505c2901f954fa7b516ae1 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/array_initialized.c (with preprocessing) [kernel] tests/wp_typed/array_initialized.c:13: Warning: Too many initializers for array g diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle index 407f88f1e8dca2dd91a571c38fdbcd9b396c919d..1c4aad2918c041cddd328830e5399d8bf0eb5f8d 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/array_initialized.c (with preprocessing) [kernel] tests/wp_typed/array_initialized.c:13: Warning: Too many initializers for array g diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle index 882fd42aa67fcd60983696e0344edb2ea46445d1..a8932bccedf0b6a407165e0a8e2c9503a00e7593 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/avar.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle index 68e665c137e8ce9a49a2d7ec9fd9b4a03662815a..de595eb78834b53baf22ad0a68a4f31a2565669e 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/cast_fits.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/cast_fits.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle index a64bd492a48b533063f67a46bc620998aed335ea..7c6f289582ec1efb2896b844fa9bde729fba1a8c 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/shift_lemma.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle index 8549fbcc64f0223c9a9d18214fea174152e0a9e0..fc0bebfe6e6c32fb33b1bddea5e0bd791b6811ec 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/struct_array_type.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle index e8a1ae26e730dcde8d49887a0b6c277f04a26475..33c30e5011ffb60e802f90a6349566f6a680d721 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_alloc.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle index d0235b8a0873f05cc47e5a026484c823e75a997d..44d2660eb212b4aa20727e4889cc47c4d161f358 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_alloc.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle index 9a11fc16b0ced3efe537cda627bace6c888c54ea..84f7b84effb20be4db4da5bc3988605987046ef8 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_bitwise.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle index 1c1f801a70c0aef7706b91635e9980f12d0ad42a..f89e7bf6498769582592c7062cab02596f10c0db 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_bitwise.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle index eb02a84c8a14fa3e6d31e0ddf486444ea0387661..d9dd667a56392061d1021765053171ffecb610fc 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_call.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle index 92b3928c5f7c495dfaca780f50cf7aa6c684cd54..32cabdf891b34ee11803c54f24f23f9fb7d26c36 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_cast.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle index 27195d8e897753d79f385a0f0d93f0ac540ec82a..4c071c988dc2273c396cf8dcb45305ce120b1771 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_cst.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle index a636e612e81df564f9fdb164b7b7fb65284ba954..2b61ac101b76814dd56c7ad75e7c42d338d4e9c0 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed' [...] [kernel] Parsing tests/wp_typed/unit_float.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_typed/unit_float.i:21: Warning: Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle index 5aab1b036220867e4957a2661cc10e3af6834eda..b5a6c46d069cd94900077f88522254a63e42798c 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_hard.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle index 2f4749d9608805b97dd6e8b971da74397b22d839..176778cfcb43b6b114b21b8ee41cbb6bf62b18e7 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_ite.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle index f83f7c8a48375e803b02f6705616b6c2a8580c76..6ff11cc1d5c227b5904f067522094e9e367ccd1a 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_labels.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle index 34fd709d63e75cb42f6cf067203f23eef954f495..187ce05819653312a9a7e48b448da687af3d3398 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_lemma.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle index 4a7acb218e3b2549ee7364e57b16a813ab2c921d..8ee86f601117d0b6f5ec0f74584de8b72ddcbe80 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_local.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle index 907467024d1d1358a23de8569151f9c9ed11e151..f0b944bdbcce3e819d288fab774b68e286f2a58c 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Raw)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Raw)' [...] [kernel] Parsing tests/wp_typed/unit_local.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle index bf3d6522ac99eebaa0ee7cc29f804e2a1afc5a6d..28cab47713a5fada2c6cd1e0bc71ece49bb732d6 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_loopscope.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle index 41ceb697fd285fee441129e068076ef172eba313..514db21cf01114521244bdfe6b8c5d2044851f73 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/unit_loopscope.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle index 522383856688d3c27bbe7b00b750db0524a625e7..b4416b982a1dd792608361c339709e253b760492 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_matrix.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle index a8a5e99ca4c6c0a93a87800b9ed35ac84401c48d..05965e3ea997380d09ef2291cd261f20b328a747 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_string.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle index b9b2d0e9c263b7afd666dee898b4db2c6b3cd038..2a0fe19ec722ceb8859414da5a182fe138e4bed9 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/unit_tset.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle index d26be5ba50b3a72e23c8e952854f323150b5fc78..5408bc35bad4021aa374eb7030e56e0cc1d5dfcf 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/user_bitwise.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle index d63ff2f336b20473ea1dea71b2b7933d8f4e7883..edcc63f630692b4347e34264dd672acd68d90ae1 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/user_bitwise.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle index 0322e3c7950cf5ee16c2c09f28818897e17ee24b..4aaf43770a3a55096891adaf170819eec7683580 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_collect.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle index 549deb2265ca02a630d5e7a9d8cd5eecfd658186..f6b7811bc5a255b6b10447860ee65b864b8be065 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_init.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle index 0a25b0620ac8ce8de51629ac118b4e95b49a7503..2bec0646b50479e99a1b76fe7a6357bbf84c1b09 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_init.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle index 18f10ef164aa265909e5d14ab325151a51bcc1c1..5d0066fd74ea0aa5b4912e279a74880b4d099271 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 300 [...] +# frama-c -wp -wp-steps 300 [...] [kernel] Parsing tests/wp_typed/user_init.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle index c2358598c8dac977ca56732dbbc43083349748b1..c8197b04ff7f89006fdb9f02dfeb7869d967f3ac 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_injector.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle index 347c74e839d0aaaf9da291d6e7ee87fedb65ba17..aefa32d0a90bfe3dd2c0c2081463ea3a9038f084 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/user_injector.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle index 004a6b35b205717689bc86109b9de4f063ad1b3b..b3cc0003566606d2217a47c75ced6a0afaf1aeb7 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_rec.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle index 68f3ed824c653e6c755c6b4d67475adbaa43f8c6..0689081a4c3db7848d65b23c4e193fcd905ba59e 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_string.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle index 260b1c3252fe37060e6a22c09ec6e994caafdc81..a8f54d19ca9e4071ef9e9095718f97ecaaf2f6fa 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_typed/user_swap.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle index bf1b70d2492d61d3b56ff8ba8ede0613df47cd52..7b634d3983825d2378a9829a75692476ae6337fb 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Ref)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Ref)' [...] [kernel] Parsing tests/wp_typed/user_swap.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle index 0d5c1cdfb0c6883ac44538cdad5380421deedbed..4993df34f430d10e46b869d26ea9107392ba0309 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' [...] [kernel] Parsing tests/wp_usage/caveat2.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle index c210cf13b65355cca9e05876537e49ed8252fd4e..5b69c867545a814e366b0dcba77c76fb53337df3 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Caveat)' [...] [kernel] Parsing tests/wp_usage/caveat_range.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle index f85eb21dbeeba87fc2361e09cf7d60ea92258ee8..b0661cf032828930c048a589750451ae7ea2de11 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_usage/issue-189-bis.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle index d5147644f0c99886f5aa85fb419036673013a675..da52504bdeb3bdb72adf62cc07d6c47db95967d1 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_usage/issue-189-bis.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver'