diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-07 10:29:58 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-07 10:29:58 +0100 |
| commit | 178e71c74a034d7ea13645ab843f4dd0e23a3255 (patch) | |
| tree | 13d0dc4d81f7742043b086b751b96659e2d79ae4 /cparser/Cflow.ml | |
| parent | 5a7fc8637ae82d9aaf71c0053078a950ddee3b89 (diff) | |
| download | compcert-kvx-178e71c74a034d7ea13645ab843f4dd0e23a3255.tar.gz compcert-kvx-178e71c74a034d7ea13645ab843f4dd0e23a3255.zip | |
Control-flow analysis: wrong flow for "case"/"default" statements
Those labeled statements can be entered either by fall-through or by the enclosing switch.
Diffstat (limited to 'cparser/Cflow.ml')
| -rw-r--r-- | cparser/Cflow.ml | 10 |
1 files changed, 6 insertions, 4 deletions
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 |