diff --git a/src/plugins/aorai/tests/ltl/goto.c b/src/plugins/aorai/tests/ltl/goto.c index 4051a1c7461bebeccbc938ee835d02f08dcf42e6..abaf6d16f737c744fb157a8d30f8b150e562dcef 100644 --- a/src/plugins/aorai/tests/ltl/goto.c +++ b/src/plugins/aorai/tests/ltl/goto.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance */ int status=0; diff --git a/src/plugins/aorai/tests/ltl/test_boucle.c b/src/plugins/aorai/tests/ltl/test_boucle.c index 47794157e8d1c20902db348db6355a853dd3b29c..6325177b5bd437c00db0b8dfde3cf6e93afdfe76 100644 --- a/src/plugins/aorai/tests/ltl/test_boucle.c +++ b/src/plugins/aorai/tests/ltl/test_boucle.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance */ /*@ requires \true; diff --git a/src/plugins/aorai/tests/ltl/test_boucle1.c b/src/plugins/aorai/tests/ltl/test_boucle1.c index 5aa255651392ad16af77e6accd80803e74a6e101..b66e6a7c829a6641fee515eb30d1d5d629babb42 100644 --- a/src/plugins/aorai/tests/ltl/test_boucle1.c +++ b/src/plugins/aorai/tests/ltl/test_boucle1.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance */ int cpt=3; diff --git a/src/plugins/aorai/tests/ltl/test_boucle2.c b/src/plugins/aorai/tests/ltl/test_boucle2.c index 4145427d820836707432eaca4eba6999d714c69c..257a9a19b810a573fd18230f49c00c6d9eb04c2d 100644 --- a/src/plugins/aorai/tests/ltl/test_boucle2.c +++ b/src/plugins/aorai/tests/ltl/test_boucle2.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance */ int status=0; diff --git a/src/plugins/aorai/tests/ltl/test_boucle3.c b/src/plugins/aorai/tests/ltl/test_boucle3.c index 013fc8878c153ebe299d2f12c8b99fa9b0e0a209..1cdc2b029c0761d92a9581b3357538be358e2cfc 100644 --- a/src/plugins/aorai/tests/ltl/test_boucle3.c +++ b/src/plugins/aorai/tests/ltl/test_boucle3.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance */ diff --git a/src/plugins/aorai/tests/ltl/test_factorial.c b/src/plugins/aorai/tests/ltl/test_factorial.c index 3a47201d2f6459ece6a01d9809ce9da7f1fa21a8..313ecfbaa750192ad1cdd36a783fbcb75034e141 100644 --- a/src/plugins/aorai/tests/ltl/test_factorial.c +++ b/src/plugins/aorai/tests/ltl/test_factorial.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl */ diff --git a/src/plugins/aorai/tests/ltl/test_recursion1.c b/src/plugins/aorai/tests/ltl/test_recursion1.c index 781af6b7a8e4dd537958d298e11616822fb82004..a3f69a89db840f6a582edc7e2c8eaec921b3354e 100644 --- a/src/plugins/aorai/tests/ltl/test_recursion1.c +++ b/src/plugins/aorai/tests/ltl/test_recursion1.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance */ diff --git a/src/plugins/aorai/tests/ltl/test_recursion2.c b/src/plugins/aorai/tests/ltl/test_recursion2.c index 53277aac6823f3c0d423616c3017312483749fc6..7effcb5bfed5a06821d505ee9632fce32bffdcc0 100644 --- a/src/plugins/aorai/tests/ltl/test_recursion2.c +++ b/src/plugins/aorai/tests/ltl/test_recursion2.c @@ -1,6 +1,6 @@ /* run.config* - OPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ - OPT: -aorai-buchi %{dep:@PTEST_DIR@/test_recursion3.promela} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-acceptance + STDOPT: -aorai-buchi %{dep:@PTEST_DIR@/test_recursion3.promela} -aorai-acceptance */ /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */ diff --git a/src/plugins/aorai/tests/ltl/test_switch2.c b/src/plugins/aorai/tests/ltl/test_switch2.c index b489cf8ac42af7cf66e06fc8de4a9265f36d7a66..637be79d815d361f9bfc46c8a9e4a5ed15a33768 100644 --- a/src/plugins/aorai/tests/ltl/test_switch2.c +++ b/src/plugins/aorai/tests/ltl/test_switch2.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance */ int status=0; diff --git a/src/plugins/aorai/tests/ltl/test_switch3.c b/src/plugins/aorai/tests/ltl/test_switch3.c index 6954b71bb89ef6d2358260465765c77d74764065..037f58fb2c440a7277b5aed83fb53308be15fde5 100644 --- a/src/plugins/aorai/tests/ltl/test_switch3.c +++ b/src/plugins/aorai/tests/ltl/test_switch3.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance */ /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */ diff --git a/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c b/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c index 7315eb493f479f40b2ed17aa210dab9493388e88..9ef5f759998d7cbc088c6db9030f90ee378ac2ca 100644 --- a/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c +++ b/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance */ /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */ diff --git a/src/plugins/aorai/tests/ltl/test_switch3_if.c b/src/plugins/aorai/tests/ltl/test_switch3_if.c index 9fd6094996fa13fe4b773afe5c58b4bdab8ba52f..f79a2dd7b113bd8ae03f4482ad03cc9909306c47 100644 --- a/src/plugins/aorai/tests/ltl/test_switch3_if.c +++ b/src/plugins/aorai/tests/ltl/test_switch3_if.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl %{dep:@PTEST_DIR@/test_switch3.ltl} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-ltl %{dep:@PTEST_DIR@/test_switch3.ltl} -aorai-acceptance */ /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */ diff --git a/src/plugins/aorai/tests/ltl/test_switch3_return.c b/src/plugins/aorai/tests/ltl/test_switch3_return.c index 06dbc5fbcd6602de1aa867e5c19d10440548251b..9723ebe712b6c06db4fdb2dec6f5e0f157446c18 100644 --- a/src/plugins/aorai/tests/ltl/test_switch3_return.c +++ b/src/plugins/aorai/tests/ltl/test_switch3_return.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl %{dep:@PTEST_DIR@/test_switch3.ltl} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-ltl %{dep:@PTEST_DIR@/test_switch3.ltl} -aorai-acceptance */ /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */ diff --git a/src/plugins/aorai/tests/ya/aorai_ptr_field.i b/src/plugins/aorai/tests/ya/aorai_ptr_field.i index 6d48d76cff3d1a9322c5639f04b27776a24fd456..5db8ef5186c7250e985d3ad7134bb65cb88011e9 100644 --- a/src/plugins/aorai/tests/ya/aorai_ptr_field.i +++ b/src/plugins/aorai/tests/ya/aorai_ptr_field.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ struct S { int x; }; diff --git a/src/plugins/aorai/tests/ya/assigns.c b/src/plugins/aorai/tests/ya/assigns.c index 40f4cb8e76945fe8ddd102ae7d48d632990f4218..0bc1220eb21241cc334d597b56bebfec1435d140 100644 --- a/src/plugins/aorai/tests/ya/assigns.c +++ b/src/plugins/aorai/tests/ya/assigns.c @@ -1,6 +1,6 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ - OPT: -aorai-automata %{dep:@PTEST_DIR@/assigns_det.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/assigns_det.ya} MODULE: name_projects LIBS: OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -then -print diff --git a/src/plugins/aorai/tests/ya/bts1289.i b/src/plugins/aorai/tests/ya/bts1289.i index 9b018dd840ebb0ffa9fdde3eeb3befeed4408b5b..e80a9c5f728075ecdc3f8be68101f684b795783f 100644 --- a/src/plugins/aorai/tests/ya/bts1289.i +++ b/src/plugins/aorai/tests/ya/bts1289.i @@ -1,6 +1,6 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@-2.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@-2.ya} */ void a(void) {} diff --git a/src/plugins/aorai/tests/ya/declared_function.i b/src/plugins/aorai/tests/ya/declared_function.i index 2cd6b702ca4e74c7d101bb1d6320639bed89482f..7a1e3bdfc83fa2e9b4f88cfb14d97dde3871e527 100644 --- a/src/plugins/aorai/tests/ya/declared_function.i +++ b/src/plugins/aorai/tests/ya/declared_function.i @@ -1,5 +1,5 @@ /* run.config* -OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ int f(void); diff --git a/src/plugins/aorai/tests/ya/deterministic.i b/src/plugins/aorai/tests/ya/deterministic.i index 91db6c9ba342ceea82dbc1e1a66bfd3e9690a1c7..b211e6f5d4b008f5928112d9329f00f88ac8737f 100644 --- a/src/plugins/aorai/tests/ya/deterministic.i +++ b/src/plugins/aorai/tests/ya/deterministic.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ int X; diff --git a/src/plugins/aorai/tests/ya/formals.i b/src/plugins/aorai/tests/ya/formals.i index 7cd6e26c65e12719a3ddd1dfe4e8e1370369d4a7..9e2c8f1f54ed3bab747152078d60e989eab2116a 100644 --- a/src/plugins/aorai/tests/ya/formals.i +++ b/src/plugins/aorai/tests/ya/formals.i @@ -1,5 +1,5 @@ /* run.config* -OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ int f(int x) { return x; } diff --git a/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i b/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i index cd8ec32a8440120cc27fc69d41712bdcd4f0eb97..1c1f969ec371d340126ee968038d24a450bb8937 100644 --- a/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i +++ b/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ void main(void) { diff --git a/src/plugins/aorai/tests/ya/hoare_seq.i b/src/plugins/aorai/tests/ya/hoare_seq.i index 213f469ea1acaaf6c6478d4b987feec89a919cd0..4004035e243dfd8bb1bb29ec8f26d3b8ecb9a10c 100644 --- a/src/plugins/aorai/tests/ya/hoare_seq.i +++ b/src/plugins/aorai/tests/ya/hoare_seq.i @@ -1,5 +1,5 @@ /* run.config* -OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance */ void f(void) { } diff --git a/src/plugins/aorai/tests/ya/incorrect.i b/src/plugins/aorai/tests/ya/incorrect.i index fad205dde2be66a2dbfddee5473ba46dd140ff87..a301da7b70e16c0c23566cbb0d5fceb7b17ea44f 100644 --- a/src/plugins/aorai/tests/ya/incorrect.i +++ b/src/plugins/aorai/tests/ya/incorrect.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ int f(void); diff --git a/src/plugins/aorai/tests/ya/logical_operators.i b/src/plugins/aorai/tests/ya/logical_operators.i index e70aa15ac821e50fdee3bfb33d49684350c735a2..7ea6dc39a863fcd567c2e7bc7e5112e1ea272f0d 100644 --- a/src/plugins/aorai/tests/ya/logical_operators.i +++ b/src/plugins/aorai/tests/ya/logical_operators.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ void f(int x) {} diff --git a/src/plugins/aorai/tests/ya/loop_bts1050.i b/src/plugins/aorai/tests/ya/loop_bts1050.i index 7ee8431f8e46826c223b7f9df8c60ae7dc81a2a1..b47c0974753351cddb17fcd4b0a669cfea3e02f9 100644 --- a/src/plugins/aorai/tests/ya/loop_bts1050.i +++ b/src/plugins/aorai/tests/ya/loop_bts1050.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance */ void f(){}; diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.i b/src/plugins/aorai/tests/ya/metavariables-incompatible.i index 0654e388f0d77060f17d6a6a69c47d20383e9744..907ea985b9cf115b5b2d57d0381f51158390f7fd 100644 --- a/src/plugins/aorai/tests/ya/metavariables-incompatible.i +++ b/src/plugins/aorai/tests/ya/metavariables-incompatible.i @@ -1,5 +1,5 @@ /* run.config* EXIT: 1 - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ void main(void) {} diff --git a/src/plugins/aorai/tests/ya/metavariables-right.i b/src/plugins/aorai/tests/ya/metavariables-right.i index 2d51676f37c310c85389194d485329208781f581..3891653355a949e580d8bc868c965825d42c1070 100644 --- a/src/plugins/aorai/tests/ya/metavariables-right.i +++ b/src/plugins/aorai/tests/ya/metavariables-right.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ void f(int x) {} diff --git a/src/plugins/aorai/tests/ya/metavariables-wrong.i b/src/plugins/aorai/tests/ya/metavariables-wrong.i index 86c3fea665572e8e103d04f2e91bdcb1474b0dd8..130102d4f1b2e6e702040a952c0706b8aae48f17 100644 --- a/src/plugins/aorai/tests/ya/metavariables-wrong.i +++ b/src/plugins/aorai/tests/ya/metavariables-wrong.i @@ -1,6 +1,6 @@ /* run.config* EXIT: 1 - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ void f(int x) {} void g(void) {} diff --git a/src/plugins/aorai/tests/ya/monostate.i b/src/plugins/aorai/tests/ya/monostate.i index 306c7473dc11a52b88dabe8fcbb6d5607c4448a3..8dc7942ca00320782a2a538046c04b9ea117d02b 100644 --- a/src/plugins/aorai/tests/ya/monostate.i +++ b/src/plugins/aorai/tests/ya/monostate.i @@ -1,7 +1,9 @@ /* run.config -OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} +*/ +/* run.config_prove + DONTRUN: */ - void f(void) {} void main(void) { diff --git a/src/plugins/aorai/tests/ya/not_prm.i b/src/plugins/aorai/tests/ya/not_prm.i index e633a78721bae2a0234a8b38fc944165afdda96d..edd20eb2a8a7ac1e5691e45976936831735cd306 100644 --- a/src/plugins/aorai/tests/ya/not_prm.i +++ b/src/plugins/aorai/tests/ya/not_prm.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -main f -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -main f */ int f(int x) { diff --git a/src/plugins/aorai/tests/ya/observed.i b/src/plugins/aorai/tests/ya/observed.i index 0e289248335e13dc700fdd49bd628a8b7b5d295f..9eb7db20d8483282f65eb5923057e9982125dcc3 100644 --- a/src/plugins/aorai/tests/ya/observed.i +++ b/src/plugins/aorai/tests/ya/observed.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ void f(void) {} diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle index 071567fcd96ef48b2762990dd8b3853fcef9d103..a9b448b9b7ec3c488447c1a870cb38e485d0947e 100644 --- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle @@ -1,6 +1,6 @@ [kernel] Parsing monostate.i (no preprocessing) [aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead -[aorai] monostate.i:8: Warning: +[aorai] monostate.i:10: Warning: Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path [kernel] Parsing TMPDIR/aorai_monostate_0.i (no preprocessing) /* Generated by Frama-C */ diff --git a/src/plugins/aorai/tests/ya/oracle_prove/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/monostate.res.oracle deleted file mode 100644 index da8b11c285cb1df1c13f47ad5865cd36256ed01a..0000000000000000000000000000000000000000 --- a/src/plugins/aorai/tests/ya/oracle_prove/monostate.res.oracle +++ /dev/null @@ -1 +0,0 @@ -[kernel] Parsing monostate.i (no preprocessing) diff --git a/src/plugins/aorai/tests/ya/other.c b/src/plugins/aorai/tests/ya/other.c index 8362960d7563ce2ed5566a52ec3278bdfb20d262..c4b00e283bbfd259fc7f6f80739f81ce119b21d7 100644 --- a/src/plugins/aorai/tests/ya/other.c +++ b/src/plugins/aorai/tests/ya/other.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance */ int x=0; diff --git a/src/plugins/aorai/tests/ya/seq.i b/src/plugins/aorai/tests/ya/seq.i index 24ad34ad46684603c1efdfc844515d42debd44a4..12ca5498910bd6c6fc0745c18a6c9067a4440855 100644 --- a/src/plugins/aorai/tests/ya/seq.i +++ b/src/plugins/aorai/tests/ya/seq.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance */ void f() { } diff --git a/src/plugins/aorai/tests/ya/seq_loop.i b/src/plugins/aorai/tests/ya/seq_loop.i index 7c6dd8e7f027bbb113ddab4b4c7dd829904cd555..0dffe8e0a154e9f11af5bbbd87ef16305c3230e0 100644 --- a/src/plugins/aorai/tests/ya/seq_loop.i +++ b/src/plugins/aorai/tests/ya/seq_loop.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance */ void f() {} diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c index 52bdcce277f31da80de99ac0ce33ba67734364b1..0c4d68c1b552fbead932965cf4fe801f323973d4 100644 --- a/src/plugins/aorai/tests/ya/serial.c +++ b/src/plugins/aorai/tests/ya/serial.c @@ -1,8 +1,8 @@ /* run.config - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-smoke-tests -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256 + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-smoke-tests -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256 */ /* run.config_prove -OPT: -cpp-extra-args="-DFOR_WP" -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@_wp.ya} -aorai-smoke-tests -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ -aorai-no-acceptance @PROVE_OPTIONS@ + STDOPT: -cpp-extra-args="-DFOR_WP" -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@_wp.ya} -aorai-smoke-tests -aorai-no-acceptance */ #include "__fc_builtin.h" diff --git a/src/plugins/aorai/tests/ya/single_call.i b/src/plugins/aorai/tests/ya/single_call.i index cf46f34cf511be0300f8485c9b997fdfd282dcb3..a2bb07b69cccdf40627b6c01809d8302e7dc3982 100644 --- a/src/plugins/aorai/tests/ya/single_call.i +++ b/src/plugins/aorai/tests/ya/single_call.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance */ int main () {} diff --git a/src/plugins/aorai/tests/ya/singleassignment-right.i b/src/plugins/aorai/tests/ya/singleassignment-right.i index 049a066fa4a53e6ee736731e8844445127eb1c3c..cf4738658c4d27818e96152907806060cf23d767 100644 --- a/src/plugins/aorai/tests/ya/singleassignment-right.i +++ b/src/plugins/aorai/tests/ya/singleassignment-right.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ void main(int *x, int *y) diff --git a/src/plugins/aorai/tests/ya/singleassignment-wrong.i b/src/plugins/aorai/tests/ya/singleassignment-wrong.i index 945ecd965c27ee7fbe4481867f39bf2ed93af29d..15a2e8499e9c2eb062d6de93a95ee7dae9abfe20 100644 --- a/src/plugins/aorai/tests/ya/singleassignment-wrong.i +++ b/src/plugins/aorai/tests/ya/singleassignment-wrong.i @@ -1,6 +1,6 @@ /* run.config* EXIT: 1 - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ int main(int x) { diff --git a/src/plugins/aorai/tests/ya/stack.i b/src/plugins/aorai/tests/ya/stack.i index 1e54c03921d948971878f9204d9b22cb4bb02054..5be9fa31d9f97cbb71a4730cf14e363a93141872 100644 --- a/src/plugins/aorai/tests/ya/stack.i +++ b/src/plugins/aorai/tests/ya/stack.i @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ diff --git a/src/plugins/aorai/tests/ya/test_acces_params.c b/src/plugins/aorai/tests/ya/test_acces_params.c index cf25d86e35dc068e4c801de1c5a65730268bb61f..3fdd7931639abaa45c59f4b6448f44de334ce7b2 100644 --- a/src/plugins/aorai/tests/ya/test_acces_params.c +++ b/src/plugins/aorai/tests/ya/test_acces_params.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ int status=0; diff --git a/src/plugins/aorai/tests/ya/test_acces_params2.c b/src/plugins/aorai/tests/ya/test_acces_params2.c index 220cfe50c1eec403cbd72b214b4d6580d8adfd64..eabaf7fb492b1700eae08c0ecffb5d7ae127f85d 100644 --- a/src/plugins/aorai/tests/ya/test_acces_params2.c +++ b/src/plugins/aorai/tests/ya/test_acces_params2.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ diff --git a/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c b/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c index 3adf3ad465a27d19e498b17dc82bd8710cd31fb4..08d0662bd83312b12878a2e7e76724eadabca2f2 100644 --- a/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c +++ b/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance */ diff --git a/src/plugins/aorai/tests/ya/test_factorial.c b/src/plugins/aorai/tests/ya/test_factorial.c index a132cdd62ddc2de84a3257fd7e186e7f13c31e0f..5b7b93b28555091f6745711827f3e3e10542137a 100644 --- a/src/plugins/aorai/tests/ya/test_factorial.c +++ b/src/plugins/aorai/tests/ya/test_factorial.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} */ diff --git a/src/plugins/aorai/tests/ya/test_recursion4.c b/src/plugins/aorai/tests/ya/test_recursion4.c index d07f4ba8ce6f6f36ffc103bf9c96f6b6c9636d4e..41119f495f30894fc53a67bbb0e92c0b61f8d447 100644 --- a/src/plugins/aorai/tests/ya/test_recursion4.c +++ b/src/plugins/aorai/tests/ya/test_recursion4.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance */ # pragma JessieIntegerModel(math) diff --git a/src/plugins/aorai/tests/ya/test_recursion5.c b/src/plugins/aorai/tests/ya/test_recursion5.c index f8eb2402586c7093fe9a87bafe08506f55995e08..3aae3fc01b7547c9351b5f92e98823c01780fa5e 100644 --- a/src/plugins/aorai/tests/ya/test_recursion5.c +++ b/src/plugins/aorai/tests/ya/test_recursion5.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance */ diff --git a/src/plugins/aorai/tests/ya/test_struct.c b/src/plugins/aorai/tests/ya/test_struct.c index 4566f8296cc71900c3ce3d487970f7c493c4b1a1..18e24febebca0d44e7e3a77cd8bb823ae990260a 100644 --- a/src/plugins/aorai/tests/ya/test_struct.c +++ b/src/plugins/aorai/tests/ya/test_struct.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@ + STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance */ struct People{