-
Notifications
You must be signed in to change notification settings - Fork 76
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #1360 from goblint/cfg-test
Add cram tests for CFGs
- Loading branch information
Showing
26 changed files
with
921 additions
and
32 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,45 @@ | ||
| 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} | ||
|
|
||
| (* 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. *) | ||
|
|
||
| (** 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +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: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() │ | ||
| └────────────────────────┘ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,35 @@ | ||
| $ cfgDot 20-if-0-realnode.c | ||
|
|
||
| $ graph-easy --as=boxart main.dot | ||
| ┌─────────────────────────────────┐ | ||
| │ main() │ | ||
| └─────────────────────────────────┘ | ||
| │ | ||
| │ (body) | ||
| ▼ | ||
| ┌─────────────────────────────────┐ | ||
| │ 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 │ | ||
| │ (20-if-0-realnode.c:10:9-10:16) │ | ||
| └─────────────────────────────────┘ | ||
| │ | ||
| │ stuff() | ||
| ▼ | ||
| ┌─────────────────────────────────┐ | ||
| │ 20-if-0-realnode.c:15:5-15:13 │ | ||
| │ (unknown) │ | ||
| └─────────────────────────────────┘ | ||
| │ | ||
| │ return 0 | ||
| ▼ | ||
| ┌─────────────────────────────────┐ | ||
| │ return of main() │ | ||
| └─────────────────────────────────┘ |
Oops, something went wrong.