Add square root to extraction

drivers/c.drv

@@ -16,6 +16,10 @@ module ref.Ref
   syntax val (:=) "%1 = %2"      prec 14 13 14
 end
 
+module mach.int.Bounded_int
+  syntax val of_int "%1"         prec 0
+end
+
 module mach.int.Int32
 
   syntax type int32  "int32_t"
@@ -536,15 +540,20 @@ static struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
 
   syntax val lsl "%1 << %2" prec 5 5 4
   syntax val lsr "%1 >> %2" prec 5 5 4
+  syntax val lsl_mod "%1 << %2" prec 5 5 4
+  syntax val lsr_mod "%1 >> %2" prec 5 5 4
 
   syntax val is_msb_set "%1 & 0x8000000000000000ULL" prec 8 7
 
   syntax val count_leading_zeros "__builtin_clzll(%1)" prec 1 15
 
+  syntax val to_int32 "(int32_t)%1" prec 2 2
   syntax val of_int32 "(uint64_t)%1" prec 2 2
   syntax val to_int64 "(int64_t)%1" prec 2 2
   syntax val of_int64 "(uint64_t)%1" prec 2 2
 
+  syntax val of_int "%1" prec 0
+
 end
 
 module mach.array.Array32

examples/multiprecision/Makefile

@@ -29,7 +29,7 @@ why3:
 dir:
 	mkdir -p build
 
-MLWFILES= $(addsuffix .mlw, sqrt toom logical div mul sub add compare util)
+MLWFILES= $(addsuffix .mlw, sqrtrem sqrt toom logical div mul sub add compare util)
 
 cfiles: why3 dir
 	$(WHY3) extract -D wmpn.drv -D c -L . --recursive --modular --interface -o build/ \
@@ -38,7 +38,7 @@ cfiles: why3 dir
 
 extract: why3 dir cfiles
 
-CFILES = build/uint64gmp.c build/fxp.c build/sqrt1.c build/toom.c build/div.c build/logical.c build/mul.c build/sub.c build/add.c build/compare.c build/util.c build/int32.c
+CFILES = build/uint64gmp.c build/fxp.c build/sqrt.c build/sqrt1.c build/toom.c build/div.c build/logical.c build/mul.c build/sub.c build/add.c build/compare.c build/util.c build/int32.c
 
 tests: extract check-gmp
 	gcc $(CFLAGS) tests.c $(CFILES) -Iinclude -I$(GMP_DIR) -Irandom -L$(GMP_LIB) -lgmp -o build/tests

examples/multiprecision/wmpn.mlw

@@ -11,5 +11,6 @@ module Wmpn
   use export div.Div
   use export toom.Toom
   use export sqrt.Sqrt1
+  use export sqrtrem.Sqrt
 
 end
\ No newline at end of file