From 1afa30d6925f8e27f36c2d1fa639705252169d8c Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 9 Mar 2021 16:35:57 +0100
Subject: [PATCH] [tests] oracles
---
.../tests/dive/oracle/callstack_global.dot | 2 +-
src/plugins/dive/tests/dive/oracle/global.dot | 2 +-
.../dive/tests/dive/oracle/various.dot | 2 +-
.../tests/report/oracle/classified.0.json | 4 +--
.../tests/report/oracle/classified.1.json | 2 +-
.../tests/report/oracle/classified.2.json | 2 +-
.../tests/report/oracle/classified.3.json | 5 ++--
.../tests/report/oracle/classified.4.json | 5 ++--
.../tests/report/oracle/classified.5.json | 12 ++++----
.../report/tests/report/oracle/csv.csv | 30 +++++++++----------
.../tests/batch/oracle/ast_services.out.json | 14 +++++----
"tests/syntax/foo\".c" | 3 ++
12 files changed, 42 insertions(+), 41 deletions(-)
diff --git a/src/plugins/dive/tests/dive/oracle/callstack_global.dot b/src/plugins/dive/tests/dive/oracle/callstack_global.dot
index 82c7a0b0fc6..620122edbd9 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 262b981a163..de476dbaf1e 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 201055d7fc3..05b0be0fcfa 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 e9c382db69c..0b0797c4a4f 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 27e60abed79..22ee69b9525 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 27e60abed79..22ee69b9525 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 8af0cb6a445..9936adf6978 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 8af0cb6a445..9936adf6978 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 81e4ec8552e..ea5b7db447a 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 445f2843ae3..565c7fef1e6 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 a6223032cf2..5566157ce6a 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 5933f9603a0..51ab7db0365 100644
--- "a/tests/syntax/foo\".c"
+++ "b/tests/syntax/foo\".c"
@@ -1,3 +1,6 @@
+/* run.config*
+DONTRUN:
+*/
#include "assert.h"
int test = 1;
--
GitLab