diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-17 13:49:46 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-17 13:49:46 +0100 |
commit | c0eb337aff9fe81733b15fceb79d92f7d52f1dfd (patch) | |
tree | 53033d09c37e29a391a4c7d23e428ad8d51b8c83 | |
parent | 920686c5feabda7a7b7310e89e9d0e18a822284e (diff) | |
download | compcert-c0eb337aff9fe81733b15fceb79d92f7d52f1dfd.tar.gz compcert-c0eb337aff9fe81733b15fceb79d92f7d52f1dfd.zip |
Control-flow analysis: bug in switch without default
If no 'default' case appears in a 'switch', one is implicit at the end of the switch body, making possible to have a fall-through behavior.
-rw-r--r-- | cparser/Cflow.ml | 31 |
1 files changed, 30 insertions, 1 deletions
diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml index 7b3d3d32..c7236ce8 100644 --- a/cparser/Cflow.ml +++ b/cparser/Cflow.ml @@ -173,6 +173,33 @@ let loop (s: flow) : flow = fun i -> the fallthrough exit. *) { o with onormal = false } +(* Detect the presence of a 'default' case reachable from an enclosing + 'switch' *) + +let rec contains_default s = + match s.sdesc with + | Sskip -> false + | Sdo _ -> false + | Sseq(s1, s2) -> contains_default s1 || contains_default s2 + | Sif(e, s1, s2) -> contains_default s1 || contains_default s2 + | Swhile(e, s) -> contains_default s + | Sdowhile(s, e) -> contains_default s + | Sfor(s1, e, s2, s3) -> + contains_default s1 || contains_default s2 || contains_default s3 + | Sbreak -> false + | Scontinue -> false + | Sswitch(e, s) -> false + (* the default that could appear inside the switch + cannot be reached by the enclosing switch *) + | Slabeled(Sdefault, s) -> true + | Slabeled(_, s) -> contains_default s + | Sgoto lbl -> false + | Sreturn opte -> false + | Sblock sl -> List.exists contains_default sl + | Sdecl dcl -> false + | Sasm _ -> false + + (* This is the main analysis function. Given a C statement [s] it returns a flow that overapproximates the behavior of [s]. *) @@ -214,7 +241,9 @@ let rec outcomes env s : flow = | Scontinue -> continue | Sswitch(e, s) -> - catch_break (switch (outcomes env s)) + let fl = catch_break (switch (outcomes env s)) in + if contains_default s then fl else either normal fl + (* if there is no 'default' case, the switch can fall through *) | Slabeled(Slabel lbl, s) -> label lbl (outcomes env s) | Slabeled((Scase _ | Sdefault), s) -> |