diff options
| author |  Jade Philipoom <jadep@google.com> | 2018-04-11 10:10:13 +0200 |
|---|---|---|
| committer | Jade Philipoom <jadep@google.com> | 2018-04-11 10:10:13 +0200 |
| commit | 0d2f18249f65211ad6fe318e193bfdf43d244303 (patch) | |
| tree | 5f42c59e98a36618848db798802e98f290a807e4 /src | |
| parent | 6863349da1bbdecaa7eac88188dff8369aae0249 (diff) | |
fix trashed carry flag
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 4c0ff4e95..71fca4645 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -5189,13 +5189,16 @@ Module Compilers. | inr xx => if Z.eqb xx 0 then default_no_carry a else default_with_carry a | _ => default_with_carry a end in - match (z,a) with - | (inr xx, inl e) - | (inl e, inr xx) - => if Z.eqb xx 0 - then inr (inl e, inr 0%Z) - else default tt - | _ => default tt + match y,z,a with + | inr yy, inr xx, inl e + | inr yy, inl e, inr xx + => + if Z.eqb yy 0 + then if Z.eqb xx 0 + then inr (inl e, inr 0%Z) + else default_no_carry tt + else default_with_carry tt + | _,_,_ => default tt end | _ => default_interp idc x_y_z_a end |