From 55c9e5d721beaf506fbe689ef4523e5e82e1bc0d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 9 Feb 2024 12:37:17 +0200 Subject: [PATCH 01/23] Add CFG test using graph-easy --- tests/regression/cfg/dune | 9 +++++ tests/regression/cfg/foo.t/foo.c | 8 +++++ tests/regression/cfg/foo.t/run.t | 51 +++++++++++++++++++++++++++++ tests/regression/cfg/util/cfgDot.ml | 12 +++++++ tests/regression/cfg/util/dune | 8 +++++ 5 files changed, 88 insertions(+) create mode 100644 tests/regression/cfg/dune create mode 100644 tests/regression/cfg/foo.t/foo.c create mode 100644 tests/regression/cfg/foo.t/run.t create mode 100644 tests/regression/cfg/util/cfgDot.ml create mode 100644 tests/regression/cfg/util/dune diff --git a/tests/regression/cfg/dune b/tests/regression/cfg/dune new file mode 100644 index 0000000000..c91c970cd9 --- /dev/null +++ b/tests/regression/cfg/dune @@ -0,0 +1,9 @@ +(env + (_ + (binaries ./util/cfgDot.exe))) + +(cram + (applies_to :whole_subtree) + (enabled_if %{bin-available:graph-easy}) + (deps + %{bin:cfgDot})) diff --git a/tests/regression/cfg/foo.t/foo.c b/tests/regression/cfg/foo.t/foo.c new file mode 100644 index 0000000000..597e0457f2 --- /dev/null +++ b/tests/regression/cfg/foo.t/foo.c @@ -0,0 +1,8 @@ +int main() { + int a = 1, b = 1; + while (a > 0 && b) { + a++; + b--; + } + return 0; +} diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t new file mode 100644 index 0000000000..414a0e72ee --- /dev/null +++ b/tests/regression/cfg/foo.t/run.t @@ -0,0 +1,51 @@ + $ cfgDot foo.c + + $ graph-easy --as=boxart cfg.dot + ┌──────────────────────────────────┐ + │ __goblint_dummy_init() │ + └──────────────────────────────────┘ + │ + │ return + ▼ + ┌──────────────────────────────────┐ + │ return of __goblint_dummy_init() │ + └──────────────────────────────────┘ + ┌──────────────────────────────────┐ + │ main() │ + └──────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────────────────┐ + │ 1 │ + └──────────────────────────────────┘ + │ + │ a = 1 + ▼ + ┌──────────────────────────────────┐ + │ 2 │ + └──────────────────────────────────┘ + │ + │ b = 1 + ▼ + ┌──────────────────┐ Neg(a > 0) ┌──────────────────────────────────┐ + ┌──────▶ │ 14 │ ◀──────────── │ 6 │ ◀┐ + │ └──────────────────┘ └──────────────────────────────────┘ │ + │ │ │ │ + │ │ return 0 │ Pos(a > 0) │ + │ ▼ ▼ │ + │ Neg(b) ┌──────────────────┐ ┌──────────────────────────────────┐ │ + │ │ return of main() │ ┌─────────── │ 7 │ │ + │ └──────────────────┘ │ └──────────────────────────────────┘ │ + │ │ │ │ + └──────────────────────────────┘ │ Pos(b) │ b = b - 1 + ▼ │ + ┌──────────────────────────────────┐ │ + │ 11 │ │ + └──────────────────────────────────┘ │ + │ │ + │ a = a + 1 │ + ▼ │ + ┌──────────────────────────────────┐ │ + │ 12 │ ─┘ + └──────────────────────────────────┘ diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml new file mode 100644 index 0000000000..d76a609299 --- /dev/null +++ b/tests/regression/cfg/util/cfgDot.ml @@ -0,0 +1,12 @@ +open Goblint_lib + +let main () = + Cilfacade.init (); + + let ast = Cilfacade.getAST (Fpath.v Sys.argv.(1)) in + CilCfg.createCFG ast; + let _cfgF, cfgB, _skippedByEdge = CfgTools.createCFG ast in + + CfgTools.fprint_hash_dot cfgB + +let () = main () diff --git a/tests/regression/cfg/util/dune b/tests/regression/cfg/util/dune new file mode 100644 index 0000000000..5f71944874 --- /dev/null +++ b/tests/regression/cfg/util/dune @@ -0,0 +1,8 @@ +(executable + (name cfgDot) + (libraries + goblint_lib + fpath + goblint.sites.dune + goblint.build-info.dune) + (preprocess (pps ppx_deriving.std))) From 3093d27482a7c66777a773dc1c641d988f1d3190 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 9 Feb 2024 12:44:17 +0200 Subject: [PATCH 02/23] Use locations in CFG test nodes --- tests/regression/cfg/foo.t/run.t | 105 +++++++++++++++------------- tests/regression/cfg/util/cfgDot.ml | 16 ++++- 2 files changed, 72 insertions(+), 49 deletions(-) diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index 414a0e72ee..69dc5213de 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -1,51 +1,60 @@ $ cfgDot foo.c $ graph-easy --as=boxart cfg.dot - ┌──────────────────────────────────┐ - │ __goblint_dummy_init() │ - └──────────────────────────────────┘ - │ - │ return - ▼ - ┌──────────────────────────────────┐ - │ return of __goblint_dummy_init() │ - └──────────────────────────────────┘ - ┌──────────────────────────────────┐ - │ main() │ - └──────────────────────────────────┘ - │ - │ (body) - ▼ - ┌──────────────────────────────────┐ - │ 1 │ - └──────────────────────────────────┘ - │ - │ a = 1 - ▼ - ┌──────────────────────────────────┐ - │ 2 │ - └──────────────────────────────────┘ - │ - │ b = 1 - ▼ - ┌──────────────────┐ Neg(a > 0) ┌──────────────────────────────────┐ - ┌──────▶ │ 14 │ ◀──────────── │ 6 │ ◀┐ - │ └──────────────────┘ └──────────────────────────────────┘ │ - │ │ │ │ - │ │ return 0 │ Pos(a > 0) │ - │ ▼ ▼ │ - │ Neg(b) ┌──────────────────┐ ┌──────────────────────────────────┐ │ - │ │ return of main() │ ┌─────────── │ 7 │ │ - │ └──────────────────┘ │ └──────────────────────────────────┘ │ - │ │ │ │ - └──────────────────────────────┘ │ Pos(b) │ b = b - 1 - ▼ │ - ┌──────────────────────────────────┐ │ - │ 11 │ │ - └──────────────────────────────────┘ │ - │ │ - │ a = a + 1 │ - ▼ │ - ┌──────────────────────────────────┐ │ - │ 12 │ ─┘ - └──────────────────────────────────┘ + ┌────────────────────┐ + │ :-1 │ + │ (synthetic: true) │ + └────────────────────┘ + │ + │ return + ▼ + ┌────────────────────┐ + │ :-1 │ + │ (synthetic: true) │ + └────────────────────┘ + ┌────────────────────┐ + │ foo.c:1:0-8:1 │ + │ (synthetic: false) │ + └────────────────────┘ + │ + │ (body) + ▼ + ┌────────────────────┐ + │ foo.c:2:7-2:12 │ + │ (synthetic: false) │ + └────────────────────┘ + │ + │ a = 1 + ▼ + ┌────────────────────┐ + │ foo.c:2:14-2:19 │ + │ (synthetic: false) │ + └────────────────────┘ + │ + │ b = 1 + ▼ + ┌────────────────────┐ ┌────────────────────┐ + │ foo.c:7:3-7:11 │ Neg(a > 0) │ foo.c:3:10-3:20 │ + ┌──────▶ │ (synthetic: false) │ ◀──────────── │ (synthetic: true) │ ◀┐ + │ └────────────────────┘ └────────────────────┘ │ + │ │ │ │ + │ │ return 0 │ Pos(a > 0) │ + │ ▼ ▼ │ + │ Neg(b) ┌────────────────────┐ ┌────────────────────┐ │ + │ │ foo.c:1:0-8:1 │ │ foo.c:3:10-3:20 │ │ + │ │ (synthetic: false) │ ┌─────────── │ (synthetic: true) │ │ + │ └────────────────────┘ │ └────────────────────┘ │ + │ │ │ │ + └────────────────────────────────┘ │ Pos(b) │ b = b - 1 + ▼ │ + ┌────────────────────┐ │ + │ foo.c:4:5-4:8 │ │ + │ (synthetic: false) │ │ + └────────────────────┘ │ + │ │ + │ a = a + 1 │ + ▼ │ + ┌────────────────────┐ │ + │ foo.c:5:5-5:8 │ │ + │ (synthetic: false) │ ─┘ + └────────────────────┘ diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml index d76a609299..afec2444ca 100644 --- a/tests/regression/cfg/util/cfgDot.ml +++ b/tests/regression/cfg/util/cfgDot.ml @@ -1,4 +1,5 @@ open Goblint_lib +open CfgTools let main () = Cilfacade.init (); @@ -7,6 +8,19 @@ let main () = CilCfg.createCFG ast; let _cfgF, cfgB, _skippedByEdge = CfgTools.createCFG ast in - CfgTools.fprint_hash_dot cfgB + let module NoExtraNodeStyles = + struct + let defaultNodeStyles = [] + let extraNodeStyles node = + let loc = Node.location node in + [Printf.sprintf "label=\"%s\\n(synthetic: %B)\"" (CilType.Location.show loc) loc.synthetic] + end + in + let out = open_out "cfg.dot" in + let iter_edges f = H.iter (fun n es -> List.iter (f n) es) cfgB in + let ppf = Format.formatter_of_out_channel out in + fprint_dot (module CfgPrinters (NoExtraNodeStyles)) iter_edges ppf; + Format.pp_print_flush ppf (); + close_out out let () = main () From b8c6e64f7981aaa10eccbfee729213007d1be349 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 9 Feb 2024 12:46:42 +0200 Subject: [PATCH 03/23] Use stdout for CFG test --- tests/regression/cfg/foo.t/run.t | 4 +--- tests/regression/cfg/util/cfgDot.ml | 6 ++---- 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index 69dc5213de..5f9df01ec0 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -1,6 +1,4 @@ - $ cfgDot foo.c - - $ graph-easy --as=boxart cfg.dot + $ cfgDot foo.c | graph-easy --as=boxart ┌────────────────────┐ │ :-1 │ │ (synthetic: true) │ diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml index afec2444ca..ae86dcac3e 100644 --- a/tests/regression/cfg/util/cfgDot.ml +++ b/tests/regression/cfg/util/cfgDot.ml @@ -16,11 +16,9 @@ let main () = [Printf.sprintf "label=\"%s\\n(synthetic: %B)\"" (CilType.Location.show loc) loc.synthetic] end in - let out = open_out "cfg.dot" in let iter_edges f = H.iter (fun n es -> List.iter (f n) es) cfgB in - let ppf = Format.formatter_of_out_channel out in + let ppf = Format.std_formatter in fprint_dot (module CfgPrinters (NoExtraNodeStyles)) iter_edges ppf; - Format.pp_print_flush ppf (); - close_out out + Format.pp_print_flush ppf () let () = main () From d13a432856485efc0dfb899045b0c1ed1b3400cf Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 9 Feb 2024 13:42:55 +0200 Subject: [PATCH 04/23] Use function names in CFG tests --- tests/regression/cfg/foo.t/run.t | 87 ++++++++++++++--------------- tests/regression/cfg/util/cfgDot.ml | 8 ++- 2 files changed, 47 insertions(+), 48 deletions(-) diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index 5f9df01ec0..429ea4f8a1 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -1,58 +1,55 @@ $ cfgDot foo.c | graph-easy --as=boxart - ┌────────────────────┐ - │ :-1 │ - │ (synthetic: true) │ - └────────────────────┘ + ┌──────────────────────────────────┐ + │ __goblint_dummy_init() │ + └──────────────────────────────────┘ │ │ return ▼ - ┌────────────────────┐ - │ :-1 │ - │ (synthetic: true) │ - └────────────────────┘ - ┌────────────────────┐ - │ foo.c:1:0-8:1 │ - │ (synthetic: false) │ - └────────────────────┘ + ┌──────────────────────────────────┐ + │ return of __goblint_dummy_init() │ + └──────────────────────────────────┘ + ┌──────────────────────────────────┐ + │ main() │ + └──────────────────────────────────┘ │ │ (body) ▼ - ┌────────────────────┐ - │ foo.c:2:7-2:12 │ - │ (synthetic: false) │ - └────────────────────┘ + ┌──────────────────────────────────┐ + │ foo.c:2:7-2:12 │ + │ (synthetic: false) │ + └──────────────────────────────────┘ │ │ a = 1 ▼ - ┌────────────────────┐ - │ foo.c:2:14-2:19 │ - │ (synthetic: false) │ - └────────────────────┘ + ┌──────────────────────────────────┐ + │ foo.c:2:14-2:19 │ + │ (synthetic: false) │ + └──────────────────────────────────┘ │ │ b = 1 ▼ - ┌────────────────────┐ ┌────────────────────┐ - │ foo.c:7:3-7:11 │ Neg(a > 0) │ foo.c:3:10-3:20 │ - ┌──────▶ │ (synthetic: false) │ ◀──────────── │ (synthetic: true) │ ◀┐ - │ └────────────────────┘ └────────────────────┘ │ - │ │ │ │ - │ │ return 0 │ Pos(a > 0) │ - │ ▼ ▼ │ - │ Neg(b) ┌────────────────────┐ ┌────────────────────┐ │ - │ │ foo.c:1:0-8:1 │ │ foo.c:3:10-3:20 │ │ - │ │ (synthetic: false) │ ┌─────────── │ (synthetic: true) │ │ - │ └────────────────────┘ │ └────────────────────┘ │ - │ │ │ │ - └────────────────────────────────┘ │ Pos(b) │ b = b - 1 - ▼ │ - ┌────────────────────┐ │ - │ foo.c:4:5-4:8 │ │ - │ (synthetic: false) │ │ - └────────────────────┘ │ - │ │ - │ a = a + 1 │ - ▼ │ - ┌────────────────────┐ │ - │ foo.c:5:5-5:8 │ │ - │ (synthetic: false) │ ─┘ - └────────────────────┘ + ┌────────────────────┐ ┌──────────────────────────────────┐ + │ foo.c:7:3-7:11 │ Neg(a > 0) │ foo.c:3:10-3:20 │ + ┌──────▶ │ (synthetic: false) │ ◀──────────── │ (synthetic: true) │ ◀┐ + │ └────────────────────┘ └──────────────────────────────────┘ │ + │ │ │ │ + │ │ return 0 │ Pos(a > 0) │ + │ ▼ ▼ │ + │ Neg(b) ┌────────────────────┐ ┌──────────────────────────────────┐ │ + │ │ return of main() │ │ foo.c:3:10-3:20 │ │ + │ │ │ ┌─────────── │ (synthetic: true) │ │ + │ └────────────────────┘ │ └──────────────────────────────────┘ │ + │ │ │ │ + └────────────────────────────────┘ │ Pos(b) │ b = b - 1 + ▼ │ + ┌──────────────────────────────────┐ │ + │ foo.c:4:5-4:8 │ │ + │ (synthetic: false) │ │ + └──────────────────────────────────┘ │ + │ │ + │ a = a + 1 │ + ▼ │ + ┌──────────────────────────────────┐ │ + │ foo.c:5:5-5:8 │ │ + │ (synthetic: false) │ ─┘ + └──────────────────────────────────┘ diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml index ae86dcac3e..ef13cbf763 100644 --- a/tests/regression/cfg/util/cfgDot.ml +++ b/tests/regression/cfg/util/cfgDot.ml @@ -11,9 +11,11 @@ let main () = let module NoExtraNodeStyles = struct let defaultNodeStyles = [] - let extraNodeStyles node = - let loc = Node.location node in - [Printf.sprintf "label=\"%s\\n(synthetic: %B)\"" (CilType.Location.show loc) loc.synthetic] + let extraNodeStyles = function + | Node.Statement _ as node -> + let loc = Node.location node in + [Printf.sprintf "label=\"%s\\n(synthetic: %B)\"" (CilType.Location.show loc) loc.synthetic] + | _ -> [] end in let iter_edges f = H.iter (fun n es -> List.iter (f n) es) cfgB in From 48d4b63e9aa587099047580f633012fb59e9de4f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 9 Feb 2024 13:43:14 +0200 Subject: [PATCH 05/23] Add cram tests for CFG --- tests/regression/00-sanity/19-if-0.t | 56 ++ tests/regression/00-sanity/20-if-0-realnode.t | 57 ++ tests/regression/00-sanity/21-empty-loops.t | 631 ++++++++++++++++++ tests/regression/dune | 9 +- 4 files changed, 752 insertions(+), 1 deletion(-) create mode 100644 tests/regression/00-sanity/19-if-0.t create mode 100644 tests/regression/00-sanity/20-if-0-realnode.t create mode 100644 tests/regression/00-sanity/21-empty-loops.t diff --git a/tests/regression/00-sanity/19-if-0.t b/tests/regression/00-sanity/19-if-0.t new file mode 100644 index 0000000000..50aa0ca189 --- /dev/null +++ b/tests/regression/00-sanity/19-if-0.t @@ -0,0 +1,56 @@ + $ cfgDot 19-if-0.c | graph-easy --as=boxart + ┌──────────────────────────────────┐ + │ __goblint_dummy_init() │ + └──────────────────────────────────┘ + │ + │ return + ▼ + ┌──────────────────────────────────┐ + │ return of __goblint_dummy_init() │ + └──────────────────────────────────┘ + ┌──────────────────────────────────┐ + │ main() │ + └──────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────┐ ┌──────────────────────────────────┐ + │ 19-if-0.c:15:9-15:27 │ Neg(0) │ 19-if-0.c:9:9-9:10 │ + │ (synthetic: false) │ ◀──────────────────── │ (synthetic: false) │ + └──────────────────────┘ └──────────────────────────────────┘ + │ │ + │ │ Pos(0) + │ ▼ + │ ┌──────────────────────────────────┐ + │ │ 19-if-0.c:11:9-11:16 │ + │ │ (synthetic: false) │ + │ └──────────────────────────────────┘ + │ │ + │ │ stuff() + │ ▼ + │ ┌──────────────────────────────────┐ + │ __goblint_check(1) │ 19-if-0.c:17:5-17:13 │ + └──────────────────────────────────────────▶ │ (synthetic: false) │ + └──────────────────────────────────┘ + │ + │ return 0 + ▼ + ┌──────────────────────────────────┐ + │ return of main() │ + └──────────────────────────────────┘ + ┌──────────────────────────────────┐ + │ stuff() │ + └──────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────────────────┐ + │ 19-if-0.c:5:1-5:1 │ + │ (synthetic: false) │ + └──────────────────────────────────┘ + │ + │ return + ▼ + ┌──────────────────────────────────┐ + │ return of stuff() │ + └──────────────────────────────────┘ diff --git a/tests/regression/00-sanity/20-if-0-realnode.t b/tests/regression/00-sanity/20-if-0-realnode.t new file mode 100644 index 0000000000..2b008394a8 --- /dev/null +++ b/tests/regression/00-sanity/20-if-0-realnode.t @@ -0,0 +1,57 @@ + $ cfgDot 20-if-0-realnode.c | graph-easy --as=boxart + ┌──────────────────────────────────┐ + │ __goblint_dummy_init() │ + └──────────────────────────────────┘ + │ + │ return + ▼ + ┌──────────────────────────────────┐ + │ return of __goblint_dummy_init() │ + └──────────────────────────────────┘ + ┌──────────────────────────────────┐ + │ main() │ + └──────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────────────────┐ Neg(0) + │ 20-if-0-realnode.c:8:9-8:10 │ ─────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────┘ + └──────────────────────────────────┘ + │ + │ Pos(0) + ▼ + ┌──────────────────────────────────┐ + │ 20-if-0-realnode.c:10:9-10:16 │ + │ (synthetic: false) │ + └──────────────────────────────────┘ + │ + │ stuff() + ▼ + ┌──────────────────────────────────┐ + │ 20-if-0-realnode.c:15:5-15:13 │ + │ (synthetic: false) │ + └──────────────────────────────────┘ + │ + │ return 0 + ▼ + ┌──────────────────────────────────┐ + │ return of main() │ + └──────────────────────────────────┘ + ┌──────────────────────────────────┐ + │ stuff() │ + └──────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────────────────┐ + │ 20-if-0-realnode.c:3:1-3:1 │ + │ (synthetic: false) │ + └──────────────────────────────────┘ + │ + │ return + ▼ + ┌──────────────────────────────────┐ + │ return of stuff() │ + └──────────────────────────────────┘ diff --git a/tests/regression/00-sanity/21-empty-loops.t b/tests/regression/00-sanity/21-empty-loops.t new file mode 100644 index 0000000000..ea13f4f52a --- /dev/null +++ b/tests/regression/00-sanity/21-empty-loops.t @@ -0,0 +1,631 @@ + $ cfgDot 21-empty-loops.c | graph-easy --as=boxart + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:75:3-75:11 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ suffix() + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:76:1-76:1 │ + │ (synthetic: false) │ ◀┐ + └─────────────────────────────────────────────────────────┘ │ + │ │ + │ return │ + ▼ │ + ┌─────────────────────────────────────────────────────────┐ │ + │ return of f_empty_goto_loop_suffix() │ │ + └─────────────────────────────────────────────────────────┘ │ + ┌─────────────────────────────────────────────────────────┐ │ Neg(1) + │ f_empty_goto_loop_suffix() │ │ + └─────────────────────────────────────────────────────────┘ │ + │ │ + │ (body) │ + ▼ │ + skip ┌─────────────────────────────────────────────────────────┐ │ + ┌────────────────────────────────────────────── │ 21-empty-loops.c:73:3-73:38 │ │ + │ │ (synthetic: false) │ │ + └─────────────────────────────────────────────▶ │ │ ─┘ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ main() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌───────────────────────────────┐ ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:8:7-8:26 │ Pos(r == 0) │ 21-empty-loops.c:7:5-7:11 │ + │ (synthetic: false) │ ◀─────────────────────────────────────────────── │ (synthetic: false) │ + └───────────────────────────────┘ └─────────────────────────────────────────────────────────┘ + │ │ + │ │ Neg(r == 0) + │ ▼ + │ ┌─────────────────────────────────────────────────────────┐ ┌─────────────────────────────┐ + │ │ 21-empty-loops.c:10:5-10:11 │ Pos(r == 1) │ 21-empty-loops.c:11:7-11:27 │ + │ │ (synthetic: false) │ ──────────────▶ │ (synthetic: false) │ + │ └─────────────────────────────────────────────────────────┘ └─────────────────────────────┘ + │ │ │ + │ │ Neg(r == 1) │ + │ ▼ │ + ┌─────────────────────────────┐ │ ┌─────────────────────────────────────────────────────────┐ │ + │ 21-empty-loops.c:14:7-14:33 │ Pos(r == 2) │ │ 21-empty-loops.c:13:5-13:11 │ │ + │ (synthetic: false) │ ◀────────────────┼─────────────────────────────────────────────────────────────────────────────── │ (synthetic: false) │ │ + └─────────────────────────────┘ │ └─────────────────────────────────────────────────────────┘ │ + │ │ │ │ + │ │ │ Neg(r == 2) │ + │ │ ▼ │ + │ │ ┌─────────────────────────────────────────────────────────┐ │ ┌──────────────────────────────┐ + │ │ │ 21-empty-loops.c:16:5-16:11 │ │ Pos(r == 3) │ 21-empty-loops.c:17:7-17:34 │ + │ │ │ (synthetic: false) │ ──────────────────┼──────────────────────────────────────────▶ │ (synthetic: false) │ + │ │ └─────────────────────────────────────────────────────────┘ │ └──────────────────────────────┘ + │ │ │ │ │ + │ │ │ Neg(r == 3) │ │ + │ │ ▼ │ │ + │ │ ┌─────────────────────────────────────────────────────────┐ │ │ + │ │ │ 21-empty-loops.c:19:5-19:11 │ │ │ + │ │ │ (synthetic: false) │ ──────────────────┼──────────────────────────────────────────────┼────────────────────────────────────┐ + │ │ └─────────────────────────────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ + │ │ │ Neg(r == 4) │ │ │ + │ │ ▼ │ │ │ + │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ + │ │ │ 21-empty-loops.c:22:5-22:11 │ │ │ │ + │ │ ┌────────────────────────────────────────────── │ (synthetic: false) │ │ │ │ + │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ + │ │ │ │ Neg(r == 5) │ │ │ + │ │ │ ▼ │ │ │ + │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ + │ │ │ │ 21-empty-loops.c:25:5-25:11 │ │ │ │ + │ ┌───────────────┼────────────────────────────────┼────────────────────────────────────────────── │ (synthetic: false) │ │ │ │ + │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ │ + │ │ │ │ │ Neg(r == 6) │ │ │ + │ │ │ │ ▼ │ │ │ + │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ + │ │ │ │ │ 21-empty-loops.c:28:5-28:11 │ │ │ │ + │ │ │ │ │ (synthetic: false) │ ─┐ │ │ │ + │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ + │ │ │ │ │ │ │ │ │ + │ │ │ │ │ Neg(r == 7) │ │ │ │ + │ │ │ │ ▼ │ │ │ │ + │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ + │ │ │ │ │ 21-empty-loops.c:31:5-31:11 │ │ │ │ │ + │ │ │ │ │ (synthetic: false) │ ─┼────────────────┼──────────────────────────────────────────────┼────────────────────────────────────┼────────────────────────────────────────────┐ + │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ + │ │ │ │ │ │ │ │ │ │ + │ │ │ │ │ Neg(r == 8) │ │ │ │ │ + │ │ │ │ ▼ │ │ │ │ │ + │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ │ + │ │ │ │ │ 21-empty-loops.c:34:5-34:11 │ │ │ │ │ │ + │ │ │ │ │ (synthetic: false) │ ─┼────────────────┼──────────────────────────────┐ │ │ │ + │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ │ + │ │ │ │ │ │ │ │ │ │ │ + │ │ │ │ │ Neg(r == 9) │ │ │ │ │ │ + │ │ │ │ ▼ │ │ │ │ │ │ + │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ │ │ + │ │ │ │ │ 21-empty-loops.c:37:5-37:12 │ │ │ │ │ │ │ + ┌────┼──────────────────────────────┼───────────────┼────────────────────────────────┼────────────────────────────────────────────── │ (synthetic: false) │ │ │ │ │ │ │ + │ │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ │ + │ │ │ │ │ │ │ │ │ │ │ │ + │ │ │ │ │ │ Neg(r == 10) │ │ │ │ │ │ + │ │ │ │ │ ▼ │ │ │ │ │ │ + │ │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ │ │ + │ │ │ │ │ │ 21-empty-loops.c:40:5-40:12 │ │ │ │ │ │ │ + ┌────┼────┼──────────────────────────────┼───────────────┼────────────────────────────────┼────────────────────────────────────────────── │ (synthetic: false) │ │ │ │ │ │ │ + │ │ │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ │ + │ │ │ │ │ │ │ │ │ │ │ │ │ + │ │ │ │ │ │ │ Neg(r == 11) │ │ │ │ │ │ + │ │ │ │ │ │ ▼ │ │ │ │ │ │ + │ │ │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ │ │ + │ │ │ │ │ │ │ 21-empty-loops.c:43:5-43:12 │ │ │ │ │ │ │ + ┌─────────┼────┼────┼──────────────────────────────┼───────────────┼────────────────────────────────┼────────────────────────────────────────────── │ (synthetic: false) │ │ │ └───────────────┼───────────────────────────────┐ │ │ + │ │ │ │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ │ + │ │ │ │ │ │ │ │ │ │ │ │ │ │ + │ │ │ │ │ │ │ │ Neg(r == 12) └────────────────┼──────────────────────────────┐ │ │ │ │ + │ │ │ │ │ │ │ ▼ │ │ │ │ │ │ + │ │ │ │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ │ │ + │ │ │ │ │ │ │ │ 21-empty-loops.c:46:5-46:12 │ │ │ │ │ │ │ + │ ┌────┘ │ │ │ │ │ │ (synthetic: false) │ ─┐ │ │ │ │ │ │ + │ │ │ │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ │ │ + │ │ │ │ │ │ │ │ │ │ │ │ │ │ │ + │ │ ┌────┘ │ │ │ │ │ Pos(r == 13) │ │ │ │ └────┼────────────────────────────────────────────┼──────────────────────────────┐ + │ │ │ │ │ │ │ ▼ │ │ │ │ │ │ │ + │ │ │ │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ │ │ │ + │ │ │ │ │ │ │ │ 21-empty-loops.c:47:7-47:50 │ │ │ │ │ │ │ │ + │ │ │ ┌────┼──────────────────────────────┘ │ │ │ (synthetic: false) │ │ │ └───────────────┼────────────────────────────────────┼────┐ │ │ + │ │ │ │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ │ │ + │ │ │ │ │ │ │ │ │ │ │ │ │ │ │ + │ │ │ │ │ ┌───────────────┼────────────────────────────────┘ │ f_empty_goto_loop_multiple_semicolon_both() │ Neg(r == 13) │ f_empty_while_loop() │ f_empty_while_loop_suffix() │ │ │ Pos(r == 8) │ + │ │ │ │ │ │ │ ▼ ▼ ▼ ▼ │ │ ▼ │ + │ │ │ │ │ │ │ ┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ │ ┌─────────────────────────────┐ │ Pos(r == 9) + │ │ │ │ │ │ │ f_empty_goto_loop() │ │ │ │ f_empty_goto_loop_semicolon() │ 21-empty-loops.c:32:7-32:36 │ │ + │ │ │ │ │ │ └──────────────────────────────────────────────────────────────────────────────▶ │ │ ◀┼────┼──────────────────────────────────── │ (synthetic: false) │ │ + │ │ │ │ │ │ │ │ │ │ └─────────────────────────────┘ │ + │ │ │ │ │ │ f_empty_goto_loop_suffix() │ │ │ │ │ + │ │ │ │ └──────────────────────────────┼──────────────────────────────────────────────────────────────────────────────────────────────▶ │ │ │ │ │ + │ │ │ │ │ │ │ │ │ │ + │ │ │ │ │ │ │ │ │ ┌─────────────────────────────┐ │ + │ │ │ │ │ │ │ │ │ f_empty_while_loop_semicolon() │ 21-empty-loops.c:35:7-35:37 │ │ + │ │ │ │ │ Pos(r == 5) │ │ ◀┼────┼──────────────────────────────────── │ (synthetic: false) │ ◀┘ + │ │ │ │ │ │ │ │ │ └─────────────────────────────┘ + │ │ │ │ │ ┌───────────────────────────────┐ │ │ │ │ + │ │ │ │ │ │ 21-empty-loops.c:23:7-23:30 │ f_nonempty_while_loop() │ 21-empty-loops.c:51:3-51:11 │ │ │ f_empty_goto_loop_multiple_semicolon_first() + │ │ │ │ └───────────▶ │ (synthetic: false) │ ───────────────────────────────────────────────▶ │ (synthetic: false) │ ◀┼────┼──────────────────────────────────────────────────────────────────────┐ + │ │ │ │ └───────────────────────────────┘ │ │ │ │ │ + │ │ │ │ │ │ │ │ ┌─────────────────────────────┐ │ + │ │ │ │ │ │ │ │ f_empty_goto_loop_multiple() │ 21-empty-loops.c:38:7-38:35 │ │ + │ │ │ │ │ │ ◀┼────┼──────────────────────────────────── │ (synthetic: false) │ │ + │ │ │ │ │ │ │ │ └─────────────────────────────┘ │ + │ │ │ │ ┌───────────────────────────────┐ │ │ │ │ ▲ │ + │ │ │ │ Pos(r == 6) │ 21-empty-loops.c:26:7-26:33 │ f_empty_goto_loop_prefix() │ │ │ │ │ │ + │ │ │ └───────────────────────────────────────────────▶ │ (synthetic: false) │ ───────────────────────────────────────────────▶ │ │ │ │ │ Pos(r == 10) │ + │ │ │ └───────────────────────────────┘ │ │ │ │ │ │ + │ │ │ f_empty_goto_loop_multiple_semicolon_second() │ │ │ │ │ │ + │ │ │ ┌──────────────────────────────────────────────────────────────────────────────▶ │ │ │ │ │ │ + │ │ │ │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ │ │ │ │ + │ │ │ │ │ ▲ ▲ │ │ │ │ + │ │ │ │ │ return 0 │ f_nonempty_goto_loop() │ f_empty_while_loop_prefix() │ │ │ │ + │ │ │ │ ▼ │ │ │ │ │ │ + │ │ │ │ ┌─────────────────────────────────────────────────────────┐ ┌─────────────────────────────┐ │ │ │ │ │ + │ │ │ │ │ return of main() │ │ 21-empty-loops.c:20:7-20:29 │ Pos(r == 4) │ │ │ │ │ + │ │ │ │ │ │ │ (synthetic: false) │ ◀────────────────┼────────────────────────────────────┘ │ │ │ + │ │ │ │ └─────────────────────────────────────────────────────────┘ └─────────────────────────────┘ │ │ │ │ + │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ + │ │ │ │ │ 21-empty-loops.c:29:7-29:34 │ │ │ │ │ + │ │ │ │ │ (synthetic: false) │ ─────────────────────────────────────────────────────────────────┘ │ │ │ + │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ + │ │ │ │ ▲ Pos(r == 7) │ │ │ + │ │ │ │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ │ │ + │ │ │ │ │ │ + │ │ │ │ │ │ + │ │ └────────────────────────────────────────────────────────┼───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ │ + │ │ │ │ + │ │ │ ┌─────────────────────────────────────────────────────────┐ │ + │ │ │ Pos(r == 11) │ 21-empty-loops.c:41:7-41:51 │ │ + │ └─────────────────────────────────────────────────────────────┼──────────────────────────────────────────────────────────────────────────────▶ │ (synthetic: false) │ ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ + │ │ └─────────────────────────────────────────────────────────┘ + │ │ ┌─────────────────────────────────────────────────────────┐ + │ │ │ 21-empty-loops.c:44:7-44:52 │ + │ └─────────────────────────────────────────────────────────────────────────────── │ (synthetic: false) │ + │ └─────────────────────────────────────────────────────────┘ + │ Pos(r == 12) ▲ + └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ + + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_while_loop_suffix() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:80:10-80:11 │ ─────────────┐ + │ (synthetic: true) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:82:3-82:11 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ suffix() + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:83:1-83:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_while_loop_suffix() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_goto_loop_prefix() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:112:3-112:11 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ prefix() + ▼ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:115:3-115:38 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:116:1-116:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop_prefix() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_while_loop_prefix() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:120:3-120:11 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ prefix() + ▼ + ┌─────────────────────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:122:10-122:11 │ ─────────────┐ + │ (synthetic: true) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:123:1-123:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_while_loop_prefix() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_goto_loop() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:57:3-57:31 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:58:1-58:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_while_loop() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:62:10-62:11 │ ─────────────┐ + │ (synthetic: true) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:63:1-63:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_while_loop() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ f_nonempty_goto_loop() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ body() + │ 21-empty-loops.c:93:3-93:9 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:95:1-95:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_nonempty_goto_loop() │ + └─────────────────────────────────────────────────────────┘ + + ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ + │ │ + │ ┌─────────────────────────────────────────────────────────┐ │ + │ │ f_nonempty_while_loop() │ │ + │ └─────────────────────────────────────────────────────────┘ │ + │ │ │ body() + │ │ (body) │ + │ ▼ │ + ┌───────────────────────────────┐ ┌─────────────────────────────────────────────────────────┐ │ + │ 21-empty-loops.c:101:5-101:11 │ Pos(1) │ 21-empty-loops.c:99:10-99:11 │ │ + │ (synthetic: false) │ ◀─────────────────────────────────────────────── │ (synthetic: true) │ ◀┘ + └───────────────────────────────┘ └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:103:1-103:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_nonempty_while_loop() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_goto_loop_semicolon() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:127:1-128:3 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:131:1-131:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop_semicolon() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_while_loop_semicolon() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:135:10-135:11 │ ─────────────┐ + │ (synthetic: true) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:138:1-138:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_while_loop_semicolon() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:143:3-143:42 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:146:1-146:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple_semicolon_first() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:150:1-151:3 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:155:1-155:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple_semicolon_first() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple_semicolon_second() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:160:3-160:59 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:164:1-164:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple_semicolon_second() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple_semicolon_both() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:168:1-169:3 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:174:1-174:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple_semicolon_both() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ suffix() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:68:1-68:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of suffix() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ body() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:88:1-88:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of body() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ prefix() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:108:1-108:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of prefix() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ + │ __goblint_dummy_init() │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of __goblint_dummy_init() │ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:130:3-130:41 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:145:3-145:42 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:152:3-152:58 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:154:3-154:58 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:161:1-162:3 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:163:3-163:59 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:170:3-170:57 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:171:1-172:3 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:173:3-173:57 │ ─────────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────────┘ + └─────────────────────────────────────────────────────────┘ diff --git a/tests/regression/dune b/tests/regression/dune index fdb1d941c2..a238677edc 100644 --- a/tests/regression/dune +++ b/tests/regression/dune @@ -1,3 +1,10 @@ +(env + (_ + (binaries ./cfg/util/cfgDot.exe))) + (cram (applies_to :whole_subtree) - (deps %{bin:goblint} (package goblint))) ; need entire package for includes/ + (deps + %{bin:goblint} + (package goblint) ; need entire package for includes/ + %{bin:cfgDot})) From 6ed1aae9f5aadb39cc157831bb722c9ee878d726 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 9 Feb 2024 14:09:17 +0200 Subject: [PATCH 06/23] Move some functions to CfgTools --- src/common/framework/cfgTools.ml | 6 ++++++ src/framework/control.ml | 8 +------- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml index 106f8eb5c3..53d680da9a 100644 --- a/src/common/framework/cfgTools.ml +++ b/src/common/framework/cfgTools.ml @@ -620,6 +620,12 @@ let getCFG (file: file) : cfg * cfg * stmt list CfgEdgeH.t = if get_bool "justcfg" then fprint_hash_dot cfgB; (fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n []), skippedByEdge +let compute_cfg_skips file = + let cfgF, cfgB, skippedByEdge = getCFG file in + (module struct let prev = cfgB let next = cfgF end : CfgBidir), skippedByEdge + +let compute_cfg file = fst (compute_cfg_skips file) + let iter_fd_edges (module Cfg : CfgBackward) fd = let ready = NH.create 113 in diff --git a/src/framework/control.ml b/src/framework/control.ml index 391c766feb..5a06466467 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -811,15 +811,9 @@ let rec analyze_loop (module CFG : CfgBidir) file fs change_info skippedByEdge = (* TODO: do some more incremental refinement and reuse parts of solution *) analyze_loop (module CFG) file fs change_info skippedByEdge -let compute_cfg_skips file = - let cfgF, cfgB, skippedByEdge = CfgTools.getCFG file in - (module struct let prev = cfgB let next = cfgF end : CfgBidir), skippedByEdge - -let compute_cfg = fst % compute_cfg_skips - (** The main function to perform the selected analyses. *) let analyze change_info (file: file) fs = if (get_bool "dbg.verbose") then print_endline "Generating the control flow graph."; - let (module CFG), skippedByEdge = compute_cfg_skips file in + let (module CFG), skippedByEdge = CfgTools.compute_cfg_skips file in MyCFG.current_cfg := (module CFG); analyze_loop (module CFG) file fs change_info skippedByEdge From b7275325243004907224652a2395c23b7828b617 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 9 Feb 2024 14:13:03 +0200 Subject: [PATCH 07/23] Test CFGs per function --- tests/regression/00-sanity/19-if-0.t | 65 +- tests/regression/00-sanity/20-if-0-realnode.t | 67 +- tests/regression/00-sanity/21-empty-loops.t | 1022 +++++++---------- tests/regression/cfg/foo.t/run.t | 95 +- tests/regression/cfg/util/cfgDot.ml | 30 +- tests/regression/cfg/util/dune | 3 +- 6 files changed, 497 insertions(+), 785 deletions(-) diff --git a/tests/regression/00-sanity/19-if-0.t b/tests/regression/00-sanity/19-if-0.t index 50aa0ca189..0814240a90 100644 --- a/tests/regression/00-sanity/19-if-0.t +++ b/tests/regression/00-sanity/19-if-0.t @@ -1,56 +1,33 @@ - $ cfgDot 19-if-0.c | graph-easy --as=boxart - ┌──────────────────────────────────┐ - │ __goblint_dummy_init() │ - └──────────────────────────────────┘ - │ - │ return - ▼ - ┌──────────────────────────────────┐ - │ return of __goblint_dummy_init() │ - └──────────────────────────────────┘ - ┌──────────────────────────────────┐ - │ main() │ - └──────────────────────────────────┘ + $ cfgDot 19-if-0.c + + $ graph-easy --as=boxart main.dot + ┌──────────────────────┐ + │ main() │ + └──────────────────────┘ │ │ (body) ▼ - ┌──────────────────────┐ ┌──────────────────────────────────┐ - │ 19-if-0.c:15:9-15:27 │ Neg(0) │ 19-if-0.c:9:9-9:10 │ - │ (synthetic: false) │ ◀──────────────────── │ (synthetic: false) │ - └──────────────────────┘ └──────────────────────────────────┘ + ┌──────────────────────┐ ┌──────────────────────┐ + │ 19-if-0.c:15:9-15:27 │ Neg(0) │ 19-if-0.c:9:9-9:10 │ + │ (synthetic: false) │ ◀──────────────────── │ (synthetic: false) │ + └──────────────────────┘ └──────────────────────┘ │ │ │ │ Pos(0) │ ▼ - │ ┌──────────────────────────────────┐ - │ │ 19-if-0.c:11:9-11:16 │ - │ │ (synthetic: false) │ - │ └──────────────────────────────────┘ + │ ┌──────────────────────┐ + │ │ 19-if-0.c:11:9-11:16 │ + │ │ (synthetic: false) │ + │ └──────────────────────┘ │ │ │ │ stuff() │ ▼ - │ ┌──────────────────────────────────┐ - │ __goblint_check(1) │ 19-if-0.c:17:5-17:13 │ - └──────────────────────────────────────────▶ │ (synthetic: false) │ - └──────────────────────────────────┘ + │ ┌──────────────────────┐ + │ __goblint_check(1) │ 19-if-0.c:17:5-17:13 │ + └──────────────────────────────────────────▶ │ (synthetic: false) │ + └──────────────────────┘ │ │ return 0 ▼ - ┌──────────────────────────────────┐ - │ return of main() │ - └──────────────────────────────────┘ - ┌──────────────────────────────────┐ - │ stuff() │ - └──────────────────────────────────┘ - │ - │ (body) - ▼ - ┌──────────────────────────────────┐ - │ 19-if-0.c:5:1-5:1 │ - │ (synthetic: false) │ - └──────────────────────────────────┘ - │ - │ return - ▼ - ┌──────────────────────────────────┐ - │ return of stuff() │ - └──────────────────────────────────┘ + ┌──────────────────────┐ + │ return of main() │ + └──────────────────────┘ diff --git a/tests/regression/00-sanity/20-if-0-realnode.t b/tests/regression/00-sanity/20-if-0-realnode.t index 2b008394a8..1363b3d26e 100644 --- a/tests/regression/00-sanity/20-if-0-realnode.t +++ b/tests/regression/00-sanity/20-if-0-realnode.t @@ -1,57 +1,34 @@ - $ cfgDot 20-if-0-realnode.c | graph-easy --as=boxart - ┌──────────────────────────────────┐ - │ __goblint_dummy_init() │ - └──────────────────────────────────┘ - │ - │ return - ▼ - ┌──────────────────────────────────┐ - │ return of __goblint_dummy_init() │ - └──────────────────────────────────┘ - ┌──────────────────────────────────┐ - │ main() │ - └──────────────────────────────────┘ + $ cfgDot 20-if-0-realnode.c + + $ graph-easy --as=boxart main.dot + ┌───────────────────────────────┐ + │ main() │ + └───────────────────────────────┘ │ │ (body) ▼ - ┌──────────────────────────────────┐ Neg(0) - │ 20-if-0-realnode.c:8:9-8:10 │ ─────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────┘ - └──────────────────────────────────┘ + ┌───────────────────────────────┐ Neg(0) + │ 20-if-0-realnode.c:8:9-8:10 │ ─────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────┘ + └───────────────────────────────┘ │ │ Pos(0) ▼ - ┌──────────────────────────────────┐ - │ 20-if-0-realnode.c:10:9-10:16 │ - │ (synthetic: false) │ - └──────────────────────────────────┘ + ┌───────────────────────────────┐ + │ 20-if-0-realnode.c:10:9-10:16 │ + │ (synthetic: false) │ + └───────────────────────────────┘ │ │ stuff() ▼ - ┌──────────────────────────────────┐ - │ 20-if-0-realnode.c:15:5-15:13 │ - │ (synthetic: false) │ - └──────────────────────────────────┘ + ┌───────────────────────────────┐ + │ 20-if-0-realnode.c:15:5-15:13 │ + │ (synthetic: false) │ + └───────────────────────────────┘ │ │ return 0 ▼ - ┌──────────────────────────────────┐ - │ return of main() │ - └──────────────────────────────────┘ - ┌──────────────────────────────────┐ - │ stuff() │ - └──────────────────────────────────┘ - │ - │ (body) - ▼ - ┌──────────────────────────────────┐ - │ 20-if-0-realnode.c:3:1-3:1 │ - │ (synthetic: false) │ - └──────────────────────────────────┘ - │ - │ return - ▼ - ┌──────────────────────────────────┐ - │ return of stuff() │ - └──────────────────────────────────┘ + ┌───────────────────────────────┐ + │ return of main() │ + └───────────────────────────────┘ diff --git a/tests/regression/00-sanity/21-empty-loops.t b/tests/regression/00-sanity/21-empty-loops.t index ea13f4f52a..e763b2e203 100644 --- a/tests/regression/00-sanity/21-empty-loops.t +++ b/tests/regression/00-sanity/21-empty-loops.t @@ -1,631 +1,393 @@ - $ cfgDot 21-empty-loops.c | graph-easy --as=boxart - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:75:3-75:11 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ suffix() - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:76:1-76:1 │ - │ (synthetic: false) │ ◀┐ - └─────────────────────────────────────────────────────────┘ │ - │ │ - │ return │ - ▼ │ - ┌─────────────────────────────────────────────────────────┐ │ - │ return of f_empty_goto_loop_suffix() │ │ - └─────────────────────────────────────────────────────────┘ │ - ┌─────────────────────────────────────────────────────────┐ │ Neg(1) - │ f_empty_goto_loop_suffix() │ │ - └─────────────────────────────────────────────────────────┘ │ - │ │ - │ (body) │ - ▼ │ - skip ┌─────────────────────────────────────────────────────────┐ │ - ┌────────────────────────────────────────────── │ 21-empty-loops.c:73:3-73:38 │ │ - │ │ (synthetic: false) │ │ - └─────────────────────────────────────────────▶ │ │ ─┘ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ main() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌───────────────────────────────┐ ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:8:7-8:26 │ Pos(r == 0) │ 21-empty-loops.c:7:5-7:11 │ - │ (synthetic: false) │ ◀─────────────────────────────────────────────── │ (synthetic: false) │ - └───────────────────────────────┘ └─────────────────────────────────────────────────────────┘ - │ │ - │ │ Neg(r == 0) - │ ▼ - │ ┌─────────────────────────────────────────────────────────┐ ┌─────────────────────────────┐ - │ │ 21-empty-loops.c:10:5-10:11 │ Pos(r == 1) │ 21-empty-loops.c:11:7-11:27 │ - │ │ (synthetic: false) │ ──────────────▶ │ (synthetic: false) │ - │ └─────────────────────────────────────────────────────────┘ └─────────────────────────────┘ - │ │ │ - │ │ Neg(r == 1) │ - │ ▼ │ - ┌─────────────────────────────┐ │ ┌─────────────────────────────────────────────────────────┐ │ - │ 21-empty-loops.c:14:7-14:33 │ Pos(r == 2) │ │ 21-empty-loops.c:13:5-13:11 │ │ - │ (synthetic: false) │ ◀────────────────┼─────────────────────────────────────────────────────────────────────────────── │ (synthetic: false) │ │ - └─────────────────────────────┘ │ └─────────────────────────────────────────────────────────┘ │ - │ │ │ │ - │ │ │ Neg(r == 2) │ - │ │ ▼ │ - │ │ ┌─────────────────────────────────────────────────────────┐ │ ┌──────────────────────────────┐ - │ │ │ 21-empty-loops.c:16:5-16:11 │ │ Pos(r == 3) │ 21-empty-loops.c:17:7-17:34 │ - │ │ │ (synthetic: false) │ ──────────────────┼──────────────────────────────────────────▶ │ (synthetic: false) │ - │ │ └─────────────────────────────────────────────────────────┘ │ └──────────────────────────────┘ - │ │ │ │ │ - │ │ │ Neg(r == 3) │ │ - │ │ ▼ │ │ - │ │ ┌─────────────────────────────────────────────────────────┐ │ │ - │ │ │ 21-empty-loops.c:19:5-19:11 │ │ │ - │ │ │ (synthetic: false) │ ──────────────────┼──────────────────────────────────────────────┼────────────────────────────────────┐ - │ │ └─────────────────────────────────────────────────────────┘ │ │ │ - │ │ │ │ │ │ - │ │ │ Neg(r == 4) │ │ │ - │ │ ▼ │ │ │ - │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ - │ │ │ 21-empty-loops.c:22:5-22:11 │ │ │ │ - │ │ ┌────────────────────────────────────────────── │ (synthetic: false) │ │ │ │ - │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ - │ │ │ │ │ │ │ - │ │ │ │ Neg(r == 5) │ │ │ - │ │ │ ▼ │ │ │ - │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ - │ │ │ │ 21-empty-loops.c:25:5-25:11 │ │ │ │ - │ ┌───────────────┼────────────────────────────────┼────────────────────────────────────────────── │ (synthetic: false) │ │ │ │ - │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ - │ │ │ │ │ │ │ │ - │ │ │ │ │ Neg(r == 6) │ │ │ - │ │ │ │ ▼ │ │ │ - │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ - │ │ │ │ │ 21-empty-loops.c:28:5-28:11 │ │ │ │ - │ │ │ │ │ (synthetic: false) │ ─┐ │ │ │ - │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ - │ │ │ │ │ │ │ │ │ - │ │ │ │ │ Neg(r == 7) │ │ │ │ - │ │ │ │ ▼ │ │ │ │ - │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ - │ │ │ │ │ 21-empty-loops.c:31:5-31:11 │ │ │ │ │ - │ │ │ │ │ (synthetic: false) │ ─┼────────────────┼──────────────────────────────────────────────┼────────────────────────────────────┼────────────────────────────────────────────┐ - │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ - │ │ │ │ │ │ │ │ │ │ - │ │ │ │ │ Neg(r == 8) │ │ │ │ │ - │ │ │ │ ▼ │ │ │ │ │ - │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ │ - │ │ │ │ │ 21-empty-loops.c:34:5-34:11 │ │ │ │ │ │ - │ │ │ │ │ (synthetic: false) │ ─┼────────────────┼──────────────────────────────┐ │ │ │ - │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ │ - │ │ │ │ │ │ │ │ │ │ │ - │ │ │ │ │ Neg(r == 9) │ │ │ │ │ │ - │ │ │ │ ▼ │ │ │ │ │ │ - │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ │ │ - │ │ │ │ │ 21-empty-loops.c:37:5-37:12 │ │ │ │ │ │ │ - ┌────┼──────────────────────────────┼───────────────┼────────────────────────────────┼────────────────────────────────────────────── │ (synthetic: false) │ │ │ │ │ │ │ - │ │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ │ - │ │ │ │ │ │ │ │ │ │ │ │ - │ │ │ │ │ │ Neg(r == 10) │ │ │ │ │ │ - │ │ │ │ │ ▼ │ │ │ │ │ │ - │ │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ │ │ - │ │ │ │ │ │ 21-empty-loops.c:40:5-40:12 │ │ │ │ │ │ │ - ┌────┼────┼──────────────────────────────┼───────────────┼────────────────────────────────┼────────────────────────────────────────────── │ (synthetic: false) │ │ │ │ │ │ │ - │ │ │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ │ - │ │ │ │ │ │ │ │ │ │ │ │ │ - │ │ │ │ │ │ │ Neg(r == 11) │ │ │ │ │ │ - │ │ │ │ │ │ ▼ │ │ │ │ │ │ - │ │ │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ │ │ - │ │ │ │ │ │ │ 21-empty-loops.c:43:5-43:12 │ │ │ │ │ │ │ - ┌─────────┼────┼────┼──────────────────────────────┼───────────────┼────────────────────────────────┼────────────────────────────────────────────── │ (synthetic: false) │ │ │ └───────────────┼───────────────────────────────┐ │ │ - │ │ │ │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ │ - │ │ │ │ │ │ │ │ │ │ │ │ │ │ - │ │ │ │ │ │ │ │ Neg(r == 12) └────────────────┼──────────────────────────────┐ │ │ │ │ - │ │ │ │ │ │ │ ▼ │ │ │ │ │ │ - │ │ │ │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ │ │ - │ │ │ │ │ │ │ │ 21-empty-loops.c:46:5-46:12 │ │ │ │ │ │ │ - │ ┌────┘ │ │ │ │ │ │ (synthetic: false) │ ─┐ │ │ │ │ │ │ - │ │ │ │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ │ │ - │ │ │ │ │ │ │ │ │ │ │ │ │ │ │ - │ │ ┌────┘ │ │ │ │ │ Pos(r == 13) │ │ │ │ └────┼────────────────────────────────────────────┼──────────────────────────────┐ - │ │ │ │ │ │ │ ▼ │ │ │ │ │ │ │ - │ │ │ │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ │ │ │ - │ │ │ │ │ │ │ │ 21-empty-loops.c:47:7-47:50 │ │ │ │ │ │ │ │ - │ │ │ ┌────┼──────────────────────────────┘ │ │ │ (synthetic: false) │ │ │ └───────────────┼────────────────────────────────────┼────┐ │ │ - │ │ │ │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ │ │ │ │ - │ │ │ │ │ │ │ │ │ │ │ │ │ │ │ - │ │ │ │ │ ┌───────────────┼────────────────────────────────┘ │ f_empty_goto_loop_multiple_semicolon_both() │ Neg(r == 13) │ f_empty_while_loop() │ f_empty_while_loop_suffix() │ │ │ Pos(r == 8) │ - │ │ │ │ │ │ │ ▼ ▼ ▼ ▼ │ │ ▼ │ - │ │ │ │ │ │ │ ┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ │ ┌─────────────────────────────┐ │ Pos(r == 9) - │ │ │ │ │ │ │ f_empty_goto_loop() │ │ │ │ f_empty_goto_loop_semicolon() │ 21-empty-loops.c:32:7-32:36 │ │ - │ │ │ │ │ │ └──────────────────────────────────────────────────────────────────────────────▶ │ │ ◀┼────┼──────────────────────────────────── │ (synthetic: false) │ │ - │ │ │ │ │ │ │ │ │ │ └─────────────────────────────┘ │ - │ │ │ │ │ │ f_empty_goto_loop_suffix() │ │ │ │ │ - │ │ │ │ └──────────────────────────────┼──────────────────────────────────────────────────────────────────────────────────────────────▶ │ │ │ │ │ - │ │ │ │ │ │ │ │ │ │ - │ │ │ │ │ │ │ │ │ ┌─────────────────────────────┐ │ - │ │ │ │ │ │ │ │ │ f_empty_while_loop_semicolon() │ 21-empty-loops.c:35:7-35:37 │ │ - │ │ │ │ │ Pos(r == 5) │ │ ◀┼────┼──────────────────────────────────── │ (synthetic: false) │ ◀┘ - │ │ │ │ │ │ │ │ │ └─────────────────────────────┘ - │ │ │ │ │ ┌───────────────────────────────┐ │ │ │ │ - │ │ │ │ │ │ 21-empty-loops.c:23:7-23:30 │ f_nonempty_while_loop() │ 21-empty-loops.c:51:3-51:11 │ │ │ f_empty_goto_loop_multiple_semicolon_first() - │ │ │ │ └───────────▶ │ (synthetic: false) │ ───────────────────────────────────────────────▶ │ (synthetic: false) │ ◀┼────┼──────────────────────────────────────────────────────────────────────┐ - │ │ │ │ └───────────────────────────────┘ │ │ │ │ │ - │ │ │ │ │ │ │ │ ┌─────────────────────────────┐ │ - │ │ │ │ │ │ │ │ f_empty_goto_loop_multiple() │ 21-empty-loops.c:38:7-38:35 │ │ - │ │ │ │ │ │ ◀┼────┼──────────────────────────────────── │ (synthetic: false) │ │ - │ │ │ │ │ │ │ │ └─────────────────────────────┘ │ - │ │ │ │ ┌───────────────────────────────┐ │ │ │ │ ▲ │ - │ │ │ │ Pos(r == 6) │ 21-empty-loops.c:26:7-26:33 │ f_empty_goto_loop_prefix() │ │ │ │ │ │ - │ │ │ └───────────────────────────────────────────────▶ │ (synthetic: false) │ ───────────────────────────────────────────────▶ │ │ │ │ │ Pos(r == 10) │ - │ │ │ └───────────────────────────────┘ │ │ │ │ │ │ - │ │ │ f_empty_goto_loop_multiple_semicolon_second() │ │ │ │ │ │ - │ │ │ ┌──────────────────────────────────────────────────────────────────────────────▶ │ │ │ │ │ │ - │ │ │ │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ │ │ │ │ - │ │ │ │ │ ▲ ▲ │ │ │ │ - │ │ │ │ │ return 0 │ f_nonempty_goto_loop() │ f_empty_while_loop_prefix() │ │ │ │ - │ │ │ │ ▼ │ │ │ │ │ │ - │ │ │ │ ┌─────────────────────────────────────────────────────────┐ ┌─────────────────────────────┐ │ │ │ │ │ - │ │ │ │ │ return of main() │ │ 21-empty-loops.c:20:7-20:29 │ Pos(r == 4) │ │ │ │ │ - │ │ │ │ │ │ │ (synthetic: false) │ ◀────────────────┼────────────────────────────────────┘ │ │ │ - │ │ │ │ └─────────────────────────────────────────────────────────┘ └─────────────────────────────┘ │ │ │ │ - │ │ │ │ ┌─────────────────────────────────────────────────────────┐ │ │ │ │ - │ │ │ │ │ 21-empty-loops.c:29:7-29:34 │ │ │ │ │ - │ │ │ │ │ (synthetic: false) │ ─────────────────────────────────────────────────────────────────┘ │ │ │ - │ │ │ │ └─────────────────────────────────────────────────────────┘ │ │ │ - │ │ │ │ ▲ Pos(r == 7) │ │ │ - │ │ │ │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ │ │ - │ │ │ │ │ │ - │ │ │ │ │ │ - │ │ └────────────────────────────────────────────────────────┼───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ │ - │ │ │ │ - │ │ │ ┌─────────────────────────────────────────────────────────┐ │ - │ │ │ Pos(r == 11) │ 21-empty-loops.c:41:7-41:51 │ │ - │ └─────────────────────────────────────────────────────────────┼──────────────────────────────────────────────────────────────────────────────▶ │ (synthetic: false) │ ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ - │ │ └─────────────────────────────────────────────────────────┘ - │ │ ┌─────────────────────────────────────────────────────────┐ - │ │ │ 21-empty-loops.c:44:7-44:52 │ - │ └─────────────────────────────────────────────────────────────────────────────── │ (synthetic: false) │ - │ └─────────────────────────────────────────────────────────┘ - │ Pos(r == 12) ▲ - └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ + $ cfgDot 21-empty-loops.c + + $ graph-easy --as=boxart f_empty_goto_loop.dot + ┌───────────────────────────────┐ + │ f_empty_goto_loop() │ + └───────────────────────────────┘ + │ + │ (body) + ▼ + ┌───────────────────────────────┐ skip + │ 21-empty-loops.c:57:3-57:31 │ ───────┐ + │ (synthetic: false) │ │ + │ │ ◀──────┘ + └───────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌───────────────────────────────┐ + │ 21-empty-loops.c:58:1-58:1 │ + │ (synthetic: false) │ + └───────────────────────────────┘ + │ + │ return + ▼ + ┌───────────────────────────────┐ + │ return of f_empty_goto_loop() │ + └───────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_while_loop.dot + ┌────────────────────────────────┐ + │ f_empty_while_loop() │ + └────────────────────────────────┘ + │ + │ (body) + ▼ + ┌────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:62:10-62:11 │ ─────────┐ + │ (synthetic: true) │ │ + │ │ ◀────────┘ + └────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌────────────────────────────────┐ + │ 21-empty-loops.c:63:1-63:1 │ + │ (synthetic: false) │ + └────────────────────────────────┘ + │ + │ return + ▼ + ┌────────────────────────────────┐ + │ return of f_empty_while_loop() │ + └────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_goto_loop_suffix.dot + ┌──────────────────────────────────────┐ + │ 21-empty-loops.c:75:3-75:11 │ + │ (synthetic: false) │ + └──────────────────────────────────────┘ + │ + │ suffix() + ▼ + ┌──────────────────────────────────────┐ + │ 21-empty-loops.c:76:1-76:1 │ + │ (synthetic: false) │ ◀┐ + └──────────────────────────────────────┘ │ + │ │ + │ return │ + ▼ │ + ┌──────────────────────────────────────┐ │ + │ return of f_empty_goto_loop_suffix() │ │ + └──────────────────────────────────────┘ │ + ┌──────────────────────────────────────┐ │ Neg(1) + │ f_empty_goto_loop_suffix() │ │ + └──────────────────────────────────────┘ │ + │ │ + │ (body) │ + ▼ │ + skip ┌──────────────────────────────────────┐ │ + ┌─────── │ 21-empty-loops.c:73:3-73:38 │ │ + │ │ (synthetic: false) │ │ + └──────▶ │ │ ─┘ + └──────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_while_loop_suffix.dot + ┌───────────────────────────────────────┐ + │ f_empty_while_loop_suffix() │ + └───────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌───────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:80:10-80:11 │ ─────────┐ + │ (synthetic: true) │ │ + │ │ ◀────────┘ + └───────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌───────────────────────────────────────┐ + │ 21-empty-loops.c:82:3-82:11 │ + │ (synthetic: false) │ + └───────────────────────────────────────┘ + │ + │ suffix() + ▼ + ┌───────────────────────────────────────┐ + │ 21-empty-loops.c:83:1-83:1 │ + │ (synthetic: false) │ + └───────────────────────────────────────┘ + │ + │ return + ▼ + ┌───────────────────────────────────────┐ + │ return of f_empty_while_loop_suffix() │ + └───────────────────────────────────────┘ + + $ graph-easy --as=boxart f_nonempty_goto_loop.dot + ┌──────────────────────────────────┐ + │ f_nonempty_goto_loop() │ + └──────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────────────────┐ body() + │ 21-empty-loops.c:93:3-93:9 │ ─────────┐ + │ (synthetic: false) │ │ + │ │ ◀────────┘ + └──────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌──────────────────────────────────┐ + │ 21-empty-loops.c:95:1-95:1 │ + │ (synthetic: false) │ + └──────────────────────────────────┘ + │ + │ return + ▼ + ┌──────────────────────────────────┐ + │ return of f_nonempty_goto_loop() │ + └──────────────────────────────────┘ + + $ graph-easy --as=boxart f_nonempty_while_loop.dot - ┌─────────────────────────────────────────────────────────┐ - │ f_empty_while_loop_suffix() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ Pos(1) - │ 21-empty-loops.c:80:10-80:11 │ ─────────────┐ - │ (synthetic: true) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:82:3-82:11 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ suffix() - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:83:1-83:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_empty_while_loop_suffix() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ f_empty_goto_loop_prefix() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:112:3-112:11 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ prefix() - ▼ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:115:3-115:38 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:116:1-116:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_empty_goto_loop_prefix() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ f_empty_while_loop_prefix() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:120:3-120:11 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ prefix() - ▼ - ┌─────────────────────────────────────────────────────────┐ Pos(1) - │ 21-empty-loops.c:122:10-122:11 │ ─────────────┐ - │ (synthetic: true) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:123:1-123:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_empty_while_loop_prefix() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ f_empty_goto_loop() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:57:3-57:31 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:58:1-58:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_empty_goto_loop() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ f_empty_while_loop() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ Pos(1) - │ 21-empty-loops.c:62:10-62:11 │ ─────────────┐ - │ (synthetic: true) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:63:1-63:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_empty_while_loop() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ f_nonempty_goto_loop() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ body() - │ 21-empty-loops.c:93:3-93:9 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:95:1-95:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_nonempty_goto_loop() │ - └─────────────────────────────────────────────────────────┘ - - ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ - │ │ - │ ┌─────────────────────────────────────────────────────────┐ │ - │ │ f_nonempty_while_loop() │ │ - │ └─────────────────────────────────────────────────────────┘ │ - │ │ │ body() - │ │ (body) │ - │ ▼ │ - ┌───────────────────────────────┐ ┌─────────────────────────────────────────────────────────┐ │ - │ 21-empty-loops.c:101:5-101:11 │ Pos(1) │ 21-empty-loops.c:99:10-99:11 │ │ - │ (synthetic: false) │ ◀─────────────────────────────────────────────── │ (synthetic: true) │ ◀┘ - └───────────────────────────────┘ └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:103:1-103:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_nonempty_while_loop() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ f_empty_goto_loop_semicolon() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:127:1-128:3 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:131:1-131:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_empty_goto_loop_semicolon() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ f_empty_while_loop_semicolon() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ Pos(1) - │ 21-empty-loops.c:135:10-135:11 │ ─────────────┐ - │ (synthetic: true) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:138:1-138:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_empty_while_loop_semicolon() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ f_empty_goto_loop_multiple() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:143:3-143:42 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:146:1-146:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_empty_goto_loop_multiple() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ f_empty_goto_loop_multiple_semicolon_first() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:150:1-151:3 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:155:1-155:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_empty_goto_loop_multiple_semicolon_first() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ f_empty_goto_loop_multiple_semicolon_second() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:160:3-160:59 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:164:1-164:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_empty_goto_loop_multiple_semicolon_second() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ f_empty_goto_loop_multiple_semicolon_both() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:168:1-169:3 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:174:1-174:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of f_empty_goto_loop_multiple_semicolon_both() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ suffix() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:68:1-68:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of suffix() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ body() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:88:1-88:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of body() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ prefix() │ - └─────────────────────────────────────────────────────────┘ - │ - │ (body) - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:108:1-108:1 │ - │ (synthetic: false) │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of prefix() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ - │ __goblint_dummy_init() │ - └─────────────────────────────────────────────────────────┘ - │ - │ return - ▼ - ┌─────────────────────────────────────────────────────────┐ - │ return of __goblint_dummy_init() │ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:130:3-130:41 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:145:3-145:42 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:152:3-152:58 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:154:3-154:58 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:161:1-162:3 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:163:3-163:59 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:170:3-170:57 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:171:1-172:3 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:173:3-173:57 │ ─────────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────────┘ - └─────────────────────────────────────────────────────────┘ + ┌────────────────────────────────────────────────────────────────────────────────┐ + │ │ + │ ┌───────────────────────────────────┐ │ + │ │ f_nonempty_while_loop() │ │ + │ └───────────────────────────────────┘ │ + │ │ │ body() + │ │ (body) │ + │ ▼ │ + ┌───────────────────────────────┐ ┌───────────────────────────────────┐ │ + │ 21-empty-loops.c:101:5-101:11 │ Pos(1) │ 21-empty-loops.c:99:10-99:11 │ │ + │ (synthetic: false) │ ◀──────── │ (synthetic: true) │ ◀┘ + └───────────────────────────────┘ └───────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌───────────────────────────────────┐ + │ 21-empty-loops.c:103:1-103:1 │ + │ (synthetic: false) │ + └───────────────────────────────────┘ + │ + │ return + ▼ + ┌───────────────────────────────────┐ + │ return of f_nonempty_while_loop() │ + └───────────────────────────────────┘ + + + $ graph-easy --as=boxart f_empty_goto_loop_prefix.dot + ┌──────────────────────────────────────┐ + │ f_empty_goto_loop_prefix() │ + └──────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────────────────────┐ + │ 21-empty-loops.c:112:3-112:11 │ + │ (synthetic: false) │ + └──────────────────────────────────────┘ + │ + │ prefix() + ▼ + ┌──────────────────────────────────────┐ skip + │ 21-empty-loops.c:115:3-115:38 │ ───────┐ + │ (synthetic: false) │ │ + │ │ ◀──────┘ + └──────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌──────────────────────────────────────┐ + │ 21-empty-loops.c:116:1-116:1 │ + │ (synthetic: false) │ + └──────────────────────────────────────┘ + │ + │ return + ▼ + ┌──────────────────────────────────────┐ + │ return of f_empty_goto_loop_prefix() │ + └──────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_while_loop_prefix.dot + ┌───────────────────────────────────────┐ + │ f_empty_while_loop_prefix() │ + └───────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌───────────────────────────────────────┐ + │ 21-empty-loops.c:120:3-120:11 │ + │ (synthetic: false) │ + └───────────────────────────────────────┘ + │ + │ prefix() + ▼ + ┌───────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:122:10-122:11 │ ─────────┐ + │ (synthetic: true) │ │ + │ │ ◀────────┘ + └───────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌───────────────────────────────────────┐ + │ 21-empty-loops.c:123:1-123:1 │ + │ (synthetic: false) │ + └───────────────────────────────────────┘ + │ + │ return + ▼ + ┌───────────────────────────────────────┐ + │ return of f_empty_while_loop_prefix() │ + └───────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_goto_loop_semicolon.dot + ┌─────────────────────────────────────────┐ + │ f_empty_goto_loop_semicolon() │ + └─────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────┐ skip + │ 21-empty-loops.c:127:1-128:3 │ ───────┐ + │ (synthetic: false) │ │ + │ │ ◀──────┘ + └─────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────┐ + │ 21-empty-loops.c:131:1-131:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────┐ + │ return of f_empty_goto_loop_semicolon() │ + └─────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_while_loop_semicolon.dot + ┌──────────────────────────────────────────┐ + │ f_empty_while_loop_semicolon() │ + └──────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:135:10-135:11 │ ─────────┐ + │ (synthetic: true) │ │ + │ │ ◀────────┘ + └──────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌──────────────────────────────────────────┐ + │ 21-empty-loops.c:138:1-138:1 │ + │ (synthetic: false) │ + └──────────────────────────────────────────┘ + │ + │ return + ▼ + ┌──────────────────────────────────────────┐ + │ return of f_empty_while_loop_semicolon() │ + └──────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_goto_loop_multiple.dot + ┌────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple() │ + └────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌────────────────────────────────────────┐ skip + │ 21-empty-loops.c:143:3-143:42 │ ───────┐ + │ (synthetic: false) │ │ + │ │ ◀──────┘ + └────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌────────────────────────────────────────┐ + │ 21-empty-loops.c:146:1-146:1 │ + │ (synthetic: false) │ + └────────────────────────────────────────┘ + │ + │ return + ▼ + ┌────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple() │ + └────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_goto_loop_multiple_semicolon_first.dot + ┌────────────────────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple_semicolon_first() │ + └────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:150:1-151:3 │ ───────┐ + │ (synthetic: false) │ │ + │ │ ◀──────┘ + └────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:155:1-155:1 │ + │ (synthetic: false) │ + └────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌────────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple_semicolon_first() │ + └────────────────────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_goto_loop_multiple_semicolon_second.dot + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple_semicolon_second() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:160:3-160:59 │ ───────┐ + │ (synthetic: false) │ │ + │ │ ◀──────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:164:1-164:1 │ + │ (synthetic: false) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple_semicolon_second() │ + └─────────────────────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_goto_loop_multiple_semicolon_both.dot + ┌───────────────────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple_semicolon_both() │ + └───────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌───────────────────────────────────────────────────────┐ skip + │ 21-empty-loops.c:168:1-169:3 │ ───────┐ + │ (synthetic: false) │ │ + │ │ ◀──────┘ + └───────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌───────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:174:1-174:1 │ + │ (synthetic: false) │ + └───────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌───────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple_semicolon_both() │ + └───────────────────────────────────────────────────────┘ diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index 429ea4f8a1..d37010657f 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -1,55 +1,40 @@ - $ cfgDot foo.c | graph-easy --as=boxart - ┌──────────────────────────────────┐ - │ __goblint_dummy_init() │ - └──────────────────────────────────┘ - │ - │ return - ▼ - ┌──────────────────────────────────┐ - │ return of __goblint_dummy_init() │ - └──────────────────────────────────┘ - ┌──────────────────────────────────┐ - │ main() │ - └──────────────────────────────────┘ - │ - │ (body) - ▼ - ┌──────────────────────────────────┐ - │ foo.c:2:7-2:12 │ - │ (synthetic: false) │ - └──────────────────────────────────┘ - │ - │ a = 1 - ▼ - ┌──────────────────────────────────┐ - │ foo.c:2:14-2:19 │ - │ (synthetic: false) │ - └──────────────────────────────────┘ - │ - │ b = 1 - ▼ - ┌────────────────────┐ ┌──────────────────────────────────┐ - │ foo.c:7:3-7:11 │ Neg(a > 0) │ foo.c:3:10-3:20 │ - ┌──────▶ │ (synthetic: false) │ ◀──────────── │ (synthetic: true) │ ◀┐ - │ └────────────────────┘ └──────────────────────────────────┘ │ - │ │ │ │ - │ │ return 0 │ Pos(a > 0) │ - │ ▼ ▼ │ - │ Neg(b) ┌────────────────────┐ ┌──────────────────────────────────┐ │ - │ │ return of main() │ │ foo.c:3:10-3:20 │ │ - │ │ │ ┌─────────── │ (synthetic: true) │ │ - │ └────────────────────┘ │ └──────────────────────────────────┘ │ - │ │ │ │ - └────────────────────────────────┘ │ Pos(b) │ b = b - 1 - ▼ │ - ┌──────────────────────────────────┐ │ - │ foo.c:4:5-4:8 │ │ - │ (synthetic: false) │ │ - └──────────────────────────────────┘ │ - │ │ - │ a = a + 1 │ - ▼ │ - ┌──────────────────────────────────┐ │ - │ foo.c:5:5-5:8 │ │ - │ (synthetic: false) │ ─┘ - └──────────────────────────────────┘ + $ cfgDot foo.c + + $ graph-easy --as=boxart main.dot + ┌────────────────────┐ + │ main() │ + └────────────────────┘ + │ + │ (body) + ▼ + ┌────────────────────┐ + │ foo.c:2:7-2:12 │ + │ (synthetic: false) │ + └────────────────────┘ + │ + │ + ▼ + ┌────────────────────┐ + │ foo.c:3:10-3:20 │ + ┌────────────────────────────▶ │ (synthetic: true) │ ─┐ + │ └────────────────────┘ │ + │ │ │ + │ │ Pos(a > 0) │ + │ ▼ │ + ┌────────────────────┐ ┌────────────────────┐ │ + │ foo.c:4:5-4:8 │ Pos(b) │ foo.c:3:10-3:20 │ │ + │ (synthetic: false) │ ◀──────── │ (synthetic: true) │ │ Neg(a > 0) + └────────────────────┘ └────────────────────┘ │ + │ │ + │ Neg(b) │ + ▼ │ + ┌────────────────────┐ │ + │ foo.c:7:3-7:11 │ │ + │ (synthetic: false) │ ◀┘ + └────────────────────┘ + │ + │ return 0 + ▼ + ┌────────────────────┐ + │ return of main() │ + └────────────────────┘ diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml index ef13cbf763..20c05020b1 100644 --- a/tests/regression/cfg/util/cfgDot.ml +++ b/tests/regression/cfg/util/cfgDot.ml @@ -1,14 +1,17 @@ -open Goblint_lib -open CfgTools - let main () = Cilfacade.init (); let ast = Cilfacade.getAST (Fpath.v Sys.argv.(1)) in - CilCfg.createCFG ast; - let _cfgF, cfgB, _skippedByEdge = CfgTools.createCFG ast in + (* Part of CilCfg.createCFG *) + GoblintCil.iterGlobals ast (function + | GFun (fd, _) -> + GoblintCil.prepareCFG fd; + GoblintCil.computeCFGInfo fd true + | _ -> () + ); + let (module Cfg) = CfgTools.compute_cfg ast in - let module NoExtraNodeStyles = + let module LocationExtraNodeStyles = struct let defaultNodeStyles = [] let extraNodeStyles = function @@ -18,9 +21,16 @@ let main () = | _ -> [] end in - let iter_edges f = H.iter (fun n es -> List.iter (f n) es) cfgB in - let ppf = Format.std_formatter in - fprint_dot (module CfgPrinters (NoExtraNodeStyles)) iter_edges ppf; - Format.pp_print_flush ppf () + + GoblintCil.iterGlobals ast (function + | GFun (fd, _) -> + let out = open_out (fd.svar.vname ^ ".dot") in + let iter_edges = CfgTools.iter_fd_edges (module Cfg) fd in + let ppf = Format.formatter_of_out_channel out in + CfgTools.fprint_dot (module CfgTools.CfgPrinters (LocationExtraNodeStyles)) iter_edges ppf; + Format.pp_print_flush ppf (); + close_out out + | _ -> () + ) let () = main () diff --git a/tests/regression/cfg/util/dune b/tests/regression/cfg/util/dune index 5f71944874..b0a04f0ef5 100644 --- a/tests/regression/cfg/util/dune +++ b/tests/regression/cfg/util/dune @@ -1,7 +1,8 @@ (executable (name cfgDot) (libraries - goblint_lib + goblint-cil + goblint_common fpath goblint.sites.dune goblint.build-info.dune) From a1483d6c8644186a5f7446249f40b93b71a3d380 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 9 Feb 2024 15:10:15 +0200 Subject: [PATCH 08/23] Fix instructions in CFG testing --- tests/regression/cfg/foo.t/run.t | 82 ++++++++++++++++------------- tests/regression/cfg/util/cfgDot.ml | 19 +++++++ 2 files changed, 64 insertions(+), 37 deletions(-) diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index d37010657f..34852c803c 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -1,40 +1,48 @@ $ cfgDot foo.c $ graph-easy --as=boxart main.dot - ┌────────────────────┐ - │ main() │ - └────────────────────┘ - │ - │ (body) - ▼ - ┌────────────────────┐ - │ foo.c:2:7-2:12 │ - │ (synthetic: false) │ - └────────────────────┘ - │ - │ - ▼ - ┌────────────────────┐ - │ foo.c:3:10-3:20 │ - ┌────────────────────────────▶ │ (synthetic: true) │ ─┐ - │ └────────────────────┘ │ - │ │ │ - │ │ Pos(a > 0) │ - │ ▼ │ - ┌────────────────────┐ ┌────────────────────┐ │ - │ foo.c:4:5-4:8 │ Pos(b) │ foo.c:3:10-3:20 │ │ - │ (synthetic: false) │ ◀──────── │ (synthetic: true) │ │ Neg(a > 0) - └────────────────────┘ └────────────────────┘ │ - │ │ - │ Neg(b) │ - ▼ │ - ┌────────────────────┐ │ - │ foo.c:7:3-7:11 │ │ - │ (synthetic: false) │ ◀┘ - └────────────────────┘ - │ - │ return 0 - ▼ - ┌────────────────────┐ - │ return of main() │ - └────────────────────┘ + ┌────────────────────┐ + │ main() │ + └────────────────────┘ + │ + │ (body) + ▼ + ┌────────────────────┐ + │ foo.c:2:7-2:12 │ + │ (synthetic: false) │ + └────────────────────┘ + │ + │ a = 1 + ▼ + ┌────────────────────┐ + │ foo.c:2:14-2:19 │ + │ (synthetic: false) │ + └────────────────────┘ + │ + │ b = 1 + ▼ + ┌────────────────────┐ ┌────────────────────┐ + │ foo.c:7:3-7:11 │ Neg(a > 0) │ foo.c:3:10-3:20 │ + ┌──────▶ │ (synthetic: false) │ ◀──────────── │ (synthetic: true) │ ◀┐ + │ └────────────────────┘ └────────────────────┘ │ + │ │ │ │ + │ │ return 0 │ Pos(a > 0) │ + │ ▼ ▼ │ + │ Neg(b) ┌────────────────────┐ ┌────────────────────┐ │ + │ │ return of main() │ │ foo.c:3:10-3:20 │ │ + │ │ │ ┌─────────── │ (synthetic: true) │ │ + │ └────────────────────┘ │ └────────────────────┘ │ + │ │ │ │ + └────────────────────────────────┘ │ Pos(b) │ b = b - 1 + ▼ │ + ┌────────────────────┐ │ + │ foo.c:4:5-4:8 │ │ + │ (synthetic: false) │ │ + └────────────────────┘ │ + │ │ + │ a = a + 1 │ + ▼ │ + ┌────────────────────┐ │ + │ foo.c:5:5-5:8 │ │ + │ (synthetic: false) │ ─┘ + └────────────────────┘ diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml index 20c05020b1..13725bb97d 100644 --- a/tests/regression/cfg/util/cfgDot.ml +++ b/tests/regression/cfg/util/cfgDot.ml @@ -1,7 +1,26 @@ +(* Part of CilCfg *) +class allBBVisitor = object (* puts every instruction into its own basic block *) + inherit GoblintCil.nopCilVisitor + method! vstmt s = + match s.skind with + | Instr(il) -> + let list_of_stmts = + List.map (fun one_inst -> GoblintCil.mkStmtOneInstr one_inst) il in + let block = GoblintCil.mkBlock list_of_stmts in + ChangeDoChildrenPost(s, (fun _ -> s.skind <- Block(block); s)) + | _ -> DoChildren + + method! vvdec _ = SkipChildren + method! vexpr _ = SkipChildren + method! vlval _ = SkipChildren + method! vtype _ = SkipChildren +end + let main () = Cilfacade.init (); let ast = Cilfacade.getAST (Fpath.v Sys.argv.(1)) in + GoblintCil.visitCilFileSameGlobals (new allBBVisitor) ast; (* Part of CilCfg.createCFG *) GoblintCil.iterGlobals ast (function | GFun (fd, _) -> From 361af131c0bf31bcd07ffd3bc902994422f71457 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 9 Feb 2024 15:27:12 +0200 Subject: [PATCH 09/23] More detailed location output in CFG tests --- src/common/util/cilLocation.ml | 52 +++ tests/regression/00-sanity/19-if-0.t | 60 ++-- tests/regression/00-sanity/20-if-0-realnode.t | 39 ++- tests/regression/00-sanity/21-empty-loops.t | 324 +++++++++--------- tests/regression/cfg/foo.t/run.t | 90 ++--- tests/regression/cfg/util/cfgDot.ml | 25 +- 6 files changed, 334 insertions(+), 256 deletions(-) create mode 100644 src/common/util/cilLocation.ml diff --git a/src/common/util/cilLocation.ml b/src/common/util/cilLocation.ml new file mode 100644 index 0000000000..6f9a3ce7c4 --- /dev/null +++ b/src/common/util/cilLocation.ml @@ -0,0 +1,52 @@ +open GoblintCil + +type locs = { + loc: location; + eloc: location; +} + +let get_labelLoc = function + | Label (_, loc, _) -> {loc; eloc = locUnknown} + | Case (_, loc, eloc) -> {loc; eloc} + | CaseRange (_, _, loc, eloc) -> {loc; eloc} + | Default (loc, eloc) -> {loc; eloc} + +(* let rec get_labelsLoc = function + | [] -> {loc = locUnknown; eloc = locUnknown} + | label :: labels -> + let loc = get_labelLoc label in + if CilType.Location.equal loc Cil.locUnknown then + get_labelsLoc labels (* maybe another label has known location *) + else + loc *) + +(** Following functions are similar to [Cil] versions, but return expression location instead of entire statement location, where possible. *) +(* Ideally we would have both copies of the functions available, but UpdateCil would have to be adapted per-stmtkind/instr to store and update either one or two locations. *) + +(** Get locations for {!Cil.instr}. *) +let get_instrLoc = function + | Set (_, _, loc, eloc) -> {loc; eloc} + | Call (_, _, _, loc, eloc) -> {loc; eloc} + | Asm (_, _, _, _, _, loc) -> {loc; eloc = locUnknown} + | VarDecl (_, loc) -> {loc; eloc = locUnknown} + +(** Get locations for {!Cil.stmt}. *) +(* confusingly {!Cil.get_stmtLoc} works on stmtkind instead *) +let rec get_stmtLoc stmt: locs = + match stmt.skind with + (* no stmtkind/instr location in these cases, so try labels instead *) + | Instr [] + | Block {bstmts = []; _} -> + (* get_labelsLoc stmt.labels *) + {loc = locUnknown; eloc = locUnknown} + + | Instr (hd :: _) -> get_instrLoc hd + | Return (_, loc) -> {loc; eloc = locUnknown} + | Goto (_, loc) -> {loc; eloc = locUnknown} + | ComputedGoto (_, loc) -> {loc; eloc = locUnknown} + | Break loc -> {loc; eloc = locUnknown} + | Continue loc -> {loc; eloc = locUnknown} + | If (_, _, _, loc, eloc) -> {loc; eloc} + | Switch (_, _, _, loc, eloc) -> {loc; eloc} + | Loop (_, loc, eloc, _, _) -> {loc; eloc} + | Block {bstmts = hd :: _; _} -> get_stmtLoc hd diff --git a/tests/regression/00-sanity/19-if-0.t b/tests/regression/00-sanity/19-if-0.t index 0814240a90..f847d75446 100644 --- a/tests/regression/00-sanity/19-if-0.t +++ b/tests/regression/00-sanity/19-if-0.t @@ -1,33 +1,33 @@ $ cfgDot 19-if-0.c $ graph-easy --as=boxart main.dot - ┌──────────────────────┐ - │ main() │ - └──────────────────────┘ - │ - │ (body) - ▼ - ┌──────────────────────┐ ┌──────────────────────┐ - │ 19-if-0.c:15:9-15:27 │ Neg(0) │ 19-if-0.c:9:9-9:10 │ - │ (synthetic: false) │ ◀──────────────────── │ (synthetic: false) │ - └──────────────────────┘ └──────────────────────┘ - │ │ - │ │ Pos(0) - │ ▼ - │ ┌──────────────────────┐ - │ │ 19-if-0.c:11:9-11:16 │ - │ │ (synthetic: false) │ - │ └──────────────────────┘ - │ │ - │ │ stuff() - │ ▼ - │ ┌──────────────────────┐ - │ __goblint_check(1) │ 19-if-0.c:17:5-17:13 │ - └──────────────────────────────────────────▶ │ (synthetic: false) │ - └──────────────────────┘ - │ - │ return 0 - ▼ - ┌──────────────────────┐ - │ return of main() │ - └──────────────────────┘ + ┌────────────────────────┐ + │ main() │ + └────────────────────────┘ + │ + │ (body) + ▼ + ┌────────────────────────┐ ┌────────────────────────┐ + │ 19-if-0.c:15:9-15:27 │ Neg(0) │ 19-if-0.c:9:5-16:5 │ + │ (19-if-0.c:15:9-15:27) │ ◀──────────────────── │ (19-if-0.c:9:9-9:10) │ + └────────────────────────┘ └────────────────────────┘ + │ │ + │ │ Pos(0) + │ ▼ + │ ┌────────────────────────┐ + │ │ 19-if-0.c:11:9-11:16 │ + │ │ (19-if-0.c:11:9-11:16) │ + │ └────────────────────────┘ + │ │ + │ │ stuff() + │ ▼ + │ ┌────────────────────────┐ + │ __goblint_check(1) │ 19-if-0.c:17:5-17:13 │ + └────────────────────────────────────────────▶ │ (unknown) │ + └────────────────────────┘ + │ + │ return 0 + ▼ + ┌────────────────────────┐ + │ return of main() │ + └────────────────────────┘ diff --git a/tests/regression/00-sanity/20-if-0-realnode.t b/tests/regression/00-sanity/20-if-0-realnode.t index 1363b3d26e..06a0bba865 100644 --- a/tests/regression/00-sanity/20-if-0-realnode.t +++ b/tests/regression/00-sanity/20-if-0-realnode.t @@ -1,34 +1,35 @@ $ cfgDot 20-if-0-realnode.c $ graph-easy --as=boxart main.dot - ┌───────────────────────────────┐ - │ main() │ - └───────────────────────────────┘ + ┌─────────────────────────────────┐ + │ main() │ + └─────────────────────────────────┘ │ │ (body) ▼ - ┌───────────────────────────────┐ Neg(0) - │ 20-if-0-realnode.c:8:9-8:10 │ ─────────┐ - │ (synthetic: false) │ │ - │ │ ◀────────┘ - └───────────────────────────────┘ + ┌─────────────────────────────────┐ + │ 20-if-0-realnode.c:8:5-14:5 │ Neg(0) + │ (20-if-0-realnode.c:8:9-8:10) │ ─────────┐ + │ [20-if-0-realnode.c:7:5-8:5 │ │ + │ (unknown)] │ ◀────────┘ + └─────────────────────────────────┘ │ │ Pos(0) ▼ - ┌───────────────────────────────┐ - │ 20-if-0-realnode.c:10:9-10:16 │ - │ (synthetic: false) │ - └───────────────────────────────┘ + ┌─────────────────────────────────┐ + │ 20-if-0-realnode.c:10:9-10:16 │ + │ (20-if-0-realnode.c:10:9-10:16) │ + └─────────────────────────────────┘ │ │ stuff() ▼ - ┌───────────────────────────────┐ - │ 20-if-0-realnode.c:15:5-15:13 │ - │ (synthetic: false) │ - └───────────────────────────────┘ + ┌─────────────────────────────────┐ + │ 20-if-0-realnode.c:15:5-15:13 │ + │ (unknown) │ + └─────────────────────────────────┘ │ │ return 0 ▼ - ┌───────────────────────────────┐ - │ return of main() │ - └───────────────────────────────┘ + ┌─────────────────────────────────┐ + │ return of main() │ + └─────────────────────────────────┘ diff --git a/tests/regression/00-sanity/21-empty-loops.t b/tests/regression/00-sanity/21-empty-loops.t index e763b2e203..202a4d1071 100644 --- a/tests/regression/00-sanity/21-empty-loops.t +++ b/tests/regression/00-sanity/21-empty-loops.t @@ -2,22 +2,23 @@ $ graph-easy --as=boxart f_empty_goto_loop.dot ┌───────────────────────────────┐ - │ f_empty_goto_loop() │ + │ f_empty_goto_loop() │ └───────────────────────────────┘ │ │ (body) ▼ - ┌───────────────────────────────┐ skip - │ 21-empty-loops.c:57:3-57:31 │ ───────┐ - │ (synthetic: false) │ │ - │ │ ◀──────┘ + ┌───────────────────────────────┐ + │ 21-empty-loops.c:57:3-57:31 │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:56:1-57:3 │ │ + │ (unknown)] │ ◀──────┘ └───────────────────────────────┘ │ │ Neg(1) ▼ ┌───────────────────────────────┐ - │ 21-empty-loops.c:58:1-58:1 │ - │ (synthetic: false) │ + │ 21-empty-loops.c:58:1-58:1 │ + │ (unknown) │ └───────────────────────────────┘ │ │ return @@ -27,42 +28,42 @@ └───────────────────────────────┘ $ graph-easy --as=boxart f_empty_while_loop.dot - ┌────────────────────────────────┐ - │ f_empty_while_loop() │ - └────────────────────────────────┘ + ┌────────────────────────────────────────────┐ + │ f_empty_while_loop() │ + └────────────────────────────────────────────┘ │ │ (body) ▼ - ┌────────────────────────────────┐ Pos(1) - │ 21-empty-loops.c:62:10-62:11 │ ─────────┐ - │ (synthetic: true) │ │ - │ │ ◀────────┘ - └────────────────────────────────┘ + ┌────────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:62:3-62:14 (synthetic) │ ─────────┐ + │ (21-empty-loops.c:62:10-62:11 (synthetic)) │ │ + │ │ ◀────────┘ + └────────────────────────────────────────────┘ │ │ Neg(1) ▼ - ┌────────────────────────────────┐ - │ 21-empty-loops.c:63:1-63:1 │ - │ (synthetic: false) │ - └────────────────────────────────┘ + ┌────────────────────────────────────────────┐ + │ 21-empty-loops.c:63:1-63:1 │ + │ (unknown) │ + └────────────────────────────────────────────┘ │ │ return ▼ - ┌────────────────────────────────┐ - │ return of f_empty_while_loop() │ - └────────────────────────────────┘ + ┌────────────────────────────────────────────┐ + │ return of f_empty_while_loop() │ + └────────────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_goto_loop_suffix.dot ┌──────────────────────────────────────┐ - │ 21-empty-loops.c:75:3-75:11 │ - │ (synthetic: false) │ + │ 21-empty-loops.c:75:3-75:11 │ + │ (21-empty-loops.c:75:3-75:11) │ └──────────────────────────────────────┘ │ │ suffix() ▼ ┌──────────────────────────────────────┐ - │ 21-empty-loops.c:76:1-76:1 │ - │ (synthetic: false) │ ◀┐ + │ 21-empty-loops.c:76:1-76:1 │ + │ (unknown) │ ◀┐ └──────────────────────────────────────┘ │ │ │ │ return │ @@ -71,68 +72,69 @@ │ return of f_empty_goto_loop_suffix() │ │ └──────────────────────────────────────┘ │ ┌──────────────────────────────────────┐ │ Neg(1) - │ f_empty_goto_loop_suffix() │ │ + │ f_empty_goto_loop_suffix() │ │ └──────────────────────────────────────┘ │ │ │ │ (body) │ ▼ │ - skip ┌──────────────────────────────────────┐ │ - ┌─────── │ 21-empty-loops.c:73:3-73:38 │ │ - │ │ (synthetic: false) │ │ - └──────▶ │ │ ─┘ + ┌──────────────────────────────────────┐ │ + skip │ 21-empty-loops.c:73:3-73:38 │ │ + ┌─────── │ (unknown) │ │ + │ │ [21-empty-loops.c:72:1-73:3 │ │ + └──────▶ │ (unknown)] │ ─┘ └──────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_while_loop_suffix.dot - ┌───────────────────────────────────────┐ - │ f_empty_while_loop_suffix() │ - └───────────────────────────────────────┘ + ┌────────────────────────────────────────────┐ + │ f_empty_while_loop_suffix() │ + └────────────────────────────────────────────┘ │ │ (body) ▼ - ┌───────────────────────────────────────┐ Pos(1) - │ 21-empty-loops.c:80:10-80:11 │ ─────────┐ - │ (synthetic: true) │ │ - │ │ ◀────────┘ - └───────────────────────────────────────┘ + ┌────────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:80:3-80:14 (synthetic) │ ─────────┐ + │ (21-empty-loops.c:80:10-80:11 (synthetic)) │ │ + │ │ ◀────────┘ + └────────────────────────────────────────────┘ │ │ Neg(1) ▼ - ┌───────────────────────────────────────┐ - │ 21-empty-loops.c:82:3-82:11 │ - │ (synthetic: false) │ - └───────────────────────────────────────┘ + ┌────────────────────────────────────────────┐ + │ 21-empty-loops.c:82:3-82:11 │ + │ (21-empty-loops.c:82:3-82:11) │ + └────────────────────────────────────────────┘ │ │ suffix() ▼ - ┌───────────────────────────────────────┐ - │ 21-empty-loops.c:83:1-83:1 │ - │ (synthetic: false) │ - └───────────────────────────────────────┘ + ┌────────────────────────────────────────────┐ + │ 21-empty-loops.c:83:1-83:1 │ + │ (unknown) │ + └────────────────────────────────────────────┘ │ │ return ▼ - ┌───────────────────────────────────────┐ - │ return of f_empty_while_loop_suffix() │ - └───────────────────────────────────────┘ + ┌────────────────────────────────────────────┐ + │ return of f_empty_while_loop_suffix() │ + └────────────────────────────────────────────┘ $ graph-easy --as=boxart f_nonempty_goto_loop.dot ┌──────────────────────────────────┐ - │ f_nonempty_goto_loop() │ + │ f_nonempty_goto_loop() │ └──────────────────────────────────┘ │ │ (body) ▼ ┌──────────────────────────────────┐ body() - │ 21-empty-loops.c:93:3-93:9 │ ─────────┐ - │ (synthetic: false) │ │ + │ 21-empty-loops.c:93:3-93:9 │ ─────────┐ + │ (21-empty-loops.c:93:3-93:9) │ │ │ │ ◀────────┘ └──────────────────────────────────┘ │ │ Neg(1) ▼ ┌──────────────────────────────────┐ - │ 21-empty-loops.c:95:1-95:1 │ - │ (synthetic: false) │ + │ 21-empty-loops.c:95:1-95:1 │ + │ (unknown) │ └──────────────────────────────────┘ │ │ return @@ -143,58 +145,59 @@ $ graph-easy --as=boxart f_nonempty_while_loop.dot - ┌────────────────────────────────────────────────────────────────────────────────┐ - │ │ - │ ┌───────────────────────────────────┐ │ - │ │ f_nonempty_while_loop() │ │ - │ └───────────────────────────────────┘ │ - │ │ │ body() - │ │ (body) │ - │ ▼ │ - ┌───────────────────────────────┐ ┌───────────────────────────────────┐ │ - │ 21-empty-loops.c:101:5-101:11 │ Pos(1) │ 21-empty-loops.c:99:10-99:11 │ │ - │ (synthetic: false) │ ◀──────── │ (synthetic: true) │ ◀┘ - └───────────────────────────────┘ └───────────────────────────────────┘ - │ - │ Neg(1) - ▼ - ┌───────────────────────────────────┐ - │ 21-empty-loops.c:103:1-103:1 │ - │ (synthetic: false) │ - └───────────────────────────────────┘ - │ - │ return - ▼ - ┌───────────────────────────────────┐ - │ return of f_nonempty_while_loop() │ - └───────────────────────────────────┘ + ┌───────────────────────────────────────────────────────────────────────────────────────────┐ + │ │ + │ ┌────────────────────────────────────────────┐ │ + │ │ f_nonempty_while_loop() │ │ + │ └────────────────────────────────────────────┘ │ + │ │ │ body() + │ │ (body) │ + │ ▼ │ + ┌─────────────────────────────────┐ ┌────────────────────────────────────────────┐ │ + │ 21-empty-loops.c:101:5-101:11 │ Pos(1) │ 21-empty-loops.c:99:3-102:3 (synthetic) │ │ + │ (21-empty-loops.c:101:5-101:11) │ ◀──────── │ (21-empty-loops.c:99:10-99:11 (synthetic)) │ ◀┘ + └─────────────────────────────────┘ └────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌────────────────────────────────────────────┐ + │ 21-empty-loops.c:103:1-103:1 │ + │ (unknown) │ + └────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌────────────────────────────────────────────┐ + │ return of f_nonempty_while_loop() │ + └────────────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_goto_loop_prefix.dot ┌──────────────────────────────────────┐ - │ f_empty_goto_loop_prefix() │ + │ f_empty_goto_loop_prefix() │ └──────────────────────────────────────┘ │ │ (body) ▼ ┌──────────────────────────────────────┐ - │ 21-empty-loops.c:112:3-112:11 │ - │ (synthetic: false) │ + │ 21-empty-loops.c:112:3-112:11 │ + │ (21-empty-loops.c:112:3-112:11) │ └──────────────────────────────────────┘ │ │ prefix() ▼ - ┌──────────────────────────────────────┐ skip - │ 21-empty-loops.c:115:3-115:38 │ ───────┐ - │ (synthetic: false) │ │ - │ │ ◀──────┘ + ┌──────────────────────────────────────┐ + │ 21-empty-loops.c:115:3-115:38 │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:114:1-115:3 │ │ + │ (unknown)] │ ◀──────┘ └──────────────────────────────────────┘ │ │ Neg(1) ▼ ┌──────────────────────────────────────┐ - │ 21-empty-loops.c:116:1-116:1 │ - │ (synthetic: false) │ + │ 21-empty-loops.c:116:1-116:1 │ + │ (unknown) │ └──────────────────────────────────────┘ │ │ return @@ -204,56 +207,57 @@ └──────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_while_loop_prefix.dot - ┌───────────────────────────────────────┐ - │ f_empty_while_loop_prefix() │ - └───────────────────────────────────────┘ + ┌──────────────────────────────────────────────┐ + │ f_empty_while_loop_prefix() │ + └──────────────────────────────────────────────┘ │ │ (body) ▼ - ┌───────────────────────────────────────┐ - │ 21-empty-loops.c:120:3-120:11 │ - │ (synthetic: false) │ - └───────────────────────────────────────┘ + ┌──────────────────────────────────────────────┐ + │ 21-empty-loops.c:120:3-120:11 │ + │ (21-empty-loops.c:120:3-120:11) │ + └──────────────────────────────────────────────┘ │ │ prefix() ▼ - ┌───────────────────────────────────────┐ Pos(1) - │ 21-empty-loops.c:122:10-122:11 │ ─────────┐ - │ (synthetic: true) │ │ - │ │ ◀────────┘ - └───────────────────────────────────────┘ + ┌──────────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:122:3-122:14 (synthetic) │ ─────────┐ + │ (21-empty-loops.c:122:10-122:11 (synthetic)) │ │ + │ │ ◀────────┘ + └──────────────────────────────────────────────┘ │ │ Neg(1) ▼ - ┌───────────────────────────────────────┐ - │ 21-empty-loops.c:123:1-123:1 │ - │ (synthetic: false) │ - └───────────────────────────────────────┘ + ┌──────────────────────────────────────────────┐ + │ 21-empty-loops.c:123:1-123:1 │ + │ (unknown) │ + └──────────────────────────────────────────────┘ │ │ return ▼ - ┌───────────────────────────────────────┐ - │ return of f_empty_while_loop_prefix() │ - └───────────────────────────────────────┘ + ┌──────────────────────────────────────────────┐ + │ return of f_empty_while_loop_prefix() │ + └──────────────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_goto_loop_semicolon.dot ┌─────────────────────────────────────────┐ - │ f_empty_goto_loop_semicolon() │ + │ f_empty_goto_loop_semicolon() │ └─────────────────────────────────────────┘ │ │ (body) ▼ - ┌─────────────────────────────────────────┐ skip - │ 21-empty-loops.c:127:1-128:3 │ ───────┐ - │ (synthetic: false) │ │ - │ │ ◀──────┘ + ┌─────────────────────────────────────────┐ + │ unknown │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:127:1-128:3 │ │ + │ (unknown)] │ ◀──────┘ └─────────────────────────────────────────┘ │ │ Neg(1) ▼ ┌─────────────────────────────────────────┐ - │ 21-empty-loops.c:131:1-131:1 │ - │ (synthetic: false) │ + │ 21-empty-loops.c:131:1-131:1 │ + │ (unknown) │ └─────────────────────────────────────────┘ │ │ return @@ -263,49 +267,50 @@ └─────────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_while_loop_semicolon.dot - ┌──────────────────────────────────────────┐ - │ f_empty_while_loop_semicolon() │ - └──────────────────────────────────────────┘ + ┌──────────────────────────────────────────────┐ + │ f_empty_while_loop_semicolon() │ + └──────────────────────────────────────────────┘ │ │ (body) ▼ - ┌──────────────────────────────────────────┐ Pos(1) - │ 21-empty-loops.c:135:10-135:11 │ ─────────┐ - │ (synthetic: true) │ │ - │ │ ◀────────┘ - └──────────────────────────────────────────┘ + ┌──────────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:135:3-137:3 (synthetic) │ ─────────┐ + │ (21-empty-loops.c:135:10-135:11 (synthetic)) │ │ + │ │ ◀────────┘ + └──────────────────────────────────────────────┘ │ │ Neg(1) ▼ - ┌──────────────────────────────────────────┐ - │ 21-empty-loops.c:138:1-138:1 │ - │ (synthetic: false) │ - └──────────────────────────────────────────┘ + ┌──────────────────────────────────────────────┐ + │ 21-empty-loops.c:138:1-138:1 │ + │ (unknown) │ + └──────────────────────────────────────────────┘ │ │ return ▼ - ┌──────────────────────────────────────────┐ - │ return of f_empty_while_loop_semicolon() │ - └──────────────────────────────────────────┘ + ┌──────────────────────────────────────────────┐ + │ return of f_empty_while_loop_semicolon() │ + └──────────────────────────────────────────────┘ $ graph-easy --as=boxart f_empty_goto_loop_multiple.dot ┌────────────────────────────────────────┐ - │ f_empty_goto_loop_multiple() │ + │ f_empty_goto_loop_multiple() │ └────────────────────────────────────────┘ │ │ (body) ▼ - ┌────────────────────────────────────────┐ skip - │ 21-empty-loops.c:143:3-143:42 │ ───────┐ - │ (synthetic: false) │ │ - │ │ ◀──────┘ + ┌────────────────────────────────────────┐ + │ 21-empty-loops.c:143:3-143:42 │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:142:1-143:3 │ │ + │ (unknown)] │ ◀──────┘ └────────────────────────────────────────┘ │ │ Neg(1) ▼ ┌────────────────────────────────────────┐ - │ 21-empty-loops.c:146:1-146:1 │ - │ (synthetic: false) │ + │ 21-empty-loops.c:146:1-146:1 │ + │ (unknown) │ └────────────────────────────────────────┘ │ │ return @@ -316,22 +321,23 @@ $ graph-easy --as=boxart f_empty_goto_loop_multiple_semicolon_first.dot ┌────────────────────────────────────────────────────────┐ - │ f_empty_goto_loop_multiple_semicolon_first() │ + │ f_empty_goto_loop_multiple_semicolon_first() │ └────────────────────────────────────────────────────────┘ │ │ (body) ▼ - ┌────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:150:1-151:3 │ ───────┐ - │ (synthetic: false) │ │ - │ │ ◀──────┘ + ┌────────────────────────────────────────────────────────┐ + │ unknown │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:150:1-151:3 │ │ + │ (unknown)] │ ◀──────┘ └────────────────────────────────────────────────────────┘ │ │ Neg(1) ▼ ┌────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:155:1-155:1 │ - │ (synthetic: false) │ + │ 21-empty-loops.c:155:1-155:1 │ + │ (unknown) │ └────────────────────────────────────────────────────────┘ │ │ return @@ -342,22 +348,23 @@ $ graph-easy --as=boxart f_empty_goto_loop_multiple_semicolon_second.dot ┌─────────────────────────────────────────────────────────┐ - │ f_empty_goto_loop_multiple_semicolon_second() │ + │ f_empty_goto_loop_multiple_semicolon_second() │ └─────────────────────────────────────────────────────────┘ │ │ (body) ▼ - ┌─────────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:160:3-160:59 │ ───────┐ - │ (synthetic: false) │ │ - │ │ ◀──────┘ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:160:3-160:59 │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:159:1-160:3 │ │ + │ (unknown)] │ ◀──────┘ └─────────────────────────────────────────────────────────┘ │ │ Neg(1) ▼ ┌─────────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:164:1-164:1 │ - │ (synthetic: false) │ + │ 21-empty-loops.c:164:1-164:1 │ + │ (unknown) │ └─────────────────────────────────────────────────────────┘ │ │ return @@ -368,22 +375,23 @@ $ graph-easy --as=boxart f_empty_goto_loop_multiple_semicolon_both.dot ┌───────────────────────────────────────────────────────┐ - │ f_empty_goto_loop_multiple_semicolon_both() │ + │ f_empty_goto_loop_multiple_semicolon_both() │ └───────────────────────────────────────────────────────┘ │ │ (body) ▼ - ┌───────────────────────────────────────────────────────┐ skip - │ 21-empty-loops.c:168:1-169:3 │ ───────┐ - │ (synthetic: false) │ │ - │ │ ◀──────┘ + ┌───────────────────────────────────────────────────────┐ + │ unknown │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:168:1-169:3 │ │ + │ (unknown)] │ ◀──────┘ └───────────────────────────────────────────────────────┘ │ │ Neg(1) ▼ ┌───────────────────────────────────────────────────────┐ - │ 21-empty-loops.c:174:1-174:1 │ - │ (synthetic: false) │ + │ 21-empty-loops.c:174:1-174:1 │ + │ (unknown) │ └───────────────────────────────────────────────────────┘ │ │ return diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index 34852c803c..a9f91bf4a6 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -1,48 +1,48 @@ $ cfgDot foo.c $ graph-easy --as=boxart main.dot - ┌────────────────────┐ - │ main() │ - └────────────────────┘ - │ - │ (body) - ▼ - ┌────────────────────┐ - │ foo.c:2:7-2:12 │ - │ (synthetic: false) │ - └────────────────────┘ - │ - │ a = 1 - ▼ - ┌────────────────────┐ - │ foo.c:2:14-2:19 │ - │ (synthetic: false) │ - └────────────────────┘ - │ - │ b = 1 - ▼ - ┌────────────────────┐ ┌────────────────────┐ - │ foo.c:7:3-7:11 │ Neg(a > 0) │ foo.c:3:10-3:20 │ - ┌──────▶ │ (synthetic: false) │ ◀──────────── │ (synthetic: true) │ ◀┐ - │ └────────────────────┘ └────────────────────┘ │ - │ │ │ │ - │ │ return 0 │ Pos(a > 0) │ - │ ▼ ▼ │ - │ Neg(b) ┌────────────────────┐ ┌────────────────────┐ │ - │ │ return of main() │ │ foo.c:3:10-3:20 │ │ - │ │ │ ┌─────────── │ (synthetic: true) │ │ - │ └────────────────────┘ │ └────────────────────┘ │ - │ │ │ │ - └────────────────────────────────┘ │ Pos(b) │ b = b - 1 - ▼ │ - ┌────────────────────┐ │ - │ foo.c:4:5-4:8 │ │ - │ (synthetic: false) │ │ - └────────────────────┘ │ - │ │ - │ a = a + 1 │ - ▼ │ - ┌────────────────────┐ │ - │ foo.c:5:5-5:8 │ │ - │ (synthetic: false) │ ─┘ - └────────────────────┘ + ┌───────────────────────────────┐ + │ main() │ + └───────────────────────────────┘ + │ + │ (body) + ▼ + ┌───────────────────────────────┐ + │ foo.c:2:7-2:12 │ + │ (foo.c:2:7-2:12) │ + └───────────────────────────────┘ + │ + │ a = 1 + ▼ + ┌───────────────────────────────┐ + │ foo.c:2:14-2:19 │ + │ (foo.c:2:14-2:19) │ + └───────────────────────────────┘ + │ + │ b = 1 + ▼ + ┌──────────────────┐ ┌───────────────────────────────┐ + │ foo.c:7:3-7:11 │ Neg(a > 0) │ foo.c:3:3-6:3 (synthetic) │ + ┌──────▶ │ (unknown) │ ◀──────────── │ (foo.c:3:10-3:20 (synthetic)) │ ◀┐ + │ └──────────────────┘ └───────────────────────────────┘ │ + │ │ │ │ + │ │ return 0 │ Pos(a > 0) │ + │ ▼ ▼ │ + │ Neg(b) ┌──────────────────┐ ┌───────────────────────────────┐ │ + │ │ return of main() │ │ foo.c:3:3-6:3 (synthetic) │ │ + │ │ │ ┌─────────── │ (foo.c:3:10-3:20 (synthetic)) │ │ + │ └──────────────────┘ │ └───────────────────────────────┘ │ + │ │ │ │ + └──────────────────────────────┘ │ Pos(b) │ b = b - 1 + ▼ │ + ┌───────────────────────────────┐ │ + │ foo.c:4:5-4:8 │ │ + │ (foo.c:4:5-4:8) │ │ + └───────────────────────────────┘ │ + │ │ + │ a = a + 1 │ + ▼ │ + ┌───────────────────────────────┐ │ + │ foo.c:5:5-5:8 │ │ + │ (foo.c:5:5-5:8) │ ─┘ + └───────────────────────────────┘ diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml index 13725bb97d..ea38f593d3 100644 --- a/tests/regression/cfg/util/cfgDot.ml +++ b/tests/regression/cfg/util/cfgDot.ml @@ -32,11 +32,28 @@ let main () = let module LocationExtraNodeStyles = struct - let defaultNodeStyles = [] + let defaultNodeStyles = ["align=\"left\""] + + let pp_loc ppf (loc: GoblintCil.location) = + if loc.line < 0 then + Format.pp_print_string ppf "unknown" + else if loc.synthetic then + Format.fprintf ppf "%a (synthetic)" CilType.Location.pp loc + else + CilType.Location.pp ppf loc + + let pp_locs ppf {CilLocation.loc; eloc} = + Format.fprintf ppf "@[%a@;(%a)@]" pp_loc loc pp_loc eloc + + let pp_label_locs ppf label = + let locs = CilLocation.get_labelLoc label in + Format.fprintf ppf "[%a]" pp_locs locs + let extraNodeStyles = function - | Node.Statement _ as node -> - let loc = Node.location node in - [Printf.sprintf "label=\"%s\\n(synthetic: %B)\"" (CilType.Location.show loc) loc.synthetic] + | Node.Statement stmt -> + let locs: CilLocation.locs = CilLocation.get_stmtLoc stmt in + let label = Format.asprintf "@[%a@;%a@]" pp_locs locs (Format.pp_print_list ~pp_sep:Format.pp_print_cut pp_label_locs) stmt.labels in + [Printf.sprintf "label=\"%s\"" (Str.global_replace (Str.regexp "\n") "\\n" label)] | _ -> [] end in From e81df45c2354dd929e769406349361e608f49453 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 13 Feb 2024 16:17:12 +0200 Subject: [PATCH 10/23] Add test for synthetic witness invariant locations (PR #758) --- tests/regression/cfg/pr-758.t/pr-758.c | 22 ++++++++ tests/regression/cfg/pr-758.t/run.t | 71 ++++++++++++++++++++++++++ 2 files changed, 93 insertions(+) create mode 100644 tests/regression/cfg/pr-758.t/pr-758.c create mode 100644 tests/regression/cfg/pr-758.t/run.t diff --git a/tests/regression/cfg/pr-758.t/pr-758.c b/tests/regression/cfg/pr-758.t/pr-758.c new file mode 100644 index 0000000000..87aa41889d --- /dev/null +++ b/tests/regression/cfg/pr-758.t/pr-758.c @@ -0,0 +1,22 @@ +// Code from https://github.com/goblint/cil/pull/98 + +int main() { + // for loop + int x = 42; + for (x = 0; x < 10; x++) { // there shouldn't be invariants x <= 9, x <= 10 and 0 <= x before this line + // ... + } + + // expression with side effect + int i, k; + i = k = 0; // there shouldn't be invariant k == 0 before this line + + // compound initializers + struct kala { + int kaal; + int hind; + }; + + struct kala a = {2, 3}; // there shouldn't be invariant a.kaal == 2 before this line + return 0; +} diff --git a/tests/regression/cfg/pr-758.t/run.t b/tests/regression/cfg/pr-758.t/run.t new file mode 100644 index 0000000000..d87d9128c7 --- /dev/null +++ b/tests/regression/cfg/pr-758.t/run.t @@ -0,0 +1,71 @@ + $ cfgDot pr-758.c + + $ graph-easy --as=boxart main.dot + + ┌────────────────────────────────────────────────────────────────────────────────────────┐ + │ │ + │ ┌────────────────────────────────────┐ │ + │ │ main() │ │ + │ └────────────────────────────────────┘ │ + │ │ │ + │ │ (body) │ + │ ▼ │ + │ ┌────────────────────────────────────┐ │ + │ │ pr-758.c:5:7-5:13 │ │ + │ │ (pr-758.c:5:7-5:13) │ │ + │ └────────────────────────────────────┘ │ + │ │ │ x = x + 1 + │ │ x = 42 │ + │ ▼ │ + │ ┌────────────────────────────────────┐ │ + │ │ pr-758.c:6:3-8:3 (synthetic) │ │ + │ │ (pr-758.c:6:7-6:26 (synthetic)) │ │ + │ └────────────────────────────────────┘ │ + │ │ │ + │ │ x = 0 │ + │ ▼ │ + ┌─────────────────────────────────┐ ┌────────────────────────────────────┐ │ + │ pr-758.c:6:3-8:3 (synthetic) │ Pos(x < 10) │ pr-758.c:6:3-8:3 (synthetic) │ │ + │ (pr-758.c:6:7-6:26 (synthetic)) │ ◀───────────── │ (pr-758.c:6:7-6:26 (synthetic)) │ ◀┘ + └─────────────────────────────────┘ └────────────────────────────────────┘ + │ + │ Neg(x < 10) + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:12:3-12:12 │ + │ (pr-758.c:12:3-12:12) │ + └────────────────────────────────────┘ + │ + │ k = 0 + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:12:3-12:12 (synthetic) │ + │ (pr-758.c:12:3-12:12 (synthetic)) │ + └────────────────────────────────────┘ + │ + │ i = k + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:20:15-20:24 │ + │ (pr-758.c:20:15-20:24) │ + └────────────────────────────────────┘ + │ + │ a.kaal = 2 + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:20:15-20:24 (synthetic) │ + │ (pr-758.c:20:15-20:24 (synthetic)) │ + └────────────────────────────────────┘ + │ + │ a.hind = 3 + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:21:3-21:11 │ + │ (unknown) │ + └────────────────────────────────────┘ + │ + │ return 0 + ▼ + ┌────────────────────────────────────┐ + │ return of main() │ + └────────────────────────────────────┘ From 7018ccf7915bd31fd3bd66e1250ad007bc18b09d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 13 Feb 2024 16:19:01 +0200 Subject: [PATCH 11/23] Add test for incorrect witness invariant locations from CIL transformations (issue #1356) --- .../regression/cfg/issue-1356.t/issue-1356.c | 20 +++++ tests/regression/cfg/issue-1356.t/run.t | 78 +++++++++++++++++++ 2 files changed, 98 insertions(+) create mode 100644 tests/regression/cfg/issue-1356.t/issue-1356.c create mode 100644 tests/regression/cfg/issue-1356.t/run.t diff --git a/tests/regression/cfg/issue-1356.t/issue-1356.c b/tests/regression/cfg/issue-1356.t/issue-1356.c new file mode 100644 index 0000000000..b773f6cf66 --- /dev/null +++ b/tests/regression/cfg/issue-1356.t/issue-1356.c @@ -0,0 +1,20 @@ +extern int __VERIFIER_nondet_int(void); + +extern void abort(void); +void assume_abort_if_not(int cond) { + if(!cond) {abort();} +} + +int minus(int a, int b) { + assume_abort_if_not(b <= 0 || a >= b - 2147483648); // there shouldn't be invariants 1 <= b and b != 0 before this line + assume_abort_if_not(b >= 0 || a <= b + 2147483647); // there shouldn't be invariants b <= -1 and b != 0 before this line + return a - b; +} + +int main() { + int x, y; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + minus(x, y); + return 0; +} diff --git a/tests/regression/cfg/issue-1356.t/run.t b/tests/regression/cfg/issue-1356.t/run.t new file mode 100644 index 0000000000..1013576527 --- /dev/null +++ b/tests/regression/cfg/issue-1356.t/run.t @@ -0,0 +1,78 @@ + $ cfgDot issue-1356.c + + $ graph-easy --as=boxart minus.dot + + ┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ + │ │ + │ ┌─────────────────────────────────────────┐ │ + │ │ minus() │ │ + │ └─────────────────────────────────────────┘ │ + │ │ │ + │ Pos((long )a >= (long )b - 2147483648) │ (body) │ + ▼ ▼ │ + ┌─────────────────────────────────────────┐ ┌─────────────────────────────────────────┐ │ + │ issue-1356.c:9:3-9:53 (synthetic) │ Pos(b <= 0) │ issue-1356.c:9:3-9:53 (synthetic) │ │ + │ (issue-1356.c:9:3-9:53 (synthetic)) │ ◀────────────────────────── │ (issue-1356.c:9:3-9:53 (synthetic)) │ │ + └─────────────────────────────────────────┘ └─────────────────────────────────────────┘ │ + │ │ │ + │ │ Neg(b <= 0) │ + │ ▼ │ + │ ┌─────────────────────────────────────────┐ │ + │ │ issue-1356.c:9:3-9:53 │ │ + │ │ (issue-1356.c:9:3-9:53) │ ─┘ + │ └─────────────────────────────────────────┘ + │ │ + │ │ Neg((long )a >= (long )b - 2147483648) + │ ▼ + │ ┌─────────────────────────────────────────┐ + │ │ issue-1356.c:9:3-9:53 (synthetic) │ + │ │ (issue-1356.c:9:3-9:53 (synthetic)) │ + │ └─────────────────────────────────────────┘ + │ │ + │ │ tmp = 0 + │ ▼ + │ ┌─────────────────────────────────────────┐ + │ tmp = 1 │ issue-1356.c:9:3-9:53 (synthetic) │ + └───────────────────────────────────────────────────────────────────▶ │ (issue-1356.c:9:3-9:53 (synthetic)) │ + └─────────────────────────────────────────┘ + │ + │ assume_abort_if_not(tmp) + ▼ + ┌─────────────────────────────────────────┐ + │ issue-1356.c:10:3-10:53 (synthetic) │ + │ (issue-1356.c:10:3-10:53 (synthetic)) │ ─┐ + └─────────────────────────────────────────┘ │ + │ │ + │ Neg(b >= 0) │ + ▼ │ + ┌─────────────────────────────────────────┐ ┌─────────────────────────────────────────┐ │ + │ issue-1356.c:10:3-10:53 (synthetic) │ Neg(a <= b + 2147483647) │ issue-1356.c:10:3-10:53 │ │ + │ (issue-1356.c:10:3-10:53 (synthetic)) │ ◀────────────────────────── │ (issue-1356.c:10:3-10:53) │ │ Pos(b >= 0) + └─────────────────────────────────────────┘ └─────────────────────────────────────────┘ │ + │ │ │ + │ │ Pos(a <= b + 2147483647) │ + │ ▼ │ + │ ┌─────────────────────────────────────────┐ │ + │ │ issue-1356.c:10:3-10:53 (synthetic) │ │ + │ │ (issue-1356.c:10:3-10:53 (synthetic)) │ ◀┘ + │ └─────────────────────────────────────────┘ + │ │ + │ │ tmp___0 = 1 + │ ▼ + │ ┌─────────────────────────────────────────┐ + │ tmp___0 = 0 │ issue-1356.c:10:3-10:53 (synthetic) │ + └───────────────────────────────────────────────────────────────────▶ │ (issue-1356.c:10:3-10:53 (synthetic)) │ + └─────────────────────────────────────────┘ + │ + │ assume_abort_if_not(tmp___0) + ▼ + ┌─────────────────────────────────────────┐ + │ issue-1356.c:11:3-11:15 │ + │ (unknown) │ + └─────────────────────────────────────────┘ + │ + │ return a - b + ▼ + ┌─────────────────────────────────────────┐ + │ return of minus() │ + └─────────────────────────────────────────┘ From b734f50ace1a13557cffb0b61413f0f1ad0b8f5e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 13 Feb 2024 16:22:09 +0200 Subject: [PATCH 12/23] Update CIL for synthetic locations fix --- goblint.opam | 2 +- goblint.opam.locked | 2 +- goblint.opam.template | 2 +- tests/regression/cfg/issue-1356.t/run.t | 16 ++++++++-------- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/goblint.opam b/goblint.opam index e4f45fadb4..3805729f9e 100644 --- a/goblint.opam +++ b/goblint.opam @@ -77,7 +77,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git" available: os-distribution != "alpine" & arch != "arm64" pin-depends: [ # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed - [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51" ] + [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ] # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] ] diff --git a/goblint.opam.locked b/goblint.opam.locked index c6c9b49913..4a54c45876 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -133,7 +133,7 @@ post-messages: [ pin-depends: [ [ "goblint-cil.2.0.3" - "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51" + "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ] [ "ppx_deriving.5.2.1" diff --git a/goblint.opam.template b/goblint.opam.template index 8289cd4e2f..6ddeb0a85c 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -3,7 +3,7 @@ available: os-distribution != "alpine" & arch != "arm64" pin-depends: [ # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed - [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51" ] + [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ] # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] ] diff --git a/tests/regression/cfg/issue-1356.t/run.t b/tests/regression/cfg/issue-1356.t/run.t index 1013576527..78a81aff68 100644 --- a/tests/regression/cfg/issue-1356.t/run.t +++ b/tests/regression/cfg/issue-1356.t/run.t @@ -11,15 +11,15 @@ │ Pos((long )a >= (long )b - 2147483648) │ (body) │ ▼ ▼ │ ┌─────────────────────────────────────────┐ ┌─────────────────────────────────────────┐ │ - │ issue-1356.c:9:3-9:53 (synthetic) │ Pos(b <= 0) │ issue-1356.c:9:3-9:53 (synthetic) │ │ - │ (issue-1356.c:9:3-9:53 (synthetic)) │ ◀────────────────────────── │ (issue-1356.c:9:3-9:53 (synthetic)) │ │ + │ issue-1356.c:9:3-9:53 (synthetic) │ Pos(b <= 0) │ issue-1356.c:9:3-9:53 │ │ + │ (issue-1356.c:9:3-9:53 (synthetic)) │ ◀────────────────────────── │ (issue-1356.c:9:3-9:53) │ │ └─────────────────────────────────────────┘ └─────────────────────────────────────────┘ │ │ │ │ │ │ Neg(b <= 0) │ │ ▼ │ │ ┌─────────────────────────────────────────┐ │ - │ │ issue-1356.c:9:3-9:53 │ │ - │ │ (issue-1356.c:9:3-9:53) │ ─┘ + │ │ issue-1356.c:9:3-9:53 (synthetic) │ │ + │ │ (issue-1356.c:9:3-9:53 (synthetic)) │ ─┘ │ └─────────────────────────────────────────┘ │ │ │ │ Neg((long )a >= (long )b - 2147483648) @@ -39,15 +39,15 @@ │ assume_abort_if_not(tmp) ▼ ┌─────────────────────────────────────────┐ - │ issue-1356.c:10:3-10:53 (synthetic) │ - │ (issue-1356.c:10:3-10:53 (synthetic)) │ ─┐ + │ issue-1356.c:10:3-10:53 │ + │ (issue-1356.c:10:3-10:53) │ ─┐ └─────────────────────────────────────────┘ │ │ │ │ Neg(b >= 0) │ ▼ │ ┌─────────────────────────────────────────┐ ┌─────────────────────────────────────────┐ │ - │ issue-1356.c:10:3-10:53 (synthetic) │ Neg(a <= b + 2147483647) │ issue-1356.c:10:3-10:53 │ │ - │ (issue-1356.c:10:3-10:53 (synthetic)) │ ◀────────────────────────── │ (issue-1356.c:10:3-10:53) │ │ Pos(b >= 0) + │ issue-1356.c:10:3-10:53 (synthetic) │ Neg(a <= b + 2147483647) │ issue-1356.c:10:3-10:53 (synthetic) │ │ + │ (issue-1356.c:10:3-10:53 (synthetic)) │ ◀────────────────────────── │ (issue-1356.c:10:3-10:53 (synthetic)) │ │ Pos(b >= 0) └─────────────────────────────────────────┘ └─────────────────────────────────────────┘ │ │ │ │ │ │ Pos(a <= b + 2147483647) │ From 65ae0f0322aa4d4bdd628f21755457fe0d54fe1d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 13 Feb 2024 16:28:10 +0200 Subject: [PATCH 13/23] Add graph-easy Ubuntu depext --- goblint.opam | 3 +++ goblint.opam.locked | 1 + goblint.opam.template | 3 +++ 3 files changed, 7 insertions(+) diff --git a/goblint.opam b/goblint.opam index 3805729f9e..8ccde7c6ba 100644 --- a/goblint.opam +++ b/goblint.opam @@ -81,6 +81,9 @@ pin-depends: [ # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] ] +depexts: [ + ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} +] post-messages: [ "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"} ] diff --git a/goblint.opam.locked b/goblint.opam.locked index 4a54c45876..5224d5aa18 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -140,3 +140,4 @@ pin-depends: [ "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] ] +depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} diff --git a/goblint.opam.template b/goblint.opam.template index 6ddeb0a85c..1364586310 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -7,6 +7,9 @@ pin-depends: [ # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] ] +depexts: [ + ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} +] post-messages: [ "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"} ] From de83ccc1e082ee49a84af54cbcf04e1f77d6b367 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 13 Feb 2024 16:32:40 +0200 Subject: [PATCH 14/23] Try to pin using with-test in CI --- .github/workflows/coverage.yml | 1 + .github/workflows/locked.yml | 2 ++ .github/workflows/unlocked.yml | 6 ++++++ 3 files changed, 9 insertions(+) diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 4b47a66e15..998e1e766f 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -35,6 +35,7 @@ jobs: # otherwise setup-ocaml pins non-locked dependencies # https://github.com/ocaml/setup-ocaml/issues/166 OPAMLOCKED: locked + OPAMWITHTEST: true uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index e25ccfcea1..1401564466 100644 --- a/.github/workflows/locked.yml +++ b/.github/workflows/locked.yml @@ -37,6 +37,7 @@ jobs: # otherwise setup-ocaml pins non-locked dependencies # https://github.com/ocaml/setup-ocaml/issues/166 OPAMLOCKED: locked + OPAMWITHTEST: true uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} @@ -111,6 +112,7 @@ jobs: # otherwise setup-ocaml pins non-locked dependencies # https://github.com/ocaml/setup-ocaml/issues/166 OPAMLOCKED: locked + OPAMWITHTEST: true uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index 57fa0cb6b5..080a9303e5 100644 --- a/.github/workflows/unlocked.yml +++ b/.github/workflows/unlocked.yml @@ -49,6 +49,8 @@ jobs: uses: actions/checkout@v4 - name: Set up OCaml ${{ matrix.ocaml-compiler }} + env: + OPAMWITHTEST: true uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} @@ -139,6 +141,8 @@ jobs: uses: actions/checkout@v4 - name: Set up OCaml ${{ matrix.ocaml-compiler }} + env: + OPAMWITHTEST: true uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} @@ -255,6 +259,8 @@ jobs: uses: actions/checkout@v4 - name: Set up OCaml ${{ matrix.ocaml-compiler }} + env: + OPAMWITHTEST: true uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} From 4d86fd01028133ccf1f592236fe7ca59ae9af8bd Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 13 Feb 2024 16:39:09 +0200 Subject: [PATCH 15/23] Add enabled_if to CFG tests in 00-sanity as well --- tests/regression/00-sanity/dune | 6 ++++++ tests/regression/dune | 3 +-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/tests/regression/00-sanity/dune b/tests/regression/00-sanity/dune index 23c0dd3290..d6e0ac7094 100644 --- a/tests/regression/00-sanity/dune +++ b/tests/regression/00-sanity/dune @@ -1,2 +1,8 @@ (cram (deps (glob_files *.c))) + +(cram + (applies_to 19-if-0 20-if-0-realnode 21-empty-loops) + (enabled_if %{bin-available:graph-easy}) + (deps + %{bin:cfgDot})) diff --git a/tests/regression/dune b/tests/regression/dune index a238677edc..ab95324fa4 100644 --- a/tests/regression/dune +++ b/tests/regression/dune @@ -6,5 +6,4 @@ (applies_to :whole_subtree) (deps %{bin:goblint} - (package goblint) ; need entire package for includes/ - %{bin:cfgDot})) + (package goblint))) ; need entire package for includes/ From d48e85ea2557efeeb61ba7803192357044bdb138 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 13 Feb 2024 17:01:53 +0200 Subject: [PATCH 16/23] Try to pin using with-test in CI via opam-depext-flags --- .github/workflows/coverage.yml | 1 + .github/workflows/locked.yml | 2 ++ .github/workflows/unlocked.yml | 3 +++ 3 files changed, 6 insertions(+) diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 998e1e766f..10ccf2944e 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -39,6 +39,7 @@ jobs: uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} + opam-depext-flags: --with-test - name: Install dependencies run: opam install . --deps-only --locked --with-test diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index 1401564466..546699fc14 100644 --- a/.github/workflows/locked.yml +++ b/.github/workflows/locked.yml @@ -41,6 +41,7 @@ jobs: uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} + opam-depext-flags: --with-test - name: Install dependencies run: opam install . --deps-only --locked --with-test @@ -116,6 +117,7 @@ jobs: uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} + opam-depext-flags: --with-test - name: Install spin run: sudo apt-get -y install spin diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index 080a9303e5..58d23c575d 100644 --- a/.github/workflows/unlocked.yml +++ b/.github/workflows/unlocked.yml @@ -54,6 +54,7 @@ jobs: uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} + opam-depext-flags: --with-test - name: Install dependencies run: opam install . --deps-only --with-test @@ -146,6 +147,7 @@ jobs: uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} + opam-depext-flags: --with-test - name: Install dependencies run: opam install . --deps-only --with-test @@ -264,6 +266,7 @@ jobs: uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} + opam-depext-flags: --with-test - name: Install Goblint with test run: opam install goblint --with-test From 4b58d45481f781e81a4c4d78663ce97d82d33190 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 13 Feb 2024 17:14:53 +0200 Subject: [PATCH 17/23] Try to pin using with-test in CI via hack https://github.com/ocaml/opam/issues/3790#issuecomment-765650349. --- .github/workflows/locked.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index 546699fc14..11d617029f 100644 --- a/.github/workflows/locked.yml +++ b/.github/workflows/locked.yml @@ -43,6 +43,8 @@ jobs: ocaml-compiler: ${{ matrix.ocaml-compiler }} opam-depext-flags: --with-test + - run: opam install . --dry-run --deps-only -ty | awk '/-> installed/{print $3}' | xargs opam depext -iy + - name: Install dependencies run: opam install . --deps-only --locked --with-test From ae5b2cf9f859ff7365c4b38ba9668f22ed58ace6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 13 Feb 2024 17:33:05 +0200 Subject: [PATCH 18/23] Install graph-easy manually in CI because nothing works --- .github/workflows/coverage.yml | 6 ++++-- .github/workflows/locked.yml | 12 +++++++----- .github/workflows/unlocked.yml | 21 ++++++++++++--------- 3 files changed, 23 insertions(+), 16 deletions(-) diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 10ccf2944e..62806a7669 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -35,11 +35,13 @@ jobs: # otherwise setup-ocaml pins non-locked dependencies # https://github.com/ocaml/setup-ocaml/issues/166 OPAMLOCKED: locked - OPAMWITHTEST: true uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext-flags: --with-test + opam-depext-flags: --with-test # doesn't work + + - name: Install graph-easy + run: sudo apt install -y libgraph-easy-perl - name: Install dependencies run: opam install . --deps-only --locked --with-test diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index 11d617029f..c9fd4a5693 100644 --- a/.github/workflows/locked.yml +++ b/.github/workflows/locked.yml @@ -37,13 +37,13 @@ jobs: # otherwise setup-ocaml pins non-locked dependencies # https://github.com/ocaml/setup-ocaml/issues/166 OPAMLOCKED: locked - OPAMWITHTEST: true uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext-flags: --with-test + opam-depext-flags: --with-test # doesn't work - - run: opam install . --dry-run --deps-only -ty | awk '/-> installed/{print $3}' | xargs opam depext -iy + - name: Install graph-easy + run: sudo apt install -y libgraph-easy-perl - name: Install dependencies run: opam install . --deps-only --locked --with-test @@ -115,11 +115,13 @@ jobs: # otherwise setup-ocaml pins non-locked dependencies # https://github.com/ocaml/setup-ocaml/issues/166 OPAMLOCKED: locked - OPAMWITHTEST: true uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext-flags: --with-test + opam-depext-flags: --with-test # doesn't work + + - name: Install graph-easy + run: sudo apt install -y libgraph-easy-perl - name: Install spin run: sudo apt-get -y install spin diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index 58d23c575d..d9948c4af6 100644 --- a/.github/workflows/unlocked.yml +++ b/.github/workflows/unlocked.yml @@ -49,12 +49,13 @@ jobs: uses: actions/checkout@v4 - name: Set up OCaml ${{ matrix.ocaml-compiler }} - env: - OPAMWITHTEST: true uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext-flags: --with-test + opam-depext-flags: --with-test # doesn't work + + - name: Install graph-easy + run: sudo apt install -y libgraph-easy-perl - name: Install dependencies run: opam install . --deps-only --with-test @@ -142,12 +143,13 @@ jobs: uses: actions/checkout@v4 - name: Set up OCaml ${{ matrix.ocaml-compiler }} - env: - OPAMWITHTEST: true uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext-flags: --with-test + opam-depext-flags: --with-test # doesn't work + + - name: Install graph-easy + run: sudo apt install -y libgraph-easy-perl - name: Install dependencies run: opam install . --deps-only --with-test @@ -261,12 +263,13 @@ jobs: uses: actions/checkout@v4 - name: Set up OCaml ${{ matrix.ocaml-compiler }} - env: - OPAMWITHTEST: true uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext-flags: --with-test + opam-depext-flags: --with-test # doesn't work + + - name: Install graph-easy + run: sudo apt install -y libgraph-easy-perl - name: Install Goblint with test run: opam install goblint --with-test From 15e8ca3c9c893414ad3958043fe88e04cab7c084 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 13 Feb 2024 17:55:41 +0200 Subject: [PATCH 19/23] Install graph-easy only on Ubuntu in CI --- .github/workflows/coverage.yml | 1 + .github/workflows/locked.yml | 2 ++ .github/workflows/unlocked.yml | 3 +++ 3 files changed, 6 insertions(+) diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 62806a7669..6a12d7d11c 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -41,6 +41,7 @@ jobs: opam-depext-flags: --with-test # doesn't work - name: Install graph-easy + if: ${{ matrix.os == 'ubuntu-latest' }} run: sudo apt install -y libgraph-easy-perl - name: Install dependencies diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index c9fd4a5693..45bb4b8f9e 100644 --- a/.github/workflows/locked.yml +++ b/.github/workflows/locked.yml @@ -43,6 +43,7 @@ jobs: opam-depext-flags: --with-test # doesn't work - name: Install graph-easy + if: ${{ matrix.os == 'ubuntu-latest' }} run: sudo apt install -y libgraph-easy-perl - name: Install dependencies @@ -121,6 +122,7 @@ jobs: opam-depext-flags: --with-test # doesn't work - name: Install graph-easy + if: ${{ matrix.os == 'ubuntu-latest' }} run: sudo apt install -y libgraph-easy-perl - name: Install spin diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index d9948c4af6..906f23ab90 100644 --- a/.github/workflows/unlocked.yml +++ b/.github/workflows/unlocked.yml @@ -55,6 +55,7 @@ jobs: opam-depext-flags: --with-test # doesn't work - name: Install graph-easy + if: ${{ matrix.os == 'ubuntu-latest' }} run: sudo apt install -y libgraph-easy-perl - name: Install dependencies @@ -149,6 +150,7 @@ jobs: opam-depext-flags: --with-test # doesn't work - name: Install graph-easy + if: ${{ matrix.os == 'ubuntu-latest' }} run: sudo apt install -y libgraph-easy-perl - name: Install dependencies @@ -269,6 +271,7 @@ jobs: opam-depext-flags: --with-test # doesn't work - name: Install graph-easy + if: ${{ matrix.os == 'ubuntu-latest' }} run: sudo apt install -y libgraph-easy-perl - name: Install Goblint with test From d146e9b33d416a251833e30b5eed3875087d27f3 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 14 Feb 2024 10:28:47 +0200 Subject: [PATCH 20/23] Update GobView for moved compute_cfg --- gobview | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gobview b/gobview index 649451b76d..581a3e2e06 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 649451b76de7294b736ff863d1c1479bf5be2270 +Subproject commit 581a3e2e06f7f076b05688e2e7085db36de3e260 From b730994801d469e0af747cd3854e11b21885f9ef Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 16:44:14 +0200 Subject: [PATCH 21/23] Comment about depext --with-test --- .github/workflows/coverage.yml | 4 ++-- .github/workflows/locked.yml | 8 ++++---- .github/workflows/unlocked.yml | 12 ++++++------ 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 6a12d7d11c..3d02f33dc5 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -38,9 +38,9 @@ jobs: uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext-flags: --with-test # doesn't work + opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836) - - name: Install graph-easy + - name: Install graph-easy # TODO: remove if depext --with-test works if: ${{ matrix.os == 'ubuntu-latest' }} run: sudo apt install -y libgraph-easy-perl diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index 45bb4b8f9e..f28e21e147 100644 --- a/.github/workflows/locked.yml +++ b/.github/workflows/locked.yml @@ -40,9 +40,9 @@ jobs: uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext-flags: --with-test # doesn't work + opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836) - - name: Install graph-easy + - name: Install graph-easy # TODO: remove if depext --with-test works if: ${{ matrix.os == 'ubuntu-latest' }} run: sudo apt install -y libgraph-easy-perl @@ -119,9 +119,9 @@ jobs: uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext-flags: --with-test # doesn't work + opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836) - - name: Install graph-easy + - name: Install graph-easy # TODO: remove if depext --with-test works if: ${{ matrix.os == 'ubuntu-latest' }} run: sudo apt install -y libgraph-easy-perl diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index 906f23ab90..956a03ea32 100644 --- a/.github/workflows/unlocked.yml +++ b/.github/workflows/unlocked.yml @@ -52,9 +52,9 @@ jobs: uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext-flags: --with-test # doesn't work + opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836) - - name: Install graph-easy + - name: Install graph-easy # TODO: remove if depext --with-test works if: ${{ matrix.os == 'ubuntu-latest' }} run: sudo apt install -y libgraph-easy-perl @@ -147,9 +147,9 @@ jobs: uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext-flags: --with-test # doesn't work + opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836) - - name: Install graph-easy + - name: Install graph-easy # TODO: remove if depext --with-test works if: ${{ matrix.os == 'ubuntu-latest' }} run: sudo apt install -y libgraph-easy-perl @@ -268,9 +268,9 @@ jobs: uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext-flags: --with-test # doesn't work + opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836) - - name: Install graph-easy + - name: Install graph-easy # TODO: remove if depext --with-test works if: ${{ matrix.os == 'ubuntu-latest' }} run: sudo apt install -y libgraph-easy-perl From 45e01c361447dddcab52e22e9a317b3392e1178b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 16:53:34 +0200 Subject: [PATCH 22/23] Extract CilCfg0 --- src/common/util/cilCfg0.ml | 24 ++++++++++++++++++++++++ src/util/cilCfg.ml | 21 +-------------------- tests/regression/cfg/util/cfgDot.ml | 20 +------------------- 3 files changed, 26 insertions(+), 39 deletions(-) create mode 100644 src/common/util/cilCfg0.ml diff --git a/src/common/util/cilCfg0.ml b/src/common/util/cilCfg0.ml new file mode 100644 index 0000000000..d48884135f --- /dev/null +++ b/src/common/util/cilCfg0.ml @@ -0,0 +1,24 @@ +(** CIL CFG functions to avoid dependency problems. *) + +open GoblintCil + +class allBBVisitor = object (* puts every instruction into its own basic block *) + inherit nopCilVisitor + method! vstmt s = + match s.skind with + | Instr(il) -> + let list_of_stmts = + List.map (fun one_inst -> mkStmtOneInstr one_inst) il in + let block = mkBlock list_of_stmts in + ChangeDoChildrenPost(s, (fun _ -> s.skind <- Block(block); s)) + | _ -> DoChildren + + method! vvdec _ = SkipChildren + method! vexpr _ = SkipChildren + method! vlval _ = SkipChildren + method! vtype _ = SkipChildren +end + +let end_basic_blocks f = + let thisVisitor = new allBBVisitor in + visitCilFileSameGlobals thisVisitor f diff --git a/src/util/cilCfg.ml b/src/util/cilCfg.ml index df766d5bdd..d6e74fc8af 100644 --- a/src/util/cilCfg.ml +++ b/src/util/cilCfg.ml @@ -3,26 +3,7 @@ open GobConfig open GoblintCil -class allBBVisitor = object (* puts every instruction into its own basic block *) - inherit nopCilVisitor - method! vstmt s = - match s.skind with - | Instr(il) -> - let list_of_stmts = - List.map (fun one_inst -> mkStmtOneInstr one_inst) il in - let block = mkBlock list_of_stmts in - ChangeDoChildrenPost(s, (fun _ -> s.skind <- Block(block); s)) - | _ -> DoChildren - - method! vvdec _ = SkipChildren - method! vexpr _ = SkipChildren - method! vlval _ = SkipChildren - method! vtype _ = SkipChildren -end - -let end_basic_blocks f = - let thisVisitor = new allBBVisitor in - visitCilFileSameGlobals thisVisitor f +include CilCfg0 class countLoopsVisitor(count) = object diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml index 3d823d3963..8d28933596 100644 --- a/tests/regression/cfg/util/cfgDot.ml +++ b/tests/regression/cfg/util/cfgDot.ml @@ -1,27 +1,9 @@ -(* Part of CilCfg *) -class allBBVisitor = object (* puts every instruction into its own basic block *) - inherit GoblintCil.nopCilVisitor - method! vstmt s = - match s.skind with - | Instr(il) -> - let list_of_stmts = - List.map (fun one_inst -> GoblintCil.mkStmtOneInstr one_inst) il in - let block = GoblintCil.mkBlock list_of_stmts in - ChangeDoChildrenPost(s, (fun _ -> s.skind <- Block(block); s)) - | _ -> DoChildren - - method! vvdec _ = SkipChildren - method! vexpr _ = SkipChildren - method! vlval _ = SkipChildren - method! vtype _ = SkipChildren -end - let main () = Goblint_logs.Logs.Level.current := Info; Cilfacade.init (); let ast = Cilfacade.getAST (Fpath.v Sys.argv.(1)) in - GoblintCil.visitCilFileSameGlobals (new allBBVisitor) ast; + CilCfg0.end_basic_blocks ast; (* Part of CilCfg.createCFG *) GoblintCil.iterGlobals ast (function | GFun (fd, _) -> From 3f20225ba1abcb85323e6504437cf04cf72be60b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 16:58:29 +0200 Subject: [PATCH 23/23] Remove commented-out CilLocation.get_labelsLoc --- src/common/util/cilLocation.ml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/common/util/cilLocation.ml b/src/common/util/cilLocation.ml index 6f9a3ce7c4..23c1b8df5b 100644 --- a/src/common/util/cilLocation.ml +++ b/src/common/util/cilLocation.ml @@ -11,14 +11,7 @@ let get_labelLoc = function | CaseRange (_, _, loc, eloc) -> {loc; eloc} | Default (loc, eloc) -> {loc; eloc} -(* let rec get_labelsLoc = function - | [] -> {loc = locUnknown; eloc = locUnknown} - | label :: labels -> - let loc = get_labelLoc label in - if CilType.Location.equal loc Cil.locUnknown then - get_labelsLoc labels (* maybe another label has known location *) - else - loc *) +(* TODO: need get_labelsLoc? *) (** Following functions are similar to [Cil] versions, but return expression location instead of entire statement location, where possible. *) (* Ideally we would have both copies of the functions available, but UpdateCil would have to be adapted per-stmtkind/instr to store and update either one or two locations. *)