Commit 664e954f authored by MARCHE Claude's avatar MARCHE Claude

jessie3: logic type decl

parent 4a12677c
...@@ -29,6 +29,7 @@ why3.conf ...@@ -29,6 +29,7 @@ why3.conf
/distrib /distrib
/why3regtests.err /why3regtests.err
/why3regtests.out /why3regtests.out
/META
# /lib/why3/ # /lib/why3/
/lib/why3/META /lib/why3/META
...@@ -100,6 +101,7 @@ why3.conf ...@@ -100,6 +101,7 @@ why3.conf
/doc/manual.gls /doc/manual.gls
/doc/manual.ist /doc/manual.ist
/doc/manual.out /doc/manual.out
/doc/manual.image.out
/doc/*.haux /doc/*.haux
/doc/*.pdf /doc/*.pdf
/doc/html/ /doc/html/
...@@ -200,4 +202,5 @@ pvsbin/ ...@@ -200,4 +202,5 @@ pvsbin/
/src/jessie/autom4te.cache/ /src/jessie/autom4te.cache/
/src/jessie/config.log /src/jessie/config.log
/src/jessie/config.status /src/jessie/config.status
/src/jessie/Makefile
/src/jessie/ptests_local_config.ml /src/jessie/ptests_local_config.ml
...@@ -249,7 +249,20 @@ let add_decls_as_theory theories id decls = ...@@ -249,7 +249,20 @@ let add_decls_as_theory theories id decls =
let rec annot ~in_axiomatic a _loc (theories,decls) = let rec annot ~in_axiomatic a _loc (theories,decls) =
match a with match a with
| Dtype (_, _) -> Self.not_yet_implemented "annot Dtype" | Dtype (lt, loc) ->
let targs =
List.map (fun s -> Ty.create_tvsymbol (Ident.id_fresh s)) lt.lt_params
in
let tdef = match lt.lt_def with
| None -> None
| Some _ -> Self.not_yet_implemented "annot Dtype non abstract"
in
let ts =
Ty.create_tysymbol
(Ident.id_user lt.lt_name (Loc.extract loc)) targs tdef
in
let d = Decl.create_ty_decl ts in
(theories,d::decls)
| Dfun_or_pred (_, _) -> Self.not_yet_implemented "annot Dfun_or_pred" | Dfun_or_pred (_, _) -> Self.not_yet_implemented "annot Dfun_or_pred"
| Dlemma(name,is_axiom,labels,vars,p,loc) -> | Dlemma(name,is_axiom,labels,vars,p,loc) ->
begin begin
......
...@@ -5,9 +5,9 @@ ...@@ -5,9 +5,9 @@
/*@ axiomatic Bag { /*@ axiomatic Bag {
@ type bag; @ type bag;
@ logic bag my_union(bag b1,bag b2); @ // logic bag my_union(bag b1,bag b2);
@ axiom union_comm: \forall bag b1,b2; @ // axiom union_comm: \forall bag b1,b2;
@ my_union(b1,b2) == my_union(b2,b1); @ // my_union(b1,b2) == my_union(b2,b1);
@ } @ }
@*/ @*/
......
[kernel] preprocessing with "gcc -C -E -I. tests/basic/axiomatic.c" [kernel] preprocessing with "gcc -C -E -I. tests/basic/axiomatic.c"
[kernel] Plug-in jessie3 aborted: unimplemented feature. [jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
You may send a feature request at http://bts.frama-c.com with: [jessie3] user error: WARNING: Variable Frama_C_bzero not translated
'[Plug-in jessie3] annot Dtype'. [jessie3] found 0 decls
[jessie3] made 1 theories
[jessie3] running theory 1
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