Skip to content
Snippets Groups Projects
Commit a5067054 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'feature/eva/fix-deadcode-request' into 'master'

[ivette/eva] fix dead-code exception

See merge request frama-c/frama-c!3750
parents 0f102451 d373939e
No related branches found
No related tags found
No related merge requests found
...@@ -116,20 +116,22 @@ let dead_code kf = ...@@ -116,20 +116,22 @@ let dead_code kf =
let empty = { kf; unreachable = []; non_terminating = [] } in let empty = { kf; unreachable = []; non_terminating = [] } in
if Analysis.is_computed () if Analysis.is_computed ()
then then
let fundec = Kernel_function.get_definition kf in try
match Analysis.status kf with let fundec = Kernel_function.get_definition kf in
| Unreachable | SpecUsed | Builtin _ -> match Analysis.status kf with
{ kf; unreachable = fundec.sallstmts; non_terminating = [] } | Unreachable | SpecUsed | Builtin _ ->
| Analyzed NoResults -> empty { kf; unreachable = fundec.sallstmts; non_terminating = [] }
| Analyzed (Partial | Complete) -> | Analyzed NoResults -> empty
let classify acc stmt = | Analyzed (Partial | Complete) ->
if Results.(before stmt |> is_empty) let classify acc stmt =
then { acc with unreachable = stmt :: acc.unreachable } if Results.(before stmt |> is_empty)
else if Results.(after stmt |> is_empty) then { acc with unreachable = stmt :: acc.unreachable }
then { acc with non_terminating = stmt :: acc.non_terminating } else if Results.(after stmt |> is_empty)
else acc then { acc with non_terminating = stmt :: acc.non_terminating }
in else acc
List.fold_left classify empty fundec.sallstmts in
List.fold_left classify empty fundec.sallstmts
with Kernel_function.No_Definition -> empty
else empty else empty
let () = Request.register ~package let () = Request.register ~package
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment