diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli index 59fd3707a55fb9943393fd638761a71942cddff4..cea36be39f235677eb1c65e0471c3509d48f79c6 100644 --- a/src/plugins/dive/graph_types.mli +++ b/src/plugins/dive/graph_types.mli @@ -32,7 +32,7 @@ type node_locality = { loc_function : Cil_types.kernel_function option; } -type node_precision = Singleton | Normal | Wide | Critical +type node_precision = Unevaluated | Singleton | Normal | Wide | Critical type node = { node_key : int; diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml index 9c4aab6de23323abb9e4308fafb7596230e672f6..3f0979ffefd47f1a03ce4a358fe0a8c7d2bf5473 100644 --- a/src/plugins/dive/imprecision_graph.ml +++ b/src/plugins/dive/imprecision_graph.ml @@ -49,7 +49,7 @@ include G let next_node_key = ref 0 let next_dependency_key = ref 0 -let create_node ?(node_precision=Singleton) ~node_kind ~node_locality g = +let create_node ?(node_precision=Unevaluated) ~node_kind ~node_locality g = let node = { node_key = !next_node_key; node_kind; @@ -68,7 +68,8 @@ let update_node_precision node new_precision = | Critical, _ | _, Critical -> Critical | Wide, _ | _, Wide -> Wide | Normal, _ | _, Normal -> Normal - | Singleton, Singleton -> Singleton + | Singleton, _ | _, Singleton -> Singleton + | Unevaluated, Unevaluated -> Unevaluated let create_dependency ~allow_folding g v1 dependency_kind v2 = let same_kind (_,e,_) = @@ -143,13 +144,15 @@ let ouptput_to_dot out_channel g = | Alarm _ -> [ `Shape `Doubleoctagon ; `Style `Bold ] | File -> [ `Style `Invis ] and precision = match v.node_precision with + | Unevaluated -> [] | Singleton -> [`Color 0x88aaff ; `Style `Filled ; `Fillcolor 0xaaccff] - | Normal -> [] + | Normal -> [ `Color 0x004400 ; + `Style `Filled ; `Fillcolor 0xeeffee ] | Wide -> [ `Color 0xff0000 ; `Style `Filled ; `Fillcolor 0xffbbbb ] | Critical -> [ `Color 0xff0000 ; `Style `Bold ; - `Style `Filled ; `Fillcolor 0xffbbbb ] + `Style `Filled ; `Fillcolor 0xff0000 ] in l := precision @ kind @ !l; if not v.node_deps_computed then diff --git a/src/plugins/dive/tests/dive/assigned_param.i b/src/plugins/dive/tests/dive/assigned_param.i index 322aa200478933843561c32efa025212c260607e..a5d5fd969b460290476e06681fab085f00f35fbc 100644 --- a/src/plugins/dive/tests/dive/assigned_param.i +++ b/src/plugins/dive/tests/dive/assigned_param.i @@ -1,5 +1,5 @@ /* run.config -STDOPT: +"-dive-from main::w" +STDOPT: +"-dive-from main::w -dive-depth-limit 5" */ volatile int nondet; diff --git a/src/plugins/dive/tests/dive/const.i b/src/plugins/dive/tests/dive/const.i index adc5365c8c65e97e4fb497cc0ff8c1119ac420dc..3534fa8e7038b2d80dc0fe0a54137c6b2d771c78 100644 --- a/src/plugins/dive/tests/dive/const.i +++ b/src/plugins/dive/tests/dive/const.i @@ -1,5 +1,5 @@ /* run.config -STDOPT: +"-dive-from main::res" +STDOPT: +"-dive-from main::res -dive-depth-limit 5" */ int f(int x, int y) diff --git a/src/plugins/dive/tests/dive/oracle/assigned_param.dot b/src/plugins/dive/tests/dive/oracle/assigned_param.dot index 460be6d9d7299106e74d0f4c06e6ddb4b90058d3..e988a3cdc4ab10e39ce00d0ed91711d85cfe7c08 100644 --- a/src/plugins/dive/tests/dive/oracle/assigned_param.dot +++ b/src/plugins/dive/tests/dive/oracle/assigned_param.dot @@ -1,12 +1,14 @@ digraph G { - cp0 [fillcolor="#AACCFF", color="#88AAFF", style="invis,filled,dotted", ]; - cp1 [label=<w>, shape=box, fillcolor="#AACCFF", color="#88AAFF", - style="filled", ]; + cp0 [style="invis,dotted", ]; + cp1 [label=<w>, shape=box, ]; cp2 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF", style="filled", ]; - cp3 [label=<z>, shape=box, ]; - cp4 [label=<x>, shape=box, ]; - cp5 [label=<z>, shape=box, style="dotted", ]; + cp3 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400", + style="filled", ]; + cp4 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400", + style="filled", ]; + cp5 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400", + style="filled", ]; subgraph cluster_file_1 { label=<tests/dive/assigned_param.i>; cp0; subgraph cluster_function_19 { label=<f>; cp3;cp2; diff --git a/src/plugins/dive/tests/dive/oracle/const.dot b/src/plugins/dive/tests/dive/oracle/const.dot index cce0e10e5aa4ee290c68002c57da8703017528c2..ddf007a23e712c446ac4eb65ea6d8bbf761928d2 100644 --- a/src/plugins/dive/tests/dive/oracle/const.dot +++ b/src/plugins/dive/tests/dive/oracle/const.dot @@ -1,17 +1,22 @@ digraph G { - cp0 [fillcolor="#AACCFF", color="#88AAFF", style="invis,filled,dotted", ]; - cp1 [label=<res>, shape=box, fillcolor="#AACCFF", color="#88AAFF", - style="filled", ]; - cp2 [fillcolor="#AACCFF", color="#88AAFF", style="invis,filled,dotted", ]; + cp0 [style="invis,dotted", ]; + cp1 [label=<res>, shape=box, ]; + cp2 [style="invis,dotted", ]; cp3 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF", style="filled", ]; - cp4 [label=<c>, shape=box, ]; - cp5 [label=<w>, shape=box, ]; - cp6 [label=<x>, shape=box, style="dotted", ]; - cp7 [label=<y>, shape=box, style="dotted", ]; + cp4 [label=<c>, shape=box, fillcolor="#EEFFEE", color="#004400", + style="filled", ]; + cp5 [label=<w>, shape=box, fillcolor="#EEFFEE", color="#004400", + style="filled", ]; + cp6 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400", + style="filled", ]; + cp7 [label=<y>, shape=box, fillcolor="#EEFFEE", color="#004400", + style="filled", ]; + cp8 [label=<i>, shape=box, fillcolor="#EEFFEE", color="#004400", + style="filled", ]; subgraph cluster_file_1 { label=<tests/dive/const.i>; cp0; - subgraph cluster_function_25 { label=<main>; cp1; + subgraph cluster_function_25 { label=<main>; cp8;cp1; }; }; subgraph cluster_file_2 { label=<>; cp2; @@ -24,5 +29,7 @@ digraph G { cp5 -> cp3; cp6 -> cp4; cp7 -> cp5; + cp8 -> cp6; + cp8 -> cp7; } \ No newline at end of file diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot index acc4db37e9f88f572c2bd4c3caa454f2b24c365d..d8595e7b16c2177c22a48eaee5cdf927b63a5ce7 100644 --- a/src/plugins/dive/tests/dive/oracle/various.dot +++ b/src/plugins/dive/tests/dive/oracle/various.dot @@ -1,5 +1,5 @@ digraph G { - cp0 [fillcolor="#AACCFF", color="#88AAFF", style="invis,filled,dotted", ]; + cp0 [style="invis,dotted", ]; cp1 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000", style="filled", ]; cp2 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000", @@ -8,8 +8,7 @@ digraph G { style="filled", ]; cp4 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF", style="filled", ]; - cp5 [label=<z>, shape=box, fillcolor="#AACCFF", color="#88AAFF", - style="filled", ]; + cp5 [label=<z>, shape=box, ]; cp6 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000", style="filled", ]; cp7 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000", @@ -17,12 +16,12 @@ digraph G { cp8 [label=<tmp_0>, shape=box, fillcolor="#FFBBBB", color="#FF0000", style="filled", ]; cp9 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF", - style="filled,dotted", ]; + style="filled", ]; cp10 [label=<is_nan_or_infinite: \is_finite((float)((double)((double)y * 2.0)))>, - shape=doubleoctagon, fillcolor="#FFBBBB", color="#FF0000", + shape=doubleoctagon, fillcolor="#FF0000", color="#FF0000", style="bold,filled,bold", ]; cp11 [label=<is_nan_or_infinite: \is_finite((float)(y + w))>, - shape=doubleoctagon, fillcolor="#FFBBBB", color="#FF0000", + shape=doubleoctagon, fillcolor="#FF0000", color="#FF0000", style="bold,filled,bold", ]; subgraph cluster_file_1 { label=<tests/dive/various.i>; cp4;cp0; diff --git a/src/plugins/dive/tests/dive/various.i b/src/plugins/dive/tests/dive/various.i index c8766e6a7ad7cb0efa2022ec6b2ddb8db1083d33..f89d87ed5c813d77ece8214c04a92afc61dbc2ca 100644 --- a/src/plugins/dive/tests/dive/various.i +++ b/src/plugins/dive/tests/dive/various.i @@ -1,5 +1,5 @@ /* run.config -STDOPT: +"-dive-from main::z,f::x2 -dive-from-function-alarms f,main" +STDOPT: +"-dive-from main::z,f::x2 -dive-from-function-alarms f,main -dive-depth-limit 5" */ float g;