Skip to content
Snippets Groups Projects
Commit 57270c64 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Interpreted automata: removes unreachable vertices.

parent ea66ae9b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/kernel_services/analysis/interpreted_automata.ml
+ 21
− 0
View file @ 57270c64
......@@ -594,6 +594,27 @@ let build_automaton ~annotations kf =
in
G.iter_edges_e bind_labels g;
(* Recursively removes unreachable vertices, except those bound to a statement
in [table]. *)
let stmt_vertices =
let add _stmt (v1, v2) acc = Vertex.Set.(add v1 (add v2 acc)) in
StmtTable.fold add table Vertex.Set.empty
in
let is_unreachable vertex =
G.in_degree g vertex = 0
&& not (Vertex.equal vertex entry_point)
&& not (Vertex.Set.mem vertex stmt_vertices)
in
let rec remove_unreachable vertex =
let succs = G.succ g vertex in
G.remove_vertex g vertex;
List.iter remove_unreachable (List.filter is_unreachable succs)
in
let unreachables =
G.fold_vertex (fun v l -> if is_unreachable v then v :: l else l) g []
in
List.iter remove_unreachable unreachables;
(* Return the result *)
{graph = g; entry_point; return_point; stmt_table = table}
......
tests/misc/oracle/interpreted_automata_dataflow_backward.dot
+ 49
− 53
View file @ 57270c64
......@@ -4,77 +4,73 @@ digraph G {
cp1 [label=<x>, ];
cp2 [label=< >, ];
cp3 [label=<x>, ];
cp4 [label=< >, ];
cp4 [label=<x, y>, ];
cp5 [label=<x, y>, ];
cp6 [label=<x, y>, ];
cp7 [label=<x, y>, ];
cp8 [label=<x>, ];
cp9 [label=<x, a>, ];
cp10 [label=<x>, ];
cp11 [label=<x, a>, ];
cp12 [label=<x>, ];
cp7 [label=<x>, ];
cp8 [label=<x, a>, ];
cp9 [label=<x>, ];
cp10 [label=<x, a>, ];
cp11 [label=<x>, ];
cp12 [label=<x, a, i>, ];
cp13 [label=<x, a, i>, ];
cp14 [label=<x, a, i>, ];
cp15 [label=<x, a, i>, shape=invtriangle, ];
cp14 [label=<x, a, i>, shape=invtriangle, ];
cp15 [label=<x, a, i>, ];
cp16 [label=<x, a, i>, ];
cp17 [label=<x, a, i>, ];
cp18 [label=<x, a, i>, ];
cp18 [label=<x>, ];
cp19 [label=<x>, ];
cp20 [label=<x>, ];
cp20 [label=<x, a, i>, ];
cp21 [label=<x, a, i>, ];
cp22 [label=<x, a, i>, ];
cp23 [label=<x, a, i>, ];
cp24 [label=<x, a, i>, ];
cp25 [label=<x, a, i>, ];
cp26 [label=<x, a, i>, ];
cp25 [label=< >, ];
cp26 [label=< >, ];
cp27 [label=< >, ];
cp28 [label=< >, ];
cp29 [label=< >, ];
cp30 [label=< >, ];
cp31 [label=< >, ];
cp32 [label=< >, ];
cp31 [label=<x>, ];
cp32 [label=<x>, ];
cp33 [label=<x>, ];
cp34 [label=<x>, ];
cp35 [label=<x>, ];
subgraph cluster_1 { cp26;cp25;cp24;cp23;cp22;cp18;cp17;cp16;cp15;cp14;
subgraph cluster_1 { cp24;cp23;cp22;cp21;cp20;cp17;cp16;cp15;cp14;cp13;
};
cp1 -> cp3 [label=<Enter y, z, w, a>, ];
cp3 -> cp5 [label=<int y = 3;>, ];
cp4 -> cp2 [label=<Exit y, z, w, a>, ];
cp5 -> cp6 [label=<y *= 2;>, ];
cp6 -> cp7 [label=<int z = y + 1;>, ];
cp7 -> cp8 [label=<int w = y + x;>, ];
cp8 -> cp9 [label=<int a = 1;>, ];
cp9 -> cp11 [label=<Enter i>, ];
cp10 -> cp28 [label=<x != 3>, ];
cp10 -> cp29 [label=<!(x != 3)>, ];
cp11 -> cp13 [label=<int i = 0;>, ];
cp12 -> cp10 [label=<Exit i>, ];
cp13 -> cp14 [label=< >, ];
cp14 -> cp15 [constraint=false, label=<Enter >, ];
cp15 -> cp18 [label=<i &lt; 10>, ];
cp15 -> cp19 [label=<!(i &lt; 10)>, ];
cp16 -> cp14 [label=<Exit >, ];
cp17 -> cp23 [label=<Enter b, c>, ];
cp18 -> cp17 [label=< >, ];
cp19 -> cp20 [label=<Enter >, ];
cp20 -> cp33 [label=< >, ];
cp21 -> cp17 [label=<Exit >, ];
cp22 -> cp16 [label=<i ++;>, ];
cp23 -> cp25 [label=<int b = 3;>, ];
cp24 -> cp22 [label=<Exit b, c>, ];
cp25 -> cp26 [label=<int c = i + 1;>, ];
cp26 -> cp24 [label=<a ++;>, ];
cp27 -> cp32 [label=<return>, ];
cp28 -> cp30 [label=<Enter >, ];
cp29 -> cp27 [label=< >, ];
cp30 -> cp31 [label=<x = 3;>, ];
cp31 -> cp27 [label=<Exit >, ];
cp32 -> cp2 [label=<Exit y, z, w, a>, ];
cp33 -> cp34 [label=<Exit i>, ];
cp34 -> cp35 [label=<Exit >, ];
cp35 -> cp10 [label=<Exit >, ];
cp3 -> cp4 [label=<int y = 3;>, ];
cp4 -> cp5 [label=<y *= 2;>, ];
cp5 -> cp6 [label=<int z = y + 1;>, ];
cp6 -> cp7 [label=<int w = y + x;>, ];
cp7 -> cp8 [label=<int a = 1;>, ];
cp8 -> cp10 [label=<Enter i>, ];
cp9 -> cp26 [label=<x != 3>, ];
cp9 -> cp27 [label=<!(x != 3)>, ];
cp10 -> cp12 [label=<int i = 0;>, ];
cp11 -> cp9 [label=<Exit i>, ];
cp12 -> cp13 [label=< >, ];
cp13 -> cp14 [constraint=false, label=<Enter >, ];
cp14 -> cp17 [label=<i &lt; 10>, ];
cp14 -> cp18 [label=<!(i &lt; 10)>, ];
cp15 -> cp13 [label=<Exit >, ];
cp16 -> cp21 [label=<Enter b, c>, ];
cp17 -> cp16 [label=< >, ];
cp18 -> cp19 [label=<Enter >, ];
cp19 -> cp31 [label=< >, ];
cp20 -> cp15 [label=<i ++;>, ];
cp21 -> cp23 [label=<int b = 3;>, ];
cp22 -> cp20 [label=<Exit b, c>, ];
cp23 -> cp24 [label=<int c = i + 1;>, ];
cp24 -> cp22 [label=<a ++;>, ];
cp25 -> cp30 [label=<return>, ];
cp26 -> cp28 [label=<Enter >, ];
cp27 -> cp25 [label=< >, ];
cp28 -> cp29 [label=<x = 3;>, ];
cp29 -> cp25 [label=<Exit >, ];
cp30 -> cp2 [label=<Exit y, z, w, a>, ];
cp31 -> cp32 [label=<Exit i>, ];
cp32 -> cp33 [label=<Exit >, ];
cp33 -> cp9 [label=<Exit >, ];
}
\ No newline at end of file
tests/misc/oracle/interpreted_automata_dataflow_forward.dot
+ 54
− 58
View file @ 57270c64
......@@ -4,77 +4,73 @@ digraph G {
cp1 [label=< >, ];
cp2 [label=<x: 3<br />y: 6<br />z: 7>, ];
cp3 [label=< >, ];
cp4 [label=<⊥>, style="dashed", ];
cp5 [label=<y: 3>, ];
cp6 [label=<y: 6>, ];
cp4 [label=<y: 3>, ];
cp5 [label=<y: 6>, ];
cp6 [label=<y: 6<br />z: 7>, ];
cp7 [label=<y: 6<br />z: 7>, ];
cp8 [label=<y: 6<br />z: 7>, ];
cp9 [label=<y: 6<br />z: 7<br />a: 1>, ];
cp10 [label=<y: 6<br />z: 7>, ];
cp11 [label=<y: 6<br />z: 7<br />a: 1>, ];
cp12 [label=<⊥>, style="dashed", ];
cp13 [label=<y: 6<br />z: 7<br />a: 1<br />i: 0>, ];
cp14 [label=<y: 6<br />z: 7>, shape=invtriangle, ];
cp15 [label=<y: 6<br />z: 7>, ];
cp16 [label=<y: 6<br />z: 7<br />b: 3>, ];
cp8 [label=<y: 6<br />z: 7<br />a: 1>, ];
cp9 [label=<y: 6<br />z: 7>, ];
cp10 [label=<y: 6<br />z: 7<br />a: 1>, ];
cp11 [label=<⊥>, style="dashed", ];
cp12 [label=<y: 6<br />z: 7<br />a: 1<br />i: 0>, ];
cp13 [label=<y: 6<br />z: 7>, shape=invtriangle, ];
cp14 [label=<y: 6<br />z: 7>, ];
cp15 [label=<y: 6<br />z: 7<br />b: 3>, ];
cp16 [label=<y: 6<br />z: 7>, ];
cp17 [label=<y: 6<br />z: 7>, ];
cp18 [label=<y: 6<br />z: 7>, ];
cp19 [label=<y: 6<br />z: 7>, ];
cp20 [label=<y: 6<br />z: 7>, ];
cp21 [label=<⊥>, style="dashed", ];
cp20 [label=<y: 6<br />z: 7<br />b: 3>, ];
cp21 [label=<y: 6<br />z: 7>, ];
cp22 [label=<y: 6<br />z: 7<br />b: 3>, ];
cp23 [label=<y: 6<br />z: 7>, ];
cp23 [label=<y: 6<br />z: 7<br />b: 3>, ];
cp24 [label=<y: 6<br />z: 7<br />b: 3>, ];
cp25 [label=<y: 6<br />z: 7<br />b: 3>, ];
cp26 [label=<y: 6<br />z: 7<br />b: 3>, ];
cp25 [label=<x: 3<br />y: 6<br />z: 7>, ];
cp26 [label=<y: 6<br />z: 7>, ];
cp27 [label=<x: 3<br />y: 6<br />z: 7>, ];
cp28 [label=<y: 6<br />z: 7>, ];
cp29 [label=<x: 3<br />y: 6<br />z: 7>, ];
cp30 [label=<y: 6<br />z: 7>, ];
cp31 [label=<x: 3<br />y: 6<br />z: 7>, ];
cp32 [label=<x: 3<br />y: 6<br />z: 7>, ];
cp30 [label=<x: 3<br />y: 6<br />z: 7>, ];
cp31 [label=<y: 6<br />z: 7>, ];
cp32 [label=<y: 6<br />z: 7>, ];
cp33 [label=<y: 6<br />z: 7>, ];
cp34 [label=<y: 6<br />z: 7>, ];
cp35 [label=<y: 6<br />z: 7>, ];
subgraph cluster_1 { cp26;cp25;cp24;cp23;cp22;cp18;cp17;cp16;cp15;cp14;
subgraph cluster_1 { cp24;cp23;cp22;cp21;cp20;cp17;cp16;cp15;cp14;cp13;
};
cp1 -> cp3 [label=<Enter y, z, w, a>, ];
cp3 -> cp5 [label=<int y = 3;>, ];
cp4 -> cp2 [label=<Exit y, z, w, a>, style="dashed", ];
cp5 -> cp6 [label=<y *= 2;>, ];
cp6 -> cp7 [label=<int z = y + 1;>, ];
cp7 -> cp8 [label=<int w = y + x;>, ];
cp8 -> cp9 [label=<int a = 1;>, ];
cp9 -> cp11 [label=<Enter i>, ];
cp10 -> cp28 [label=<x != 3>, ];
cp10 -> cp29 [label=<!(x != 3)>, ];
cp11 -> cp13 [label=<int i = 0;>, ];
cp12 -> cp10 [label=<Exit i>, style="dashed", ];
cp13 -> cp14 [label=< >, ];
cp14 -> cp15 [label=<Enter >, ];
cp15 -> cp18 [label=<i &lt; 10>, ];
cp15 -> cp19 [label=<!(i &lt; 10)>, ];
cp16 -> cp14 [constraint=false, label=<Exit >, ];
cp17 -> cp23 [label=<Enter b, c>, ];
cp18 -> cp17 [label=< >, ];
cp19 -> cp20 [label=<Enter >, ];
cp20 -> cp33 [label=< >, ];
cp21 -> cp17 [label=<Exit >, style="dashed", ];
cp22 -> cp16 [label=<i ++;>, ];
cp23 -> cp25 [label=<int b = 3;>, ];
cp24 -> cp22 [label=<Exit b, c>, ];
cp25 -> cp26 [label=<int c = i + 1;>, ];
cp26 -> cp24 [label=<a ++;>, ];
cp27 -> cp32 [label=<return>, ];
cp28 -> cp30 [label=<Enter >, ];
cp29 -> cp27 [label=< >, ];
cp30 -> cp31 [label=<x = 3;>, ];
cp31 -> cp27 [label=<Exit >, ];
cp32 -> cp2 [label=<Exit y, z, w, a>, ];
cp33 -> cp34 [label=<Exit i>, ];
cp34 -> cp35 [label=<Exit >, ];
cp35 -> cp10 [label=<Exit >, ];
cp3 -> cp4 [label=<int y = 3;>, ];
cp4 -> cp5 [label=<y *= 2;>, ];
cp5 -> cp6 [label=<int z = y + 1;>, ];
cp6 -> cp7 [label=<int w = y + x;>, ];
cp7 -> cp8 [label=<int a = 1;>, ];
cp8 -> cp10 [label=<Enter i>, ];
cp9 -> cp26 [label=<x != 3>, ];
cp9 -> cp27 [label=<!(x != 3)>, ];
cp10 -> cp12 [label=<int i = 0;>, ];
cp11 -> cp9 [label=<Exit i>, style="dashed", ];
cp12 -> cp13 [label=< >, ];
cp13 -> cp14 [label=<Enter >, ];
cp14 -> cp17 [label=<i &lt; 10>, ];
cp14 -> cp18 [label=<!(i &lt; 10)>, ];
cp15 -> cp13 [constraint=false, label=<Exit >, ];
cp16 -> cp21 [label=<Enter b, c>, ];
cp17 -> cp16 [label=< >, ];
cp18 -> cp19 [label=<Enter >, ];
cp19 -> cp31 [label=< >, ];
cp20 -> cp15 [label=<i ++;>, ];
cp21 -> cp23 [label=<int b = 3;>, ];
cp22 -> cp20 [label=<Exit b, c>, ];
cp23 -> cp24 [label=<int c = i + 1;>, ];
cp24 -> cp22 [label=<a ++;>, ];
cp25 -> cp30 [label=<return>, ];
cp26 -> cp28 [label=<Enter >, ];
cp27 -> cp25 [label=< >, ];
cp28 -> cp29 [label=<x = 3;>, ];
cp29 -> cp25 [label=<Exit >, ];
cp30 -> cp2 [label=<Exit y, z, w, a>, ];
cp31 -> cp32 [label=<Exit i>, ];
cp32 -> cp33 [label=<Exit >, ];
cp33 -> cp9 [label=<Exit >, ];
}
\ No newline at end of file
tests/value/oracle/partitioning-interproc.0.res.oracle
+ 2
− 11
View file @ 57270c64
......@@ -12,9 +12,9 @@
[eva] Done for function Frama_C_nondet
[eva] Recording results for cassign
[eva] Done for function cassign
[eva:alarm] tests/value/partitioning-interproc.c:25: Warning:
accessing uninitialized left-value. assert \initialized(&x);
[eva] tests/value/partitioning-interproc.c:26: Frama_C_show_each: {1}
[eva] tests/value/partitioning-interproc.c:30:
Reusing old results for call to cassign
[eva] computing for function cassign <- cassign_test.
Called from tests/value/partitioning-interproc.c:30.
[eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
......@@ -22,15 +22,6 @@
[eva] Done for function Frama_C_nondet
[eva] Recording results for cassign
[eva] Done for function cassign
[eva] computing for function cassign <- cassign_test.
Called from tests/value/partitioning-interproc.c:30.
[eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
Called from tests/value/partitioning-interproc.c:11.
[eva] Done for function Frama_C_nondet
[eva] Recording results for cassign
[eva] Done for function cassign
[eva:alarm] tests/value/partitioning-interproc.c:31: Warning:
accessing uninitialized left-value. assert \initialized(&x);
[eva] tests/value/partitioning-interproc.c:32: Frama_C_show_each: {1}
[eva] Recording results for cassign_test
[eva] done for function cassign_test
......
tests/value/oracle/partitioning-interproc.1.res.oracle
+ 1
− 1
View file @ 57270c64
......@@ -14,7 +14,7 @@
[eva:final-states] Values at end of function fabs:
__retres ∈ [-0. .. 1.79769313486e+308]
[eva:final-states] Values at end of function fabs_test:
x ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
x ∈ [-1. .. 1.]
[from] Computing for function fabs
[from] Done for function fabs
[from] Computing for function fabs_test
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment