diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-09-22 17:11:18 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-09-22 17:11:18 +0200 |
| commit | 8fcdd1d52fcaec72edbe2bb93054f007392065f6 (patch) | |
| tree | 5caa34fc9eb2d261b9f5bdd5d877b430d6fa0350 /cfrontend/C2C.ml | |
| parent | 036ecd1ba42585b51fffd70593106aa57fb40b29 (diff) | |
| download | compcert-kvx-8fcdd1d52fcaec72edbe2bb93054f007392065f6.tar.gz compcert-kvx-8fcdd1d52fcaec72edbe2bb93054f007392065f6.zip | |
Catch case of zero in builtin debug.
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index d7b26322..92abac68 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -757,8 +757,8 @@ let rec convertExpr env e = | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) -> let (kind, args1) = match args with - | {edesc = C.EConst(CInt(n,_,_))} :: args1 -> (n, args1) - | _ -> error "argument 1 of '__builtin_debug' must be a constant"; (1L, args) in + | {edesc = C.EConst(CInt(n,_,_))} :: args1 when n <> 0L-> (n, args1) + | _ -> error "argument 1 of '__builtin_debug' must be a non-zero constant"; (1L, args) in let (text, args2) = match args1 with | {edesc = C.EConst(CStr(txt))} :: args2 -> (txt, args2) |