Jessie3: isqrt.c proved, yahoo !

src/jessie/ACSLtoWhy3.ml

@@ -419,6 +419,9 @@ let rel (ty1,t1) op (ty2,t2) =
     | Req,_,_ -> Term.t_equ t1 t2
     | Rneq,_,_ -> Term.t_neq t1 t2
     | Rge,Linteger,Linteger -> t_app ge_int [t1;t2]
+    | Rle,Linteger,Linteger -> t_app le_int [t1;t2]
+    | Rgt,Linteger,Linteger -> t_app gt_int [t1;t2]
+    | Rlt,Linteger,Linteger -> t_app lt_int [t1;t2]
     | Rge,Lreal,Lreal -> t_app ge_real [t1;t2]
     | Rge,_,_ ->
       Self.not_yet_implemented "rel Rge"
@@ -633,18 +636,22 @@ let annot a e =
     Self.not_yet_implemented "annot APragma"
 
 let loop_annot a =
-  List.fold_left (fun (_inv,_var) a ->
-    match a.annot_content with
+  List.fold_left (fun (inv,var) a ->
+    match (Annotations.code_annotation_of_rooted a).annot_content with
       | AAssert ([],_pred) ->
         Self.not_yet_implemented "loop_annot AAssert"
       | AAssert(_labels,_pred) ->
         Self.not_yet_implemented "loop_annot AAssert"
       | AStmtSpec _ ->
         Self.not_yet_implemented "loop_annot AStmtSpec"
+      | AInvariant([],true,p) ->
+        (Term.t_and inv (predicate_named ~label:Here p),var)
       | AInvariant _ ->
         Self.not_yet_implemented "loop_annot AInvariant"
-      | AVariant _ ->
-        Self.not_yet_implemented "loop_annot AVariant"
+      | AVariant (t, None) ->
+        (inv,(snd (term ~label:Here t),None)::var)
+      | AVariant (_var, Some _) ->
+        Self.not_yet_implemented "loop_annot AVariant/Some"
       | AAssigns _ ->
         Self.not_yet_implemented "loop_annot AAssigns"
       | AAllocation _ ->
@@ -767,6 +774,8 @@ let rec stmt s =
           with Continue -> ()
         with Break -> ()
       *)
+      assert (annots = []);
+      let annots = Annotations.code_annot s in
       let inv, var = loop_annot annots in
       let v =
         Mlw_ty.create_pvsymbol (Ident.id_fresh "_dummy")

src/jessie/tests/basic/oracle/isqrt.res.oracle

@@ -3,6 +3,57 @@
 [jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
 [jessie3] creating logic symbol 739 (sqr)
 [jessie3] processing function isqrt
-[kernel] Plug-in jessie3 aborted: unimplemented feature.
-         You may send a feature request at http://bts.frama-c.com with:
-         '[Plug-in jessie3] rel'.
+[jessie3] found 1 logic decl(s)
+[jessie3] made 1 theory(ies)
+[jessie3] made 1 function(s)
+[jessie3] running theory 1:
+[jessie3] theory Global_logic_declarations
+            (* use why3.BuiltIn *)
+            
+            (* use int.Int *)
+            
+            (* use real.Real *)
+            
+            function sqr (x:int) : int = x * x
+            end
+[jessie3] Alt-Ergo 0.94, Alt-Ergo 0.95, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
+[jessie3] running theory 1:
+[jessie3] theory C_Functions
+            (* use why3.BuiltIn *)
+            
+            (* use why3.Bool *)
+            
+            (* use why3.Unit *)
+            
+            (* use why3.Prelude *)
+            
+            (* use int.Int *)
+            
+            (* use real.Real *)
+            
+            (* use Global_logic_declarations *)
+            
+            (* use ref.Ref *)
+            
+            goal WP_parameter_isqrt :
+              forall x:int.
+               x >= 0 ->
+                (forall count:int.
+                  count = 0 ->
+                   (forall sum:int.
+                     sum = 1 ->
+                      ((count >= 0 /\ x >= sqr count) /\ sum = sqr (count + 1)) /\
+                       (forall sum1:int, count1:int.
+                         (count1 >= 0 /\ x >= sqr count1) /\ sum1 = sqr (count1 + 1) ->
+                          (if sum1 <= x then forall count2:int.
+                                              count2 = (count1 + 1) ->
+                                               (forall sum2:int.
+                                                 sum2 = (sum1 + ((2 * count2) + 1)) ->
+                                                  ((count2 >= 0 /\ x >= sqr count2) /\
+                                                    sum2 = sqr (count2 + 1)) /\
+                                                   0 <= (x - count1) /\
+                                                    (x - count2) < (x - count1))
+                          else (count1 >= 0 /\ sqr count1 <= x) /\ x < sqr (count1 + 1)))))
+            end
+[jessie3] Alt-Ergo 0.94, Alt-Ergo 0.95, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
+[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid, Valid