Skip to content
Snippets Groups Projects
Commit 1847a8a9 authored by Valentin Perrelle's avatar Valentin Perrelle Committed by David Bühler
Browse files

[Dive] Add constant nodes

parent c0d05ec0
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
ivette/src/frama-c/plugins/dive/style.json
+ 9
− 0
View file @ 1847a8a9
......@@ -141,6 +141,15 @@
"background-color": "#e44"
}
},
{
"selector": "node[kind='const']",
"style": {
"shape": "ellipse",
"background-color": "#bbb",
"border-width": "1px",
"border-style": "dashed"
}
},
{
"selector": "node[kind='alarm']",
"style": {
......
src/plugins/dive/build.ml
+ 13
− 4
View file @ 1847a8a9
......@@ -265,6 +265,9 @@ let build_lval context callstack kinstr lval =
update_node_values node kinstr lval;
node
let build_const context callstack exp =
add_or_update_node context callstack (Const exp)
let build_alarm context callstack stmt alarm =
let node_kind = Alarm (stmt,alarm) in
let node_locality = build_node_locality callstack node_kind in
......@@ -367,8 +370,14 @@ let build_node_writes context node =
Seq.append callee_deps return_deps
and build_exp_deps callstack stmt kind exp : deps_builder =
List.to_seq (EnumLvals.in_exp exp) |>
Seq.flat_map (build_lval_deps callstack stmt kind)
let lvals = EnumLvals.in_exp exp in
if lvals <> [] then
List.to_seq lvals |>
Seq.flat_map (build_lval_deps callstack stmt kind)
else
let kinstr = Kstmt stmt in
let dst = build_const context callstack exp in
Seq.return (Graph.create_dependency graph kinstr dst kind node)
and build_lval_deps callstack stmt kind lval : deps_builder =
let kinstr = Kstmt stmt in
......@@ -397,7 +406,7 @@ let build_node_writes context node =
build_scattered_deps callstack kinstr lval
| Alarm (stmt,alarm) ->
build_alarm_deps callstack stmt alarm
| Unknown _ | AbsoluteMemory | String _ | Error _ ->
| Unknown _ | AbsoluteMemory | String _ | Const _ | Error _ ->
Seq.empty
......@@ -512,7 +521,7 @@ let build_node_reads context node =
build_reads_deps callstack Kglobal (Cil_types.Var vi, Cil_types.NoOffset)
| Scattered (_lval,kinstr) ->
build_kinstr_deps callstack None kinstr
| Alarm _ | Unknown _ | AbsoluteMemory | String _ | Error _ ->
| Alarm _ | Unknown _ | AbsoluteMemory | Const _ | String _ | Error _ ->
Seq.empty
......
src/plugins/dive/dive_graph.ml
+ 2
− 0
View file @ 1847a8a9
......@@ -233,6 +233,7 @@ let ouptput_to_dot out_channel g =
`Style `Bold ; `Color 0xff0000 ;
`Style `Filled ; `Fillcolor 0xff0000 ]
| AbsoluteMemory | String _ -> [`Shape `Box3d]
| Const _ -> [`Shape `Ellipse]
| Error _ -> [`Color 0xff0000]
and range = match v.node_range with
| Empty -> []
......@@ -295,6 +296,7 @@ struct
| Alarm _ -> "alarm"
| AbsoluteMemory -> "absolute"
| String _ -> "string"
| Const _ -> "const"
| Error _ -> "error"
in
`String s
......
src/plugins/dive/dive_types.ml
+ 1
− 0
View file @ 1847a8a9
......@@ -28,6 +28,7 @@ type node_kind =
| Alarm of Cil_types.stmt * Alarms.alarm
| AbsoluteMemory
| String of int * Base.cstring
| Const of Cil_types.exp
| Error of string
type callstack = Callstack.t
......
src/plugins/dive/node_kind.ml
+ 11
− 3
View file @ 1847a8a9
......@@ -70,6 +70,10 @@ struct
Datatype.Int.compare i1 i2
| String _, _ -> 1
| _, String _ -> -1
| Const (e1), Const(e2) ->
Cil_datatype.Exp.compare e1 e2
| Const _, _ -> 1
| _, Const _ -> -1
| Error s1, Error s2 ->
Datatype.String.compare s1 s2
......@@ -86,6 +90,7 @@ struct
Stmt.equal stmt1 stmt2 && Alarms.equal alarm1 alarm2
| AbsoluteMemory, AbsoluteMemory -> true
| String (i,_), String (j,_) -> Datatype.Int.equal i j
| Const (e1), Const(e2) -> Cil_datatype.Exp.equal e1 e2
| Error s1, Error s2 -> Datatype.String.equal s1 s2
| _ -> false
......@@ -102,6 +107,7 @@ struct
Hashtbl.hash (5, Stmt.hash stmt, Alarms.hash alarm)
| AbsoluteMemory -> 6
| String (i, _) -> Hashtbl.hash (7, i)
| Const (e) -> Hashtbl.hash (7, Cil_datatype.Exp.hash e)
| Error s -> Hashtbl.hash (8, s)
end
......@@ -110,15 +116,15 @@ include Datatype.Make (DatatypeInput)
let get_base = function
| Scalar (vi,_,_) | Composite (vi) -> Some vi
| Scattered _ | Unknown _ | Alarm _ | AbsoluteMemory | String _ | Error _ ->
None
| Scattered _ | Unknown _ | Alarm _ | AbsoluteMemory
| String _ | Const _ | Error _ -> None
let to_lval = function
| Scalar (vi,_typ,offset) -> Some (Cil_types.Var vi, offset)
| Composite (vi) -> Some (Cil_types.Var vi, Cil_types.NoOffset)
| Scattered (lval,_) -> Some lval
| Unknown (lval,_) -> Some lval
| Alarm (_,_) | AbsoluteMemory | String _ | Error _ -> None
| Alarm (_,_) | AbsoluteMemory | String _ | Const _ | Error _ -> None
let pretty fmt = function
| (Scalar _ | Composite _ | Scattered _ | Unknown _) as kind ->
......@@ -131,5 +137,7 @@ let pretty fmt = function
Format.fprintf fmt "%S" s
| String (_, CSWstring s) ->
Format.fprintf fmt "L\"%s\"" (Escape.escape_wstring s)
| Const (e) ->
Format.fprintf fmt "%a" Cil_printer.pp_exp e
| Error s ->
Format.fprintf fmt "%s" s
src/plugins/dive/tests/dive/oracle/manydeps.dot
+ 5
− 3
View file @ 1847a8a9
......@@ -12,12 +12,13 @@ digraph G {
cp12 [label=<t10>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
cp14 [label=<__retres>, shape=box, style="bold", ];
cp15 [label=<*(pt[x])>, shape=parallelogram, fillcolor="#AACCFF",
cp15 [label=<0>, shape=ellipse, ];
cp17 [label=<*(pt[x])>, shape=parallelogram, fillcolor="#AACCFF",
color="#88AAFF", style="filled,dotted", ];
subgraph cluster_cs_1 { label=<many_writes>; cp12;cp10;cp8;cp6;cp4;cp2;
};
subgraph cluster_cs_2 { label=<many_values>; cp15;cp14;
subgraph cluster_cs_2 { label=<many_values>; cp17;cp15;cp14;
};
cp2 -> cp2 [style="bold", ];
......@@ -26,6 +27,7 @@ digraph G {
cp8 -> cp2;
cp10 -> cp2;
cp12 -> cp2;
cp15 -> cp14;
cp15 -> cp14 [style="bold", ];
cp17 -> cp14;
}
\ No newline at end of file
src/plugins/dive/tests/dive/oracle/ranges.dot
+ 57
− 1
View file @ 1847a8a9
......@@ -36,8 +36,36 @@ digraph G {
style="filled", ];
cp37 [label=<f7>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp39 [label=<0>, shape=ellipse, ];
cp41 [label=<3>, shape=ellipse, ];
cp43 [label=<0>, shape=ellipse, ];
cp45 [label=<12>, shape=ellipse, ];
cp47 [label=<0>, shape=ellipse, ];
cp49 [label=<127>, shape=ellipse, ];
cp51 [label=<0>, shape=ellipse, ];
cp53 [label=<42000>, shape=ellipse, ];
cp55 [label=<0>, shape=ellipse, ];
cp57 [label=<1350000>, shape=ellipse, ];
cp59 [label=<0>, shape=ellipse, ];
cp61 [label=<910000000>, shape=ellipse, ];
cp63 [label=<0>, shape=ellipse, ];
cp65 [label=<2000000000>, shape=ellipse, ];
cp67 [label=<0.f>, shape=ellipse, ];
cp69 [label=<0.001f>, shape=ellipse, ];
cp71 [label=<0.f>, shape=ellipse, ];
cp73 [label=<3.14f>, shape=ellipse, ];
cp75 [label=<0.f>, shape=ellipse, ];
cp77 [label=<1020.f>, shape=ellipse, ];
cp79 [label=<0.f>, shape=ellipse, ];
cp81 [label=<1e7f>, shape=ellipse, ];
cp83 [label=<0.f>, shape=ellipse, ];
cp85 [label=<1e20f>, shape=ellipse, ];
cp87 [label=<0.f>, shape=ellipse, ];
cp89 [label=<1e36f>, shape=ellipse, ];
cp91 [label=<0.f>, shape=ellipse, ];
cp93 [label=<1e37f>, shape=ellipse, ];
subgraph cluster_cs_1 { label=<main>; cp37;cp35;cp33;cp31;cp29;cp27;cp25;cp23;cp21;cp19;cp17;cp15;cp13;cp11;cp9;cp7;cp5;cp3;cp2;
subgraph cluster_cs_1 { label=<main>; cp93;cp91;cp89;cp87;cp85;cp83;cp81;cp79;cp77;cp75;cp73;cp71;cp69;cp67;cp65;cp63;cp61;cp59;cp57;cp55;cp53;cp51;cp49;cp47;cp45;cp43;cp41;cp39;cp37;cp35;cp33;cp31;cp29;cp27;cp25;cp23;cp21;cp19;cp17;cp15;cp13;cp11;cp9;cp7;cp5;cp3;cp2;
};
cp3 -> cp2;
......@@ -58,5 +86,33 @@ digraph G {
cp33 -> cp5;
cp35 -> cp5;
cp37 -> cp5;
cp39 -> cp9;
cp41 -> cp9;
cp43 -> cp11;
cp45 -> cp11;
cp47 -> cp13;
cp49 -> cp13;
cp51 -> cp15;
cp53 -> cp15;
cp55 -> cp17;
cp57 -> cp17;
cp59 -> cp19;
cp61 -> cp19;
cp63 -> cp21;
cp65 -> cp21;
cp67 -> cp25;
cp69 -> cp25;
cp71 -> cp27;
cp73 -> cp27;
cp75 -> cp29;
cp77 -> cp29;
cp79 -> cp31;
cp81 -> cp31;
cp83 -> cp33;
cp85 -> cp33;
cp87 -> cp35;
cp89 -> cp35;
cp91 -> cp37;
cp93 -> cp37;
}
\ No newline at end of file
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