Commit 2e08c89a authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

C extraction: use partial for C assert

parent 3632be0d
......@@ -3970,7 +3970,6 @@ let wmpn_divrem_1 (q x:t) (y:limb) (sz:int32) : limb
= value q (sx - sy + 1) * value y sy
+ value r sy }
ensures { value r sy < value y sy }
diverges
=
let nx = malloc (UInt32.(+) (UInt32.of_int32 sx) 1) in
c_assert (is_not_null nx);
......
......@@ -192,9 +192,8 @@ module C
ensures { forall i. old p2.min <= i < old p2.max ->
(pelts p2)[i] = old (pelts p2)[i] }
val c_assert (e:bool) : unit
val partial c_assert (e:bool) : unit
ensures { e }
diverges
(** Printing *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment