Commit d9732c3c authored by MARCHE Claude's avatar MARCHE Claude
Browse files

jessie3: updated oracles

parent 86d1574d
......@@ -484,6 +484,24 @@ One can run provers on those tasks exactly as we did above.
See the example \verb|examples/use_api/create_session.ml| of the distribution for
an illustration on how to manipulate proof sessions from an OCaml program.
\section{ML programs}
There are two ways for building WhyML programs from OCaml. The first
is to build untyped syntax trees for such WhyML programs, and then
call the Why3 typing procedure to build typed declarations. The second
way is to directly build typed programs using smart constructors that
check well-typedness at each step.
The first approach, building untyped trees and then typed them, is
examplified in file \verb|examples/use_api/mlw_tree.ml| of the
distribution. The second approach is
examplified in file \verb|examples/use_api/mlw.ml|. The first approach
is significantly simpler to do since the internal typing mechanism
using regions remains implicit, whereas when one uses the second
approach one should care about such typing. On the other hand, the
second approach is more `''efficient'' in the sense that no
intermediate form needs to be built in memory.
......
[kernel] preprocessing with "gcc -C -E -I. tests/basic/array.c"
[kernel] user error: cannot find entry point `main'.
Please use option `-main' for specifying a valid entry point.
[kernel] Frama-C aborted: invalid user input.
......@@ -18,8 +18,8 @@
lemma l1 : forall x:int. f1 x >= 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
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory BagInt
(* use why3.BuiltIn *)
......@@ -52,8 +52,8 @@
lemma l2 : f1 1 = 2
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
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations1
(* use why3.BuiltIn *)
......@@ -66,8 +66,8 @@
lemma union_comm : forall b1:bag, b2:bag. bag_union b1 b2 = bag_union b2 b1
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: Unknown, Unknown, Valid, Valid, Valid, Valid
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1: Unknown, Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
......@@ -86,4 +86,4 @@
(* use ref.Ref *)
end
[jessie3] Alt-Ergo 0.94, Alt-Ergo 0.95, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
......@@ -20,12 +20,12 @@
lemma test4 : 0x1.1p4 = 17.0
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
[jessie3] Task 2: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Task 3: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Task 4: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Task 5: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 3: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 4: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 5: Valid, Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
......@@ -44,4 +44,4 @@
(* use ref.Ref *)
end
[jessie3] Alt-Ergo 0.94, Alt-Ergo 0.95, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
......@@ -25,6 +25,6 @@
goal WP_parameter_g :
forall us_retres:int. us_retres = (6 * 7) -> us_retres = 42
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
[jessie3] Task 2: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2: Valid, Valid, Valid, Valid, Valid
......@@ -21,7 +21,7 @@
function bag_union (bag 'x) (bag 'x) : bag '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] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
......@@ -40,4 +40,4 @@
(* use ref.Ref *)
end
[jessie3] Alt-Ergo 0.94, Alt-Ergo 0.95, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
......@@ -27,6 +27,6 @@
goal WP_parameter_h :
forall x:int. forall g:int. forall g1:int. g1 = (g + x) -> g1 = (g + 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] Task 1: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2: Valid, Valid, Valid, Valid, Valid
......@@ -24,14 +24,14 @@
lemma test4r : forall x:real, y:real. (x - y) = (- (y - 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] Task 1: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Task 3: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Task 4: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Task 5: Valid, Valid, Unknown, Unknown, Valid, Valid
[jessie3] Task 6: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Task 7: Valid, Valid, Valid, Valid, Valid, Valid
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 3: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 4: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 5: Valid, Unknown, Unknown, Valid, Valid
[jessie3] Task 6: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 7: Valid, Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
......@@ -50,4 +50,4 @@
(* use ref.Ref *)
end
[jessie3] Alt-Ergo 0.94, Alt-Ergo 0.95, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[kernel] preprocessing with "gcc -C -E -I. tests/demo/binary_search.c"
[jessie3] processing function binary_search
[kernel] Plug-in jessie3 aborted: unimplemented feature.
You may send a feature request at http://bts.frama-c.com with:
'[Plug-in jessie3] bin'.
'[Plug-in jessie3] predicate'.
......@@ -14,7 +14,7 @@
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] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
......@@ -53,5 +53,5 @@
(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
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
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