aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--cfrontend/C2C.ml5
1 files changed, 1 insertions, 4 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 07de331e..6b469434 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -758,10 +758,7 @@ 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 ->
- if n <= 0L then begin
- error "ill_formed __builtin_debug"; (1L,args1)
- end else
+ | {edesc = C.EConst(CInt(n,_,_))} :: args1 when n > 0L ->
(n, args1)
| _ -> error "ill_formed __builtin_debug"; (1L, args) in
let (text, args2) =