diff --git a/src/plugins/dive/tests/dive/oracle/callstack_global.dot b/src/plugins/dive/tests/dive/oracle/callstack_global.dot index 82c7a0b0fc6e13df782c630cc9d6619869705d5d..620122edbd9a85a3fb5d89aa19bd43adf4209815 100644 --- a/src/plugins/dive/tests/dive/oracle/callstack_global.dot +++ b/src/plugins/dive/tests/dive/oracle/callstack_global.dot @@ -25,7 +25,7 @@ digraph G { }; subgraph cluster_cs_4 { label=<f>; cp15; }; - subgraph cluster_file_1 { label=<tests/dive/callstack_global.i>; cp11; + subgraph cluster_file_1 { label=<callstack_global.i>; cp11; }; cp3 -> cp2; diff --git a/src/plugins/dive/tests/dive/oracle/global.dot b/src/plugins/dive/tests/dive/oracle/global.dot index 262b981a163556c90c69875c2752a5674fe1ec59..de476dbaf1ee931794d2fb600ed7bc857b708e9f 100644 --- a/src/plugins/dive/tests/dive/oracle/global.dot +++ b/src/plugins/dive/tests/dive/oracle/global.dot @@ -9,7 +9,7 @@ digraph G { subgraph cluster_cs_1 { label=<main>; cp7;cp5;cp2; }; - subgraph cluster_file_1 { label=<tests/dive/global.i>; cp3; + subgraph cluster_file_1 { label=<global.i>; cp3; }; cp3 -> cp2; diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot index 201055d7fc3af13c2e9d636048862cdf0ff83857..05b0be0fcfa9da5123f8b40b78b5043936d96534 100644 --- a/src/plugins/dive/tests/dive/oracle/various.dot +++ b/src/plugins/dive/tests/dive/oracle/various.dot @@ -40,7 +40,7 @@ digraph G { subgraph cluster_cs_4 { label=<f>; cp31;cp25; }; }; - subgraph cluster_file_1 { label=<tests/dive/various.i>; cp28;cp8; + subgraph cluster_file_1 { label=<various.i>; cp28;cp8; }; cp2 -> cp5; diff --git a/src/plugins/report/tests/report/oracle/classified.0.json b/src/plugins/report/tests/report/oracle/classified.0.json index e9c382db69c473058f1aa9cf59aeb11173d6b2a8..0b0797c4a4f38245176eb06600a8877270e28dcb 100644 --- a/src/plugins/report/tests/report/oracle/classified.0.json +++ b/src/plugins/report/tests/report/oracle/classified.0.json @@ -1,5 +1,5 @@ [ { "classid": "unclassified.untried", "action": "REVIEW", - "title": "f_requires", "descr": "Untried status", - "file": "tests/report/classify.c", "line": 22 } + "title": "f_requires", "descr": "Untried status", "file": "classify.c", + "line": 22 } ] diff --git a/src/plugins/report/tests/report/oracle/classified.1.json b/src/plugins/report/tests/report/oracle/classified.1.json index 27e60abed79c035bb078fbee24c576854802ce37..22ee69b9525922ac6287581dd3a304209b889f7a 100644 --- a/src/plugins/report/tests/report/oracle/classified.1.json +++ b/src/plugins/report/tests/report/oracle/classified.1.json @@ -2,7 +2,7 @@ { "classid": "kernel.unclassified.warning", "action": "ERROR", "title": "Unclassified Warning (Plugin 'kernel')", "descr": "unbound logic variable ignored. Ignoring code annotation", - "file": "tests/report/classify.c", "line": 27 }, + "file": "classify.c", "line": 27 }, { "classid": "wp.unclassified.warning", "action": "ERROR", "title": "Unclassified Warning (Plugin 'wp')", "descr": "Missing RTE guards" } diff --git a/src/plugins/report/tests/report/oracle/classified.2.json b/src/plugins/report/tests/report/oracle/classified.2.json index 27e60abed79c035bb078fbee24c576854802ce37..22ee69b9525922ac6287581dd3a304209b889f7a 100644 --- a/src/plugins/report/tests/report/oracle/classified.2.json +++ b/src/plugins/report/tests/report/oracle/classified.2.json @@ -2,7 +2,7 @@ { "classid": "kernel.unclassified.warning", "action": "ERROR", "title": "Unclassified Warning (Plugin 'kernel')", "descr": "unbound logic variable ignored. Ignoring code annotation", - "file": "tests/report/classify.c", "line": 27 }, + "file": "classify.c", "line": 27 }, { "classid": "wp.unclassified.warning", "action": "ERROR", "title": "Unclassified Warning (Plugin 'wp')", "descr": "Missing RTE guards" } diff --git a/src/plugins/report/tests/report/oracle/classified.3.json b/src/plugins/report/tests/report/oracle/classified.3.json index 8af0cb6a445af179fe0b8d2d4d521890f12c81b4..9936adf6978a76a575e77864262251f41054e7f8 100644 --- a/src/plugins/report/tests/report/oracle/classified.3.json +++ b/src/plugins/report/tests/report/oracle/classified.3.json @@ -1,10 +1,9 @@ [ { "classid": "Parsing", "action": "ERROR", "title": "", "descr": "unbound logic variable ignored. Ignoring code annotation", - "file": "tests/report/classify.c", "line": 27 }, + "file": "classify.c", "line": 27 }, { "classid": "RTE", "action": "REVIEW", "title": "Missing RTE guards", "descr": "Shall run Eva plug-in" }, { "classid": "UNIT", "action": "INFO", "title": "Precondition 'f'", - "descr": "Property Untried", "file": "tests/report/classify.c", - "line": 22 } + "descr": "Property Untried", "file": "classify.c", "line": 22 } ] diff --git a/src/plugins/report/tests/report/oracle/classified.4.json b/src/plugins/report/tests/report/oracle/classified.4.json index 8af0cb6a445af179fe0b8d2d4d521890f12c81b4..9936adf6978a76a575e77864262251f41054e7f8 100644 --- a/src/plugins/report/tests/report/oracle/classified.4.json +++ b/src/plugins/report/tests/report/oracle/classified.4.json @@ -1,10 +1,9 @@ [ { "classid": "Parsing", "action": "ERROR", "title": "", "descr": "unbound logic variable ignored. Ignoring code annotation", - "file": "tests/report/classify.c", "line": 27 }, + "file": "classify.c", "line": 27 }, { "classid": "RTE", "action": "REVIEW", "title": "Missing RTE guards", "descr": "Shall run Eva plug-in" }, { "classid": "UNIT", "action": "INFO", "title": "Precondition 'f'", - "descr": "Property Untried", "file": "tests/report/classify.c", - "line": 22 } + "descr": "Property Untried", "file": "classify.c", "line": 22 } ] diff --git a/src/plugins/report/tests/report/oracle/classified.5.json b/src/plugins/report/tests/report/oracle/classified.5.json index 81e4ec8552e5d75bd10bd115b7ece07d6b619e37..ea5b7db447ae5295c3aab003c2be32f12a479895 100644 --- a/src/plugins/report/tests/report/oracle/classified.5.json +++ b/src/plugins/report/tests/report/oracle/classified.5.json @@ -1,16 +1,14 @@ [ { "classid": "Parsing", "action": "ERROR", "title": "", "descr": "unbound logic variable ignored. Ignoring code annotation", - "file": "tests/report/classify.c", "line": 27 }, + "file": "classify.c", "line": 27 }, { "classid": "RTE", "action": "REVIEW", "title": "Missing RTE guards", "descr": "Shall run Eva plug-in" }, { "classid": "UNIT", "action": "INFO", "title": "Precondition 'f'", - "descr": "Property Untried", "file": "tests/report/classify.c", - "line": 22 }, + "descr": "Property Untried", "file": "classify.c", "line": 22 }, { "classid": "GOAL", "action": "ERROR", "title": "Postcondition 'f'", - "descr": "Property Untried", "file": "tests/report/classify.c", - "line": 23 }, + "descr": "Property Untried", "file": "classify.c", "line": 23 }, { "classid": "unclassified.untried", "action": "REVIEW", - "title": "f_assigns", "descr": "Untried status", - "file": "tests/report/classify.c", "line": 24 } + "title": "f_assigns", "descr": "Untried status", "file": "classify.c", + "line": 24 } ] diff --git a/src/plugins/report/tests/report/oracle/csv.csv b/src/plugins/report/tests/report/oracle/csv.csv index 445f2843ae3c712b2b47065c1d72f36a0c2d9ec8..565c7fef1e69e20c273a322707f1eb1662a107fc 100644 --- a/src/plugins/report/tests/report/oracle/csv.csv +++ b/src/plugins/report/tests/report/oracle/csv.csv @@ -1,17 +1,17 @@ directory file line function property kind status property +. csv.c 11 main1 signed_overflow Unknown -2147483648 ≤ x * x +. csv.c 11 main1 signed_overflow Unknown x * x ≤ 2147483647 +. csv.c 12 main1 index_bound Unknown 0 ≤ x +. csv.c 12 main1 index_bound Unknown x < 15 +. csv.c 13 main1 initialization Unknown \initialized(&u[x]) +. csv.c 17 f precondition Unknown x ≥ 1 +. csv.c 18 f assigns clause Unknown assigns \nothing; +. csv.c 18 f from clause Unknown assigns \result \from x; +. csv.c 21 main2 precondition of f Unknown x ≥ 1 +. csv.c 22 main2 precondition of f Unknown x ≥ 1 +. csv.c 23 main2 precondition of f Unknown x ≥ 1 +. csv.c 33 main3 precondition of pow Unknown finite_logic_res: \is_finite(pow(x, y)) +. csv.c 37 __FC_assert precondition Invalid or unreachable \false +. csv.c 50 main4 is_nan_or_infinite Unknown \is_finite(d) +. csv.c 50 main4 precondition of __FC_assert Invalid or unreachable \false FRAMAC_SHARE/libc math.h 478 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y)) -tests/report csv.c 11 main1 signed_overflow Unknown -2147483648 ≤ x * x -tests/report csv.c 11 main1 signed_overflow Unknown x * x ≤ 2147483647 -tests/report csv.c 12 main1 index_bound Unknown 0 ≤ x -tests/report csv.c 12 main1 index_bound Unknown x < 15 -tests/report csv.c 13 main1 initialization Unknown \initialized(&u[x]) -tests/report csv.c 17 f precondition Unknown x ≥ 1 -tests/report csv.c 18 f assigns clause Unknown assigns \nothing; -tests/report csv.c 18 f from clause Unknown assigns \result \from x; -tests/report csv.c 21 main2 precondition of f Unknown x ≥ 1 -tests/report csv.c 22 main2 precondition of f Unknown x ≥ 1 -tests/report csv.c 23 main2 precondition of f Unknown x ≥ 1 -tests/report csv.c 33 main3 precondition of pow Unknown finite_logic_res: \is_finite(pow(x, y)) -tests/report csv.c 37 __FC_assert precondition Invalid or unreachable \false -tests/report csv.c 50 main4 is_nan_or_infinite Unknown \is_finite(d) -tests/report csv.c 50 main4 precondition of __FC_assert Invalid or unreachable \false diff --git a/src/plugins/server/tests/batch/oracle/ast_services.out.json b/src/plugins/server/tests/batch/oracle/ast_services.out.json index a6223032cf20850343a7d0270679a14b24daee0b..5566157ce6a5d4254502135784dd3fec57e1ea0f 100644 --- a/src/plugins/server/tests/batch/oracle/ast_services.out.json +++ b/src/plugins/server/tests/batch/oracle/ast_services.out.json @@ -9,10 +9,11 @@ "signature": "int g(int y);", "defined": true, "sloc": { - "dir": "tests/batch", + "dir": ".", "base": "ast_services.i", - "file": "tests/batch/ast_services.i", - "line": 2 + "file": + "/home/pb122476/export-local/frama-c/dune-frama-c/trunk/_build/default/src/plugins/server/tests/batch/result/ast_services.i", + "line": 8 } }, { @@ -21,10 +22,11 @@ "signature": "int f(int x);", "defined": true, "sloc": { - "dir": "tests/batch", + "dir": ".", "base": "ast_services.i", - "file": "tests/batch/ast_services.i", - "line": 1 + "file": + "/home/pb122476/export-local/frama-c/dune-frama-c/trunk/_build/default/src/plugins/server/tests/batch/result/ast_services.i", + "line": 7 } } ], diff --git "a/tests/syntax/foo\".c" "b/tests/syntax/foo\".c" index 5933f9603a0e136d34c0680af6714d936839eaa5..51ab7db036515eb4dff56be6116636cdf2137280 100644 --- "a/tests/syntax/foo\".c" +++ "b/tests/syntax/foo\".c" @@ -1,3 +1,6 @@ +/* run.config* +DONTRUN: +*/ #include "assert.h" int test = 1;