Skip to content

Add warning when both branches are dead #849

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

Merged
merged 2 commits into from
Oct 10, 2022
Merged

Add warning when both branches are dead #849

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f1b5f03
Add warning when both branches dead
michael-schwarz Oct 7, 2022
e9fba9a
Update both branches dead error
sim642 Oct 10, 2022
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
4 changes: 3 additions & 1 deletion src/framework/constraints.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1111,7 +1111,9 @@ struct
let loc = Node.location g in (* TODO: looking up location now doesn't work nicely with incremental *)
let cilinserted = if loc.synthetic then "(possibly inserted by CIL) " else "" in
M.warn ~loc:(Node g) ~tags:[CWE (if tv then 571 else 570)] ~category:Deadcode "condition '%a' %sis always %B" d_exp exp cilinserted tv
| `Bot (* all branches dead? can happen at our inserted Neg(1)-s because no Pos(1) *)
| `Bot when not (CilType.Exp.equal exp one) -> (* all branches dead *)
M.error ~loc:(Node g) ~category:Analyzer ~tags:[Category Unsound] "both branches over condition '%a' are dead" d_exp exp
| `Bot (* all branches dead, fine at our inserted Neg(1)-s because no Pos(1) *)
| `Top -> (* may be both true and false *)
()
) em;
Expand Down