diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-25 10:11:07 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-25 10:11:07 +0200 |
| commit | 7a88871feb652a3b094f3fdc8c7e933ab6eb16d3 (patch) | |
| tree | 498584f7a87e695de53940042479ebf0213effb6 /cfrontend/C2C.ml | |
| parent | 92ffa31ffc6d7a82d1949b86f0585f149c7615d8 (diff) | |
| download | compcert-kvx-7a88871feb652a3b094f3fdc8c7e933ab6eb16d3.tar.gz compcert-kvx-7a88871feb652a3b094f3fdc8c7e933ab6eb16d3.zip | |
Simplify test. Bug 19629
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 5 |
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) = |