aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cflow.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-02-16 15:53:06 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-02-16 15:53:06 +0100
commit9b63d90b40974eed35bd199fcfc6ccbabb1ed5b7 (patch)
treec5937772c4a783fae8f0306b62dec1a6a5f39ec1 /cparser/Cflow.ml
parent380ef884523013fd02fe1c52b05d3b2a5b0b8818 (diff)
downloadcompcert-kvx-9b63d90b40974eed35bd199fcfc6ccbabb1ed5b7.tar.gz
compcert-kvx-9b63d90b40974eed35bd199fcfc6ccbabb1ed5b7.zip
Reverted changes in Cutil and catch in Cflow.
Instead of changing the definition of sizeof we now ignore errors raise in the Cflow module. Bug 21005
Diffstat (limited to 'cparser/Cflow.ml')
-rw-r--r--cparser/Cflow.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml
index f5408c15..790d9079 100644
--- a/cparser/Cflow.ml
+++ b/cparser/Cflow.ml
@@ -117,6 +117,7 @@ let resolve_test env e =
match Ceval.integer_expr env e with
| None -> None
| Some n -> Some (n <> 0L)
+ | exception Env.Error _ -> None (* Any error due to local types should be ignored *)
let if_ env e (s1: flow) (s2: flow) : flow =
match resolve_test env e with