diff --git a/tests/pp/baddirective.cpp b/tests/pp/baddirective.cpp index ff95b992908cd0f963f37dfe77aa198023d185b0..cb8ecacedc519e3dbe9d02dd08eff78f74e9b242 100644 --- a/tests/pp/baddirective.cpp +++ b/tests/pp/baddirective.cpp @@ -1,4 +1,10 @@ +/* run.config* +EXIT: 1 +STDOPT: +*/ + // Tests a misspelled directive + /*@ requires \true; diff --git a/tests/pp/baddirective2.cpp b/tests/pp/baddirective2.cpp index 65625a90220d51c79f05f2501715c58c42a87dc9..8fed753b831a5e2f425cbf5a48fbed83cece9a5b 100644 --- a/tests/pp/baddirective2.cpp +++ b/tests/pp/baddirective2.cpp @@ -1,3 +1,8 @@ +/* run.config* +EXIT: 1 +STDOPT: +*/ + // Tests a misspelled directive /*@ diff --git a/tests/pp/comment.cpp b/tests/pp/comment.cpp index 59894832d30f5bdba3a56541f6abecb32e75138c..85055240bb817203e5cd3ef02774481cd260d186 100644 --- a/tests/pp/comment.cpp +++ b/tests/pp/comment.cpp @@ -1,3 +1,7 @@ +/* run.config* +EXIT: 1 +STDOPT: +*/ // Tests a directive that just has a comment /*@ diff --git a/tests/pp/define.cpp b/tests/pp/define.cpp index e8f0f1ebe4320c025e89aef8ba2ab9e64c1e0227..5254ee48620d1fdb757be447536f7c12c22b3f41 100644 --- a/tests/pp/define.cpp +++ b/tests/pp/define.cpp @@ -1,3 +1,8 @@ +/* run.config* +EXIT: 1 +STDOPT: +*/ + // Tests whether define directive is properly reported /*@ diff --git a/tests/pp/define2.cpp b/tests/pp/define2.cpp index ce554e9682e3c86aa8acbcdb83cee68369ce360f..7ec49ba66340928659274c4f01806d3b7e1bee5c 100644 --- a/tests/pp/define2.cpp +++ b/tests/pp/define2.cpp @@ -1,3 +1,8 @@ +/* run.config +EXIT: 1 +STDOPT: +*/ + // Tests whether define directive is properly reported /*@ diff --git a/tests/pp/empty.cpp b/tests/pp/empty.cpp index d295e211b2f570110198e961562607bbbff82122..5f07b7121d73960fc149357f67e7fb8e9f1ba1bc 100644 --- a/tests/pp/empty.cpp +++ b/tests/pp/empty.cpp @@ -1,3 +1,7 @@ +/* run.config* +EXIT: 1 +STDOPT: +*/ // Tests an empty directive /*@ diff --git a/tests/pp/empty2.cpp b/tests/pp/empty2.cpp index c8561e0b76a7a1c15c0a5bab58f56f02c0966239..570db21a3385992586eecdeb8c8100b1bb12f599 100644 --- a/tests/pp/empty2.cpp +++ b/tests/pp/empty2.cpp @@ -1,3 +1,7 @@ +/* run.config* +EXIT:1 +STDOPT: +*/ // Tests an empty directive /*@ diff --git a/tests/pp/empty3.cpp b/tests/pp/empty3.cpp index 5d88de48071a41edc55398bccae9c93b5a60440d..c31b34310567fbbf01d0bdb7fbbc0724685cc6a7 100644 --- a/tests/pp/empty3.cpp +++ b/tests/pp/empty3.cpp @@ -1,3 +1,7 @@ +/* run.config* +EXIT: 1 +STDOPT: +*/ // Tests an empty directive at end of line //@ # void m() {} diff --git a/tests/pp/oracle/baddirective.err.oracle b/tests/pp/oracle/baddirective.err.oracle index 4b3a771e6256421ca1f32fe16457009a85828f26..fc23daa149debff813a59919278d6eda1be78236 100644 --- a/tests/pp/oracle/baddirective.err.oracle +++ b/tests/pp/oracle/baddirective.err.oracle @@ -1,4 +1,4 @@ -tests/pp/baddirective.cpp:5:5: error: [pp] Invalid preprocessor directive [zzzzz] (ignoring line): # zzzzz "Failure2" +tests/pp/baddirective.cpp:11:5: error: [pp] Invalid preprocessor directive [zzzzz] (ignoring line): # zzzzz "Failure2" # zzzzz "Failure2" ^ code generation aborted due to one compilation error diff --git a/tests/pp/oracle/baddirective2.err.oracle b/tests/pp/oracle/baddirective2.err.oracle index b2e60058555c6cb2180c495efcae7eb8ef63237a..03f4f4a151ffc4934764cf5453b084ddf57ccf22 100644 --- a/tests/pp/oracle/baddirective2.err.oracle +++ b/tests/pp/oracle/baddirective2.err.oracle @@ -1,4 +1,4 @@ -tests/pp/baddirective2.cpp:5:2: error: [pp] Invalid preprocessor directive [zzzzz] (ignoring line): #zzzzz "Failure2" +tests/pp/baddirective2.cpp:10:2: error: [pp] Invalid preprocessor directive [zzzzz] (ignoring line): #zzzzz "Failure2" #zzzzz "Failure2" ^ code generation aborted due to one compilation error diff --git a/tests/pp/oracle/comment.err.oracle b/tests/pp/oracle/comment.err.oracle index 86cc5953cb71181301e43384120e020213aee1d7..545c70b55dda4dcd9bfdeec7771dffb4286693cc 100644 --- a/tests/pp/oracle/comment.err.oracle +++ b/tests/pp/oracle/comment.err.oracle @@ -1,4 +1,4 @@ -tests/pp/comment.cpp:5:2: error: [pp] Missing preprocessor directive (ignoring line): # // asdasd +tests/pp/comment.cpp:9:2: error: [pp] Missing preprocessor directive (ignoring line): # // asdasd # // asdasd ^ code generation aborted due to one compilation error diff --git a/tests/pp/oracle/define.err.oracle b/tests/pp/oracle/define.err.oracle index ba5416c60f31a84a7804736c1aeba7b0983b7cca..66cc7e7fe778cc50c3d7f562b5655265e28b0d96 100644 --- a/tests/pp/oracle/define.err.oracle +++ b/tests/pp/oracle/define.err.oracle @@ -1,4 +1,4 @@ -tests/pp/define.cpp:5:3: error: [pp] Preprocessor directive is not permitted in ACSL++ annotation (ignoring line): # define XX 0 +tests/pp/define.cpp:10:3: error: [pp] Preprocessor directive is not permitted in ACSL++ annotation (ignoring line): # define XX 0 # define XX 0 ^ code generation aborted due to one compilation error diff --git a/tests/pp/oracle/define2.err.oracle b/tests/pp/oracle/define2.err.oracle index e5874af63a5606e1a302fb32eeef854adf2a9906..24bc9d4f53a545dc0c3712e56512e9445e831e72 100644 --- a/tests/pp/oracle/define2.err.oracle +++ b/tests/pp/oracle/define2.err.oracle @@ -1,4 +1,4 @@ -tests/pp/define2.cpp:4:3: error: [pp] Preprocessor directive is not permitted in ACSL++ annotation (ignoring line): # define XX 0 +tests/pp/define2.cpp:9:3: error: [pp] Preprocessor directive is not permitted in ACSL++ annotation (ignoring line): # define XX 0 # define XX 0 ^ code generation aborted due to one compilation error diff --git a/tests/pp/oracle/empty.err.oracle b/tests/pp/oracle/empty.err.oracle index d309dd217177142855fb03441736ca21492f4335..c229f5f2b4af27a9f8bc0cfab888be75f5ff116d 100644 --- a/tests/pp/oracle/empty.err.oracle +++ b/tests/pp/oracle/empty.err.oracle @@ -1,4 +1,4 @@ -tests/pp/empty.cpp:5:2: error: [pp] Missing preprocessor directive (ignoring line): # +tests/pp/empty.cpp:9:2: error: [pp] Missing preprocessor directive (ignoring line): # # ^ code generation aborted due to one compilation error diff --git a/tests/pp/oracle/empty2.err.oracle b/tests/pp/oracle/empty2.err.oracle index 16a90cbe0d177c1c68caf9374371c1e8c9158347..a3059a27b07def393f2db0a3a30df16c36003813 100644 --- a/tests/pp/oracle/empty2.err.oracle +++ b/tests/pp/oracle/empty2.err.oracle @@ -1,4 +1,4 @@ -tests/pp/empty2.cpp:4:2: error: [pp] Missing preprocessor directive (ignoring line): # +tests/pp/empty2.cpp:8:2: error: [pp] Missing preprocessor directive (ignoring line): # # ^ code generation aborted due to one compilation error diff --git a/tests/pp/oracle/empty3.err.oracle b/tests/pp/oracle/empty3.err.oracle index 27802de9b8a9059bee3e3fe559890f34a6003ed2..af46b3711ad593be0cdc704b5ff7a6b0518edf32 100644 --- a/tests/pp/oracle/empty3.err.oracle +++ b/tests/pp/oracle/empty3.err.oracle @@ -1,4 +1,4 @@ -tests/pp/empty3.cpp:2:6: error: [pp] Missing preprocessor directive (ignoring line): # +tests/pp/empty3.cpp:6:6: error: [pp] Missing preprocessor directive (ignoring line): # //@ # ^ code generation aborted due to one compilation error diff --git a/tests/pp/oracle/pragma.err.oracle b/tests/pp/oracle/pragma.err.oracle index 41fa7d33c67327f16b95b225b71db8c0f1e65304..64e1f3721a4b79c720638d7ac75a05d0aebbde8c 100644 --- a/tests/pp/oracle/pragma.err.oracle +++ b/tests/pp/oracle/pragma.err.oracle @@ -1,4 +1,4 @@ -tests/pp/pragma.cpp:5:6: error: [pp] Preprocessor directive is not permitted in ACSL++ annotation (ignoring line): # pragma asdasdasd +tests/pp/pragma.cpp:9:6: error: [pp] Preprocessor directive is not permitted in ACSL++ annotation (ignoring line): # pragma asdasdasd # pragma asdasdasd ^ code generation aborted due to one compilation error diff --git a/tests/pp/oracle/valid_function1.res.oracle b/tests/pp/oracle/valid_function1.res.oracle index 6f2147a624ff0bd7354c1707d73e1b8ece6ecbbf..3f0f101dcd44df9294a15f827917afd2bc351379 100644 --- a/tests/pp/oracle/valid_function1.res.oracle +++ b/tests/pp/oracle/valid_function1.res.oracle @@ -1,6 +1,6 @@ [kernel] Parsing tests/pp/valid_function1.cpp (external front-end) Now output intermediate result -[kernel:annot-error] tests/pp/valid_function1.cpp:7: Warning: +[kernel:annot-error] tests/pp/valid_function1.cpp:11: Warning: subscripted value is neither array nor pointer. Ignoring logic specification of function _Z1h [kernel] User Error: warning annot-error treated as fatal error. [kernel] User Error: stopping on file "tests/pp/valid_function1.cpp" that has errors. diff --git a/tests/pp/oracle/valid_function2.res.oracle b/tests/pp/oracle/valid_function2.res.oracle index 182aa86a95d504b95242f44c25b7e12d0b0ec9fc..0528cf17a0b590d02d14c7ca79ad903a1e9f9546 100644 --- a/tests/pp/oracle/valid_function2.res.oracle +++ b/tests/pp/oracle/valid_function2.res.oracle @@ -1,6 +1,6 @@ [kernel] Parsing tests/pp/valid_function2.cpp (external front-end) Now output intermediate result -[kernel:annot-error] tests/pp/valid_function2.cpp:7: Warning: +[kernel:annot-error] tests/pp/valid_function2.cpp:11: Warning: expecting a function pointer, found int *. Ignoring logic specification of function _Z2hh [kernel] User Error: warning annot-error treated as fatal error. [kernel] User Error: stopping on file "tests/pp/valid_function2.cpp" that has errors. diff --git a/tests/pp/pragma.cpp b/tests/pp/pragma.cpp index d3fc42bdb194afe8546b5a694137a7020865e3eb..ebbd96d24069c1239b451dc33056a16c5193242d 100644 --- a/tests/pp/pragma.cpp +++ b/tests/pp/pragma.cpp @@ -1,3 +1,7 @@ +/* run.config* +EXIT: 1 +STDOPT: +*/ // Tests whether pragma directive is properly reported /*@ diff --git a/tests/pp/valid_function1.cpp b/tests/pp/valid_function1.cpp index 8777f47166b3f2144328709da6186cfeacbe0e43..3ae13de93ad343f1c51807f674a1c889c316ca31 100644 --- a/tests/pp/valid_function1.cpp +++ b/tests/pp/valid_function1.cpp @@ -1,3 +1,7 @@ +/* run.config* +EXIT: 1 +STDOPT: +*/ void f() {} diff --git a/tests/pp/valid_function2.cpp b/tests/pp/valid_function2.cpp index 60489cc1aa9251436d2b37ff15bf96d34fca329b..326368e456cd9710dc6f3fa2ad1306ab62d6d705 100644 --- a/tests/pp/valid_function2.cpp +++ b/tests/pp/valid_function2.cpp @@ -1,3 +1,7 @@ +/* run.config* +EXIT: 1 +STDOPT: +*/ void f() {}