Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add cram tests for CFGs #1360

Merged
merged 25 commits into from
Feb 21, 2024
Merged

Add cram tests for CFGs #1360

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
55c9e5d
Add CFG test using graph-easy
sim642 Feb 9, 2024
3093d27
Use locations in CFG test nodes
sim642 Feb 9, 2024
b8c6e64
Use stdout for CFG test
sim642 Feb 9, 2024
d13a432
Use function names in CFG tests
sim642 Feb 9, 2024
48d4b63
Add cram tests for CFG
sim642 Feb 9, 2024
6ed1aae
Move some functions to CfgTools
sim642 Feb 9, 2024
b727532
Test CFGs per function
sim642 Feb 9, 2024
a1483d6
Fix instructions in CFG testing
sim642 Feb 9, 2024
361af13
More detailed location output in CFG tests
sim642 Feb 9, 2024
9036370
Merge branch 'master' into cfg-test
sim642 Feb 13, 2024
e81df45
Add test for synthetic witness invariant locations (PR #758)
sim642 Feb 13, 2024
7018ccf
Add test for incorrect witness invariant locations from CIL transform…
sim642 Feb 13, 2024
b734f50
Update CIL for synthetic locations fix
sim642 Feb 13, 2024
65ae0f0
Add graph-easy Ubuntu depext
sim642 Feb 13, 2024
de83ccc
Try to pin using with-test in CI
sim642 Feb 13, 2024
4d86fd0
Add enabled_if to CFG tests in 00-sanity as well
sim642 Feb 13, 2024
d48e85e
Try to pin using with-test in CI via opam-depext-flags
sim642 Feb 13, 2024
4b58d45
Try to pin using with-test in CI via hack
sim642 Feb 13, 2024
ae5b2cf
Install graph-easy manually in CI because nothing works
sim642 Feb 13, 2024
15e8ca3
Install graph-easy only on Ubuntu in CI
sim642 Feb 13, 2024
d146e9b
Update GobView for moved compute_cfg
sim642 Feb 14, 2024
b730994
Comment about depext --with-test
sim642 Feb 21, 2024
45e01c3
Extract CilCfg0
sim642 Feb 21, 2024
3f20225
Remove commented-out CilLocation.get_labelsLoc
sim642 Feb 21, 2024
5e65e22
Merge branch 'master' into cfg-test
sim642 Feb 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Use locations in CFG test nodes
  • Loading branch information
@sim642
sim642 committed Feb 9, 2024
commit 3093d27482a7c66777a773dc1c641d988f1d3190
105 changes: 57 additions & 48 deletions tests/regression/cfg/foo.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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) │ ─┘
└────────────────────┘
16 changes: 15 additions & 1 deletion tests/regression/cfg/util/cfgDot.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
open Goblint_lib
open CfgTools

let main () =
Cilfacade.init ();
Expand All @@ -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 ()