Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
dd52585e
Commit
dd52585e
authored
Apr 03, 2015
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
jessie3: oracles updated
parent
b424b944
Changes
7
Hide whitespace changes
Inline
Side-by-side
Showing
7 changed files
with
116 additions
and
61 deletions
+116
-61
src/jessie/tests/basic/oracle/array.res.oracle
src/jessie/tests/basic/oracle/array.res.oracle
+6
-1
src/jessie/tests/basic/oracle/axiomatic.res.oracle
src/jessie/tests/basic/oracle/axiomatic.res.oracle
+28
-20
src/jessie/tests/basic/oracle/forty-two.res.oracle
src/jessie/tests/basic/oracle/forty-two.res.oracle
+5
-4
src/jessie/tests/basic/oracle/generic.res.oracle
src/jessie/tests/basic/oracle/generic.res.oracle
+20
-12
src/jessie/tests/basic/oracle/incr.res.oracle
src/jessie/tests/basic/oracle/incr.res.oracle
+5
-4
src/jessie/tests/basic/oracle/lemma.res.oracle
src/jessie/tests/basic/oracle/lemma.res.oracle
+24
-16
src/jessie/tests/demo/oracle/binary_search.res.oracle
src/jessie/tests/demo/oracle/binary_search.res.oracle
+28
-4
No files found.
src/jessie/tests/basic/oracle/array.res.oracle
View file @
dd52585e
[kernel] preprocessing with "gcc -C -E -I. tests/basic/array.c"
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/basic/array.c (with preprocessing)
[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.
src/jessie/tests/basic/oracle/axiomatic.res.oracle
View file @
dd52585e
[kernel] preprocessing with "gcc -C -E -I. tests/basic/axiomatic.c"
[jessie3] creating logic symbol 739 (f1)
[jessie3] creating logic symbol 743 (occ)
[jessie3] creating logic symbol 748 (singleton)
[jessie3] creating logic symbol 754 (bag_union)
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/basic/axiomatic.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] creating logic symbol 68 (f1)
[jessie3] creating logic symbol 72 (occ)
[jessie3] creating logic symbol 77 (singleton)
[jessie3] creating logic symbol 83 (bag_union)
[jessie3] found 1 logic decl(s)
[jessie3] made 3 theory(ies)
[jessie3] made 0 function(s)
[jessie3] Running provers...
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations
(* use why3.BuiltIn *)
(* use why3.BuiltIn
.BuiltIn
*)
(* use int.Int *)
...
...
@@ -20,11 +28,11 @@
lemma l1 : forall x:int. f1 x >= 1
end
[jessie3] Provers: Alt-Ergo 0.95.
1
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (l1): Valid, Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.
2, CVC4 1.4
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (l1): Valid,
Unknown,
Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory BagInt
(* use why3.BuiltIn *)
(* use why3.BuiltIn
.BuiltIn
*)
(* use int.Int *)
...
...
@@ -56,11 +64,11 @@
lemma l2 : f1 1 = 2
end
[jessie3] Provers: Alt-Ergo 0.95.
1
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (l2): Valid, Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.
2, CVC4 1.4
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (l2): Valid, Valid, Valid, Valid
, Valid
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations1
(* use why3.BuiltIn *)
(* use why3.BuiltIn
.BuiltIn
*)
(* use int.Int *)
...
...
@@ -72,17 +80,17 @@
lemma union_comm : forall b1:bag, b2:bag. bag_union b1 b2 = bag_union b2 b1
end
[jessie3] Provers: Alt-Ergo 0.95.
1
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (union_comm): Unknown,
Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.
2, CVC4 1.4
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (union_comm): Unknown,
Unknown, Unknown, Timeout, Timeout
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
(* use why3.BuiltIn
.BuiltIn
*)
(* use why3.Bool *)
(* use why3.Bool
.Bool
*)
(* use why3.Unit *)
(* use why3.Unit
.Unit
*)
(* use why3.Prelude *)
(* use why3.Prelude
.Prelude
*)
(* use int.Int *)
...
...
@@ -94,6 +102,6 @@
(* use ref.Ref *)
(* use mach
_
int.Int32 *)
(* use mach
.
int.Int32 *)
end
[jessie3] Provers: Alt-Ergo 0.95.
1
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.95.
2, CVC4 1.4
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
src/jessie/tests/basic/oracle/forty-two.res.oracle
View file @
dd52585e
...
...
@@ -2,13 +2,14 @@
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] preprocessing with "gcc -C -E -I. tests/basic/forty-two.c"
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/basic/forty-two.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] processing function f
[jessie3] created program function f (
75
7)
[jessie3] created program function f (
6
7)
[jessie3] processing function g
[jessie3] created program function g (
75
9)
[jessie3] created program function g (
6
9)
[jessie3] found 0 logic decl(s)
[jessie3] made 0 theory(ies)
[jessie3] made 2 function(s)
...
...
@@ -53,4 +54,4 @@
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter f): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2 (WP_parameter g): Valid,
Unknown
, Valid,
Valid, Valid
[jessie3] Task 2 (WP_parameter g): Valid,
Timeout
, Valid,
Timeout, Timeout
src/jessie/tests/basic/oracle/generic.res.oracle
View file @
dd52585e
[kernel] preprocessing with "gcc -C -E -I. tests/basic/generic.c"
[jessie3] creating logic symbol 740 (occ)
[jessie3] creating logic symbol 742 (singleton)
[jessie3] creating logic symbol 745 (bag_union)
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/basic/generic.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] creating logic symbol 69 (occ)
[jessie3] creating logic symbol 71 (singleton)
[jessie3] creating logic symbol 74 (bag_union)
[jessie3] found 0 logic decl(s)
[jessie3] made 1 theory(ies)
[jessie3] made 0 function(s)
[jessie3] Running provers...
[jessie3] running theory 1:
[jessie3] theory Bag
(* use why3.BuiltIn *)
(* use why3.BuiltIn
.BuiltIn
*)
(* use int.Int *)
...
...
@@ -23,16 +31,16 @@
function bag_union (bag 'x) (bag 'x) : bag 'x
end
[jessie3] Provers: Alt-Ergo 0.95.
1
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.95.
2, CVC4 1.4
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
(* use why3.BuiltIn
.BuiltIn
*)
(* use why3.Bool *)
(* use why3.Bool
.Bool
*)
(* use why3.Unit *)
(* use why3.Unit
.Unit
*)
(* use why3.Prelude *)
(* use why3.Prelude
.Prelude
*)
(* use int.Int *)
...
...
@@ -44,6 +52,6 @@
(* use ref.Ref *)
(* use mach
_
int.Int32 *)
(* use mach
.
int.Int32 *)
end
[jessie3] Provers: Alt-Ergo 0.95.
1
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.95.
2, CVC4 1.4
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
src/jessie/tests/basic/oracle/incr.res.oracle
View file @
dd52585e
...
...
@@ -2,13 +2,14 @@
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] preprocessing with "gcc -C -E -I. tests/basic/incr.c"
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/basic/incr.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] processing function f
[jessie3] created program function f (
75
7)
[jessie3] created program function f (
6
7)
[jessie3] processing function h
[jessie3] created program function h (7
6
3)
[jessie3] created program function h (73)
[jessie3] found 0 logic decl(s)
[jessie3] made 0 theory(ies)
[jessie3] made 3 function(s)
...
...
@@ -60,4 +61,4 @@
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter f): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2 (WP_parameter h): Valid, Valid, Valid,
Valid, Valid
[jessie3] Task 2 (WP_parameter h): Valid, Valid, Valid,
Timeout, Timeout
src/jessie/tests/basic/oracle/lemma.res.oracle
View file @
dd52585e
[kernel] preprocessing with "gcc -C -E -I. tests/basic/lemma.c"
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/basic/lemma.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] found 7 logic decl(s)
[jessie3] made 1 theory(ies)
[jessie3] made 0 function(s)
[jessie3] Running provers...
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations
(* use why3.BuiltIn *)
(* use why3.BuiltIn
.BuiltIn
*)
(* use int.Int *)
...
...
@@ -26,23 +34,23 @@
lemma test4r : forall x:real, y:real. (x - y) = (- (y - x))
end
[jessie3] Provers: Alt-Ergo 0.95.
1
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (test1): Valid, Valid, Valid, Valid
[jessie3] Task 2 (test2): Valid, Valid, Valid, Valid
[jessie3] Task 3 (test2r): Valid, Unknown, Valid, Valid
[jessie3] Task 4 (test3): Valid, Valid, Valid, Valid
[jessie3] Task 5 (test3r): Valid, Valid, Valid, Valid
[jessie3] Task 6 (test4): Valid, Valid, Valid, Valid
[jessie3] Task 7 (test4r): Valid, Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.
2, CVC4 1.4
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (test1): Valid, Valid, Valid, Valid
, Valid
[jessie3] Task 2 (test2): Valid,
Unknown,
Valid, Valid, Valid
[jessie3] Task 3 (test2r): Valid, Unknown,
Unknown,
Valid, Valid
[jessie3] Task 4 (test3): Valid, Valid, Valid, Valid
, Valid
[jessie3] Task 5 (test3r): Valid, Valid, Valid, Valid
, Valid
[jessie3] Task 6 (test4): Valid, Valid, Valid, Valid
, Valid
[jessie3] Task 7 (test4r): Valid, Valid, Valid, Valid
, Valid
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
(* use why3.BuiltIn
.BuiltIn
*)
(* use why3.Bool *)
(* use why3.Bool
.Bool
*)
(* use why3.Unit *)
(* use why3.Unit
.Unit
*)
(* use why3.Prelude *)
(* use why3.Prelude
.Prelude
*)
(* use int.Int *)
...
...
@@ -54,6 +62,6 @@
(* use ref.Ref *)
(* use mach
_
int.Int32 *)
(* use mach
.
int.Int32 *)
end
[jessie3] Provers: Alt-Ergo 0.95.
1
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.95.
2, CVC4 1.4
, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
src/jessie/tests/demo/oracle/binary_search.res.oracle
View file @
dd52585e
[kernel] preprocessing with "gcc -C -E -I. tests/demo/binary_search.c"
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/demo/binary_search.c (with preprocessing)
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[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] ctype TPtr(TInt,_)'.
[jessie3] created program function binary_search (69)
[jessie3] failure: Exception raised when loading prover drivers:
anomaly: Log.FeatureRequest("jessie3", "stmt Goto")
[kernel] Current source was: tests/demo/binary_search.c:21
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "register.ml", line 87, characters 6-113
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in jessie3 aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment