Jessie3: support for division, and beginning of arrays

src/jessie/ACSLtoWhy3.ml

@@ -74,6 +74,10 @@ let le_int : Term.lsymbol = find int_theory "infix <="
 let gt_int : Term.lsymbol = find int_theory "infix >"
 let lt_int : Term.lsymbol = find int_theory "infix <"
 
+let computer_div_theory : Theory.theory = 
+  Env.find_theory env ["int"] "ComputerDivision"
+let div_int : Term.lsymbol = find computer_div_theory "div"
+
 (* real.Real theory *)
 let real_type : Ty.ty = Ty.ty_real
 let real_theory : Theory.theory = Env.find_theory env ["real"] "Real"
@@ -106,6 +110,21 @@ let get_fun : Mlw_expr.psymbol =
 let set_fun : Mlw_expr.psymbol =
   Mlw_module.ns_find_ps ref_module.Mlw_module.mod_export ["infix :="]
 
+(* array.Array module *)
+
+let array_modules, array_theories =
+  Env.read_lib_file (Mlw_main.library_of_env env) ["array"]
+
+let array_module : Mlw_module.modul = Stdlib.Mstr.find "Array" array_modules
+
+let array_type : Mlw_ty.T.itysymbol =
+  match
+    Mlw_module.ns_find_ts array_module.Mlw_module.mod_export ["array"]
+  with
+    | Mlw_module.PT itys -> itys
+    | Mlw_module.TS _ -> assert false
+
+
 
 (*********)
 (* types *)
@@ -119,8 +138,7 @@ let ctype ty =
     | TInt (_, _) -> Mlw_ty.ity_pur Ty.ts_int []
     | TFloat (_, _) -> 
       Self.not_yet_implemented "ctype TFloat"
-    | TPtr (_, _) -> 
-      Self.not_yet_implemented "ctype TPtr"
+    | TPtr(ty, _attr) -> array_type
     | TArray (_, _, _, _) -> 
       Self.not_yet_implemented "ctype TArray"
     | TFun (_, _, _, _) -> 
@@ -229,9 +247,17 @@ let bin (ty1,t1) op (ty2,t2) =
       Cil.d_logic_type ty1 Cil.d_logic_type ty2
     | MinusA,_,_ -> Self.not_yet_implemented "bin MinusA"
     | Mult,_,_ -> Self.not_yet_implemented "bin Mult"
-    | ((PlusPI|IndexPI|MinusPI|MinusPP|Div|Mod|Shiftlt|Shiftrt|Lt|Gt|
- Le|Ge|Eq|Ne|BAnd|BXor|BOr|LAnd|LOr),_, _)
-      -> Self.not_yet_implemented "bin"
+    | (PlusPI|IndexPI|MinusPI|MinusPP),_,_
+      -> Self.not_yet_implemented "bin Plus"
+    | Div,Linteger,Linteger -> t_app div_int [t1;t2]
+    | (Div|Mod),_,_
+      -> Self.not_yet_implemented "bin Div/Mod"
+    | (Shiftlt|Shiftrt),_,_
+      -> Self.not_yet_implemented "bin Shift"
+    | (Lt|Gt|Le|Ge|Eq|Ne),_,_
+      -> Self.not_yet_implemented "bin Lt..Ne"
+    | (BAnd|BXor|BOr|LAnd|LOr),_,_
+      -> Self.not_yet_implemented "bin BAnd..LOr"
 
 let unary op (ty,t) =
   match op,ty with

src/jessie/tests/demo/binary_search.c

@@ -5,12 +5,13 @@
 
 //@ lemma mean: \forall integer x, y; x <= y ==> x <= (x+y)/2 <= y;
 
-/*@ predicate sorted{L}(long *t, integer a, integer b) =
+/* predicate sorted{L}(long *t, integer a, integer b) =
   @    \forall integer i,j; a <= i <= j <= b ==> t[i] <= t[j];
   @*/
 
 /*@ requires n >= 0 && \valid(t+(0..n-1));
-  @ requires sorted(t,0,n-1);
+  @ //requires sorted(t,0,n-1);
+  @ requires \forall integer i,j; 0 <= i <= j < n ==> t[i] <= t[j];
   @ ensures -1 <= \result < n;
   @ ensures \result >= 0 ==> t[\result] == v;
   @ ensures \result == -1 ==>