Revision 1d0fd52b
Added by Xavier Thirioux about 4 years ago
| src/backends/C/c_backend_common.ml | ||
|---|---|---|
| 121 | 121 |
let pp_div pp_val v1 v2 fmt = |
| 122 | 122 |
if !Options.integer_div_euclidean then |
| 123 | 123 |
(* (a - ((a mod_C b) + (a mod_C b < 0 ? abs(b) : 0))) div_C b *) |
| 124 |
Format.fprintf fmt "(%a - ((%a %% %a) + ((%a %% %a) < 0 ? abs(%a) : 0))) / %a"
|
|
| 124 |
Format.fprintf fmt "(%a - %t) / %a"
|
|
| 125 | 125 |
pp_val v1 |
| 126 |
pp_val v1 pp_val v2 |
|
| 127 |
pp_val v1 pp_val v2 |
|
| 128 |
pp_val v2 |
|
| 126 |
(pp_mod pp_val v1 v2) |
|
| 129 | 127 |
pp_val v2 |
| 130 | 128 |
else (* Regular behavior: printing a / *) |
| 131 | 129 |
Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2 |
Also available in: Unified diff
updated division for Horn clauses