[tests] oracles

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;

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;

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;

src/plugins/report/tests/report/oracle/classified.0.json

 [
   { "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 }
 ]

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" }

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" }

src/plugins/report/tests/report/oracle/classified.3.json

 [
   { "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 }
 ]

src/plugins/report/tests/report/oracle/classified.4.json

 [
   { "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 }
 ]

src/plugins/report/tests/report/oracle/classified.5.json

 [
   { "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 }
 ]

src/plugins/report/tests/report/oracle/csv.csv

 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

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
           }
         }
       ],

tests/syntax/foo".c

+/* run.config*
+DONTRUN:
+*/
 #include "assert.h"
 
 int test = 1;