From 178e71c74a034d7ea13645ab843f4dd0e23a3255 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 7 Feb 2017 10:29:58 +0100 Subject: Control-flow analysis: wrong flow for "case"/"default" statements Those labeled statements can be entered either by fall-through or by the enclosing switch. --- cparser/Cflow.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'cparser/Cflow.ml') diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml index 49a85332..dfa6ad72 100644 --- a/cparser/Cflow.ml +++ b/cparser/Cflow.ml @@ -94,14 +94,16 @@ let catch_break (s: flow) : flow = fun i is -> let o = s i is in if can _Break o then add _Fallthrough (remove _Break o) else o -(* For goto-labeled statements we assume they can always be entered normally. *) +(* For goto-labeled statements we assume they can always be entered by + a goto. *) let label (s: flow) : flow = fun i is -> s true is -(* For "case" and "default" labeled statements, we assume they can be entered - normally as soon as the nearest enclosing "switch" can be entered normally. *) +(* For "case" and "default" labeled statements, we assume they can be + entered normally as soon as the nearest enclosing "switch" can be + entered normally. *) -let case (s: flow) : flow = fun i is -> s is is +let case (s: flow) : flow = fun i is -> s (i || is) is let switch (s: flow) : flow = fun i is -> s false i -- cgit