Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
122
Issues
122
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
038febb8
Commit
038febb8
authored
Feb 01, 2013
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
jessie3 in progress, stuck on application of ref.Ref.(!)
parent
ac9a4e43
Changes
10
Hide whitespace changes
Inline
Side-by-side
Showing
10 changed files
with
195 additions
and
159 deletions
+195
-159
src/jessie/ACSLtoWhy3.ml
src/jessie/ACSLtoWhy3.ml
+135
-49
src/jessie/literals.mll
src/jessie/literals.mll
+2
-2
src/jessie/register.ml
src/jessie/register.ml
+2
-1
src/jessie/tests/basic/oracle/axiomatic.res.oracle
src/jessie/tests/basic/oracle/axiomatic.res.oracle
+14
-14
src/jessie/tests/basic/oracle/constants.res.oracle
src/jessie/tests/basic/oracle/constants.res.oracle
+12
-12
src/jessie/tests/basic/oracle/forty-two.res.oracle
src/jessie/tests/basic/oracle/forty-two.res.oracle
+3
-20
src/jessie/tests/basic/oracle/generic.res.oracle
src/jessie/tests/basic/oracle/generic.res.oracle
+7
-7
src/jessie/tests/basic/oracle/incr.res.oracle
src/jessie/tests/basic/oracle/incr.res.oracle
+3
-20
src/jessie/tests/basic/oracle/isqrt.res.oracle
src/jessie/tests/basic/oracle/isqrt.res.oracle
+3
-20
src/jessie/tests/basic/oracle/lemma.res.oracle
src/jessie/tests/basic/oracle/lemma.res.oracle
+14
-14
No files found.
src/jessie/ACSLtoWhy3.ml
View file @
038febb8
...
...
@@ -83,25 +83,39 @@ let ge_real : Term.lsymbol = find real_theory "infix >="
(* ref.Ref module *)
let
ref_modules
,
ref_theories
=
let
ref_modules
,
ref_theories
=
Env
.
read_lib_file
(
Mlw_main
.
library_of_env
env
)
[
"ref"
]
let
ref_module
:
Mlw_module
.
modul
=
Stdlib
.
Mstr
.
find
"Ref"
ref_modules
let
ref_type
:
Mlw_ty
.
T
.
itysymbol
=
let
ref_type
:
Mlw_ty
.
T
.
itysymbol
=
match
Mlw_module
.
ns_find_ts
ref_module
.
Mlw_module
.
mod_export
[
"ref"
]
with
|
Mlw_module
.
PT
itys
->
itys
|
Mlw_module
.
TS
_
->
assert
false
let
ref_fun
:
Mlw_expr
.
psymbol
=
let
ref_fun
:
Mlw_expr
.
psymbol
=
match
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"ref"
]
with
|
Mlw_module
.
PS
p
->
p
|
_
->
assert
false
let
get_fun
:
Mlw_expr
.
psymbol
=
match
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"prefix !"
]
with
|
Mlw_module
.
PS
p
->
p
|
_
->
assert
false
let
set_fun
:
Mlw_expr
.
psymbol
=
match
Mlw_module
.
ns_find_ps
ref_module
.
Mlw_module
.
mod_export
[
"infix :="
]
with
|
Mlw_module
.
PS
p
->
p
|
_
->
assert
false
(*********)
(* types *)
...
...
@@ -152,7 +166,7 @@ let rec logic_type ty =
try
let
ts
=
Hashtbl
.
find
logic_types
lt
.
lt_name
in
Ty
.
ty_app
ts
(
List
.
map
logic_type
args
)
with
with
Not_found
->
Self
.
fatal
"logic type %s not found"
lt
.
lt_name
end
|
Lvar
v
->
Ty
.
ty_var
(
find_type_var
v
)
...
...
@@ -169,16 +183,16 @@ let rec logic_type ty =
(* terms *)
(*********)
let
constant
c
=
let
logic_
constant
c
=
match
c
with
|
Integer
(
_value
,
Some
s
)
->
let
c
=
Literals
.
integer
s
in
Term
.
ConstInt
c
|
Integer
(
_value
,
Some
s
)
->
let
c
=
Literals
.
integer
s
in
Number
.
ConstInt
c
|
Integer
(
_value
,
None
)
->
Self
.
not_yet_implemented
"constant Integer None"
Self
.
not_yet_implemented
"
logic_
constant Integer None"
|
LReal
(
_value
,
s
)
->
let
c
=
Literals
.
floating_point
s
in
Term
.
ConstReal
c
let
c
=
Literals
.
floating_point
s
in
Number
.
ConstReal
c
|
(
LStr
_
|
LWStr
_
|
LChr
_
|
LEnum
_
)
->
Self
.
not_yet_implemented
"constant"
Self
.
not_yet_implemented
"
logic_
constant"
let
t_app
ls
args
=
try
...
...
@@ -261,7 +275,7 @@ let tlval (host,offset) =
let
rec
term_node
t
=
match
t
with
|
TConst
cst
->
Term
.
t_const
(
constant
cst
)
|
TConst
cst
->
Term
.
t_const
(
logic_
constant
cst
)
|
TLval
lv
->
tlval
lv
|
TBinOp
(
op
,
t1
,
t2
)
->
bin
(
term
t1
)
op
(
term
t2
)
|
TUnOp
(
op
,
t
)
->
unary
op
(
term
t
)
...
...
@@ -273,7 +287,7 @@ let rec term_node t =
let
ls
=
get_lsymbol
li
in
let
args
=
List
.
map
(
fun
x
->
snd
(
term
x
))
args
in
t_app
ls
args
|
_
->
|
_
->
Self
.
not_yet_implemented
"term_node Tapp with labels"
end
|
TSizeOf
_
...
...
@@ -447,9 +461,9 @@ let rec logic_decl ~in_axiomatic a _loc (theories,decls) =
Self
.
not_yet_implemented
"Dlemma with labels or vars"
end
|
Daxiomatic
(
name
,
decls'
,
loc
)
->
let
theories
=
add_decls_as_theory
theories
(
Ident
.
id_fresh
global_logic_decls_theory_name
)
decls
let
theories
=
add_decls_as_theory
theories
(
Ident
.
id_fresh
global_logic_decls_theory_name
)
decls
in
let
(
t
,
decls''
)
=
List
.
fold_left
...
...
@@ -483,23 +497,46 @@ let identified_proposition p =
let
program_vars
=
Hashtbl
.
create
257
let
any
_ty
=
Mlw_expr
.
e_const
(
Term
.
ConstInt
(
Term
.
int_const_decimal
"0"
))
let
any
_ty
=
Mlw_expr
.
e_const
(
Number
.
ConstInt
(
Number
.
int_const_dec
"0"
))
let
mk_ref
ty
=
let
pv
=
Mlw_ty
.
create_pvsymbol
(
Ident
.
id_fresh
"a"
)
(
Mlw_ty
.
vty_value
ty
)
in
let
ity
=
Mlw_ty
.
ity_app_fresh
ref_type
[
ty
]
in
let
vta
=
Mlw_ty
.
vty_arrow
[
pv
]
(
Mlw_ty
.
VTvalue
(
Mlw_ty
.
vty_value
ity
))
in
Mlw_expr
.
e_arrow
ref_fun
vta
let
mk_get
ty
=
try
let
vty
=
Mlw_ty
.
vty_value
ty
in
let
r
=
match
vty
.
Mlw_ty
.
vtv_mut
with
|
Some
r
->
r
|
None
->
assert
false
in
let
ity
=
Mlw_ty
.
ity_app
ref_type
[
ty
]
[
r
]
in
let
pv
=
Mlw_ty
.
create_pvsymbol
(
Ident
.
id_fresh
"a"
)
vty
in
let
vta
=
Mlw_ty
.
vty_arrow
[
pv
]
(
Mlw_ty
.
VTvalue
(
Mlw_ty
.
vty_value
ty
))
in
Mlw_expr
.
e_arrow
get_fun
vta
with
e
->
Self
.
fatal
"Exception raised during mk_get@ %a@."
Exn_printer
.
exn_printer
e
let
mk_set
ty
=
let
pv
=
Mlw_ty
.
create_pvsymbol
(
Ident
.
id_fresh
"a"
)
(
Mlw_ty
.
vty_value
ty
)
in
(* let ity = Mlw_ty.ity_app_fresh ref_type [ty] in *)
let
vta
=
Mlw_ty
.
vty_arrow
[
pv
]
(
Mlw_ty
.
VTvalue
(
Mlw_ty
.
vty_value
ty
))
in
Mlw_expr
.
e_arrow
set_fun
vta
let
create_var
v
=
let
id
=
Ident
.
id_fresh
v
.
vname
in
let
ty
=
Mlw_ty
.
vty_value
(
ctype
v
.
vtype
)
in
let
specialize_ref
=
Mlw_dty
.
specialize_psymbol
ref_fun
in
let
vty
=
match
Mlw_dty
.
vty_of_dvty
specialize_ref
with
|
Mlw_ty
.
VTarrow
vty
->
vty
|
Mlw_ty
.
VTvalue
_
->
assert
false
in
let
def
=
Mlw_expr
.
e_app
(
Mlw_expr
.
e_arrow
ref_fun
vty
)
[
any
ty
]
in
let
ty
=
ctype
v
.
vtype
in
let
def
=
Mlw_expr
.
e_app
(
mk_ref
ty
)
[
any
ty
]
in
let
let_defn
=
Mlw_expr
.
create_let_defn
id
def
in
let
vs
=
match
let_defn
.
Mlw_expr
.
let_sym
with
|
Mlw_expr
.
LetV
vs
->
vs
...
...
@@ -508,7 +545,7 @@ let create_var v =
(*
Self.result "create program variable %s (%d)" v.vname v.vid;
*)
Hashtbl
.
add
program_vars
v
.
vid
vs
;
Hashtbl
.
add
program_vars
v
.
vid
(
vs
,
ty
)
;
let_defn
let
get_var
v
=
...
...
@@ -520,7 +557,16 @@ let get_var v =
let
lval
(
host
,
offset
)
=
match
host
,
offset
with
|
Var
v
,
NoOffset
->
Mlw_expr
.
e_value
(
get_var
v
)
|
Var
v
,
NoOffset
->
let
v
,
ty
=
get_var
v
in
begin
try
Mlw_expr
.
e_app
(
mk_get
ty
)
[
Mlw_expr
.
e_value
v
]
with
e
->
Self
.
fatal
"Exception raised during application of !@ %a@."
Exn_printer
.
exn_printer
e
end
|
Var
_
,
(
Field
(
_
,
_
)
|
Index
(
_
,
_
))
->
Self
.
not_yet_implemented
"lval Var"
|
Mem
_
,
_
->
...
...
@@ -552,28 +598,68 @@ let annot a e =
|
APragma
_
->
Self
.
not_yet_implemented
"annot APragma"
let
expr
e
=
let
binop
op
e1
e2
=
match
op
with
|
PlusA
->
Mlw_expr
.
e_lapp
mul_int
[
e1
;
e2
]
Mlw_ty
.
ity_int
|
Mult
->
Mlw_expr
.
e_lapp
mul_int
[
e1
;
e2
]
Mlw_ty
.
ity_int
|
PlusPI
|
IndexPI
|
MinusA
|
MinusPI
|
MinusPP
|
Div
|
Mod
|
Shiftlt
|
Shiftrt
|
Lt
|
Gt
|
Le
|
Ge
|
Eq
|
Ne
|
BAnd
|
BXor
|
BOr
|
LAnd
|
LOr
->
Self
.
not_yet_implemented
"binop"
let
constant
c
=
match
c
with
|
CInt64
(
_t
,_
ikind
,
Some
s
)
->
Number
.
ConstInt
(
Literals
.
integer
s
)
|
CInt64
(
_t
,_
ikind
,
None
)
->
Self
.
not_yet_implemented
"constant CInt64/None"
|
CStr
_
|
CWStr
_
|
CChr
_
|
CReal
(
_
,
_
,
_
)
|
CEnum
_
->
Self
.
not_yet_implemented
"constant"
let
rec
expr
e
=
match
e
.
enode
with
|
Const
_c
->
(* constant c *)
Self
.
not_yet_implemented
"expr Const"
|
Const
c
->
Mlw_expr
.
e_const
(
constant
c
)
|
Lval
lv
->
lval
lv
|
BinOp
(
op
,
e1
,
e2
,
_loc
)
->
binop
op
(
expr
e1
)
(
expr
e2
)
|
SizeOf
_
|
SizeOfE
_
|
SizeOfStr
_
|
AlignOf
_
|
AlignOfE
_
|
UnOp
(
_
,
_
,
_
)
|
BinOp
(
_
,
_
,
_
,
_
)
|
CastE
(
_
,
_
)
|
AddrOf
_
|
StartOf
_
|
Info
(
_
,
_
)
->
Self
.
not_yet_implemented
"expr"
let
assignment
(
lhost
,
offset
)
e
_loc
=
match
lhost
,
offset
with
|
Var
v
,
NoOffset
->
let
v
,
ty
=
get_var
v
in
begin
try
Mlw_expr
.
e_app
(
mk_set
ty
)
[
Mlw_expr
.
e_value
v
;
expr
e
]
with
e
->
Self
.
fatal
"Exception raised during application of :=@ %a@."
Exn_printer
.
exn_printer
e
end
|
Var
_
,
Field
_
->
Self
.
not_yet_implemented
"assignment Var/Field"
|
Var
_
,
Index
_
->
Self
.
not_yet_implemented
"assignment Var/Index"
|
Mem
_
,
_
->
Self
.
not_yet_implemented
"assignment Mem"
let
instr
i
=
match
i
with
|
Set
(
_lv
,_
e
,_
loc
)
->
Self
.
not_yet_implemented
"instr Set"
|
Set
(
lv
,
e
,
loc
)
->
assignment
lv
e
loc
|
Call
(
_
,
_
,
_
,
_
)
->
Self
.
not_yet_implemented
"instr Call"
|
Asm
(
_
,
_
,
_
,
_
,
_
,
_
)
->
...
...
@@ -676,7 +762,7 @@ let fundecl fdec =
let
fun_id
=
fdec
.
svar
in
let
kf
=
Globals
.
Functions
.
get
fun_id
in
Self
.
log
"processing function %a"
Kernel_function
.
pretty
kf
;
let
formals
=
let
formals
=
match
Kernel_function
.
get_formals
kf
with
|
[]
->
[
"_dummy"
,
Mlw_ty
.
ity_unit
]
|
l
->
List
.
map
(
fun
v
->
(
v
.
vname
,
ctype
v
.
vtype
))
l
...
...
@@ -686,8 +772,8 @@ let fundecl fdec =
let
_pre
,_
post
,_
ass
=
extract_simple_contract
contract
in
let
_ret_type
=
ctype
(
Kernel_function
.
get_return_type
kf
)
in
let
args
=
List
.
map
(
fun
(
id
,
ity
)
->
List
.
map
(
fun
(
id
,
ity
)
->
Mlw_ty
.
create_pvsymbol
(
Ident
.
id_fresh
id
)
(
Mlw_ty
.
vty_value
ity
))
formals
in
...
...
@@ -778,15 +864,15 @@ let add_pdecl m d =
try
Mlw_module
.
add_pdecl
~
wp
:
true
m
d
with
Not_found
->
Not_found
->
Self
.
fatal
"add_pdecl %a"
(
Pp
.
print_list
Pp
.
comma
print_id
)
(
Ident
.
Sid
.
elements
d
.
Mlw_decl
.
pd_news
)
(
Ident
.
Sid
.
elements
d
.
Mlw_decl
.
pd_news
)
let
use
m
th
=
let
name
=
th
.
Theory
.
th_name
in
Mlw_module
.
close_namespace
(
Mlw_module
.
use_export_theory
(
Mlw_module
.
open_namespace
m
name
.
Ident
.
id_string
)
(
Mlw_module
.
open_namespace
m
name
.
Ident
.
id_string
)
th
)
true
...
...
@@ -797,12 +883,12 @@ let prog p =
in
Self
.
result
"found %d logic decl(s)"
(
List
.
length
decls
);
let
theories
=
add_decls_as_theory
theories
add_decls_as_theory
theories
(
Ident
.
id_fresh
global_logic_decls_theory_name
)
decls
in
Self
.
result
"made %d theory(ies)"
(
List
.
length
theories
);
let
m
=
Mlw_module
.
create_module
env
(
Ident
.
id_fresh
programs_module_name
)
let
m
=
Mlw_module
.
create_module
env
(
Ident
.
id_fresh
programs_module_name
)
in
let
m
=
use
m
int_theory
in
let
m
=
use
m
real_theory
in
...
...
@@ -811,6 +897,6 @@ let prog p =
Self
.
result
"made %d function(s)"
(
List
.
length
functions
);
let
m
=
Mlw_module
.
close_module
m
in
List
.
rev
(
m
.
Mlw_module
.
mod_theory
::
theories
)
;
with
Decl
.
UnknownIdent
(
s
)
->
Self
.
fatal
"unknown identifier %s"
s
.
Ident
.
id_string
with
e
->
Self
.
fatal
"Exception raised during translation to Why3:@ %a@."
Exn_printer
.
exn_printer
e
src/jessie/literals.mll
View file @
038febb8
...
...
@@ -81,7 +81,7 @@ and floating_point_literal = parse
|
(
rD
+
as
i
)
'.'
(
rD
*
as
f
)
([
'
e'
'
E'
]
([
'
-
'
'
+
'
]
?
rD
+
as
e
))
?
|
(
rD
*
as
i
)
'.'
(
rD
+
as
f
)
([
'
e'
'
E'
]
([
'
-
'
'
+
'
]
?
rD
+
as
e
))
?
)
rFS
eof
{
Term
.
RConstDecimal
(
i
,
f
,
Opt
.
map
remove_leading_plus
e
)
}
{
Number
.
real_const_dec
i
f
(
Opt
.
map
remove_leading_plus
e
)
}
(* hexadecimal *)
|
'
0
'
[
'
x''X'
]
(
(
rH
*
as
i
)
'.'
(
rH
+
as
f
)
...
...
@@ -89,7 +89,7 @@ and floating_point_literal = parse
|
(
rH
+
as
i
)
(
""
as
f
)
)
[
'
p''P'
]
((
'
-
'
rD
+
)
as
e
|
'
+
'
?
(
rD
+
as
e
)
)
rFS
eof
{
Term
.
RConstHexa
(
i
,
f
,
e
)
}
{
Number
.
real_const_hex
i
f
(
Some
e
)
}
|
eof
{
invalid_arg
"floating_point_literal: empty string"
}
|
_
as
c
{
invalid_arg
(
"floating_point_literal: character '"
^
...
...
src/jessie/register.ml
View file @
038febb8
...
...
@@ -63,7 +63,8 @@ let process () =
"Z32"
,
"Z3,3.2"
;
"C24"
,
"CVC3,2.4.1"
;
"C22"
,
"CVC3,2.2"
;
"AlE"
,
"Alt-Ergo,0.94"
;
"A95"
,
"Alt-Ergo,0.95"
;
"A94"
,
"Alt-Ergo,0.94"
;
]
in
let
theories
=
ACSLtoWhy3
.
prog
prog
in
...
...
src/jessie/tests/basic/oracle/axiomatic.res.oracle
View file @
038febb8
...
...
@@ -10,7 +10,7 @@
[jessie3] made 0 function(s)
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations
(* use BuiltIn *)
(* use
why3.
BuiltIn *)
(* use int.Int *)
...
...
@@ -20,11 +20,11 @@
lemma l1 : forall x:int. f1 x >= 1
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[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] running theory 1:
[jessie3] theory BagInt
(* use BuiltIn *)
(* use
why3.
BuiltIn *)
(* use int.Int *)
...
...
@@ -54,11 +54,11 @@
lemma l2 : f1 1 = 2
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[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] running theory 1:
[jessie3] theory Global_logic_declarations1
(* use BuiltIn *)
(* use
why3.
BuiltIn *)
(* use int.Int *)
...
...
@@ -68,17 +68,17 @@
lemma union_comm : forall b1:bag, b2:bag. bag_union b1 b2 = bag_union b2 b1
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Task 1: Unknown, Valid, Valid, Valid, Valid
[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] running theory 1:
[jessie3] theory C_Functions
(* use BuiltIn *)
(* use
why3.
BuiltIn *)
(* use Bool *)
(* use
why3.
Bool *)
(* use Unit *)
(* use
why3.
Unit *)
(* use Prelude *)
(* use
why3.
Prelude *)
(* use int.Int *)
...
...
@@ -86,4 +86,4 @@
(* use Global_logic_declarations1 *)
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Alt-Ergo 0.94,
Alt-Ergo 0.95,
CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
src/jessie/tests/basic/oracle/constants.res.oracle
View file @
038febb8
...
...
@@ -6,7 +6,7 @@
[jessie3] made 0 function(s)
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations
(* use BuiltIn *)
(* use
why3.
BuiltIn *)
(* use int.Int *)
...
...
@@ -22,21 +22,21 @@
lemma test4 : 0x1.1p4 = 17.0
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[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] 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] running theory 1:
[jessie3] theory C_Functions
(* use BuiltIn *)
(* use
why3.
BuiltIn *)
(* use Bool *)
(* use
why3.
Bool *)
(* use Unit *)
(* use
why3.
Unit *)
(* use Prelude *)
(* use
why3.
Prelude *)
(* use int.Int *)
...
...
@@ -44,4 +44,4 @@
(* use Global_logic_declarations *)
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Alt-Ergo 0.94,
Alt-Ergo 0.95,
CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
src/jessie/tests/basic/oracle/forty-two.res.oracle
View file @
038febb8
...
...
@@ -3,23 +3,6 @@
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] processing function f
[jessie3] processing function g
[kernel] The full backtrace is:
Raised at file "src/whyml/mlw_ty.ml", line 886, characters 26-29
Called from file "ACSLtoWhy3.ml", line 496, characters 9-50
Called from file "list.ml", line 57, characters 20-23
Called from file "ACSLtoWhy3.ml", line 692, characters 4-55
Called from file "ACSLtoWhy3.ml", line 727, characters 14-26
Called from file "list.ml", line 86, characters 24-34
Called from file "ACSLtoWhy3.ml", line 792, characters 6-48
Called from file "register.ml", line 69, characters 17-37
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 38, characters 4-20
Called from file "src/kernel/cmdline.ml", line 720, characters 2-9
Called from file "src/kernel/cmdline.ml", line 197, characters 4-8
Unexpected error (Invalid_argument("Mlw.vty_arrow")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Oxygen-20120901.
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
[kernel] Plug-in jessie3 aborted: unimplemented feature.
You may send a feature request at http://bts.frama-c.com with:
'[Plug-in jessie3] instr Set'.
src/jessie/tests/basic/oracle/generic.res.oracle
View file @
038febb8
...
...
@@ -9,7 +9,7 @@
[jessie3] made 0 function(s)
[jessie3] running theory 1:
[jessie3] theory Bag
(* use BuiltIn *)
(* use
why3.
BuiltIn *)
(* use int.Int *)
...
...
@@ -23,16 +23,16 @@
function bag_union (bag 'x) (bag 'x) : bag 'x
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[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 BuiltIn *)
(* use
why3.
BuiltIn *)
(* use Bool *)
(* use
why3.
Bool *)
(* use Unit *)
(* use
why3.
Unit *)
(* use Prelude *)
(* use
why3.
Prelude *)
(* use int.Int *)
...
...
@@ -40,4 +40,4 @@
(* use Bag *)
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Alt-Ergo 0.94,
Alt-Ergo 0.95,
CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
src/jessie/tests/basic/oracle/incr.res.oracle
View file @
038febb8
...
...
@@ -2,23 +2,6 @@
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] processing function f
[kernel] The full backtrace is:
Raised at file "src/whyml/mlw_ty.ml", line 886, characters 26-29
Called from file "ACSLtoWhy3.ml", line 496, characters 9-50
Called from file "list.ml", line 57, characters 20-23
Called from file "ACSLtoWhy3.ml", line 692, characters 4-55
Called from file "ACSLtoWhy3.ml", line 727, characters 14-26
Called from file "list.ml", line 86, characters 24-34
Called from file "ACSLtoWhy3.ml", line 792, characters 6-48
Called from file "register.ml", line 69, characters 17-37
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 38, characters 4-20
Called from file "src/kernel/cmdline.ml", line 720, characters 2-9
Called from file "src/kernel/cmdline.ml", line 197, characters 4-8
Unexpected error (Invalid_argument("Mlw.vty_arrow")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Oxygen-20120901.
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
[kernel] Plug-in jessie3 aborted: unimplemented feature.
You may send a feature request at http://bts.frama-c.com with:
'[Plug-in jessie3] instr Set'.
src/jessie/tests/basic/oracle/isqrt.res.oracle
View file @
038febb8
...
...
@@ -3,23 +3,6 @@
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] creating logic symbol 739 (sqr)
[jessie3] processing function isqrt
[kernel] The full backtrace is:
Raised at file "src/whyml/mlw_ty.ml", line 886, characters 26-29
Called from file "ACSLtoWhy3.ml", line 496, characters 9-50
Called from file "list.ml", line 57, characters 20-23
Called from file "ACSLtoWhy3.ml", line 692, characters 4-55
Called from file "ACSLtoWhy3.ml", line 727, characters 14-26
Called from file "list.ml", line 86, characters 24-34
Called from file "ACSLtoWhy3.ml", line 792, characters 6-48
Called from file "register.ml", line 69, characters 17-37
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 38, characters 4-20
Called from file "src/kernel/cmdline.ml", line 720, characters 2-9
Called from file "src/kernel/cmdline.ml", line 197, characters 4-8
Unexpected error (Invalid_argument("Mlw.vty_arrow")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Oxygen-20120901.
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
[kernel] Plug-in jessie3 aborted: unimplemented feature.
You may send a feature request at http://bts.frama-c.com with:
'[Plug-in jessie3] stmt Loop'.
src/jessie/tests/basic/oracle/lemma.res.oracle
View file @
038febb8
...
...
@@ -6,7 +6,7 @@
[jessie3] made 0 function(s)
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations
(* use BuiltIn *)
(* use
why3.
BuiltIn *)
(* use int.Int *)
...
...
@@ -26,23 +26,23 @@
lemma test4r : forall x:real, y:real. (x - y) = (- (y - x))
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[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] 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] running theory 1:
[jessie3] theory C_Functions
(* use BuiltIn *)
(* use
why3.
BuiltIn *)
(* use Bool *)
(* use
why3.
Bool *)
(* use Unit *)
(* use
why3.
Unit *)
(* use Prelude *)
(* use
why3.
Prelude *)
(* use int.Int *)
...
...
@@ -50,4 +50,4 @@
(* use Global_logic_declarations *)
end
[jessie3] Alt-Ergo 0.94, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
[jessie3] Alt-Ergo 0.94,
Alt-Ergo 0.95,
CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.2
Write
Preview