Commit 2b74c319 authored by MARCHE Claude's avatar MARCHE Claude

Jessie3: support for "\old" (need to export Mlw_wp.t_at_old)

parent 1755d5a3
......@@ -207,3 +207,4 @@ pvsbin/
/src/jessie/literals.ml
/src/jessie/ptests_local_config.ml
/src/jessie/tests/basic/result/*.log
/src/jessie/tests/demo/result/*.log
......@@ -422,5 +422,7 @@ let () =
(*
ocaml -I ../../lib/why3 unix.cma nums.cma str.cma dynlink.cma ../../lib/why3/why3.cma use_api.ml
Local Variables:
compile-command: "ocaml -I ../../lib/why3 unix.cma nums.cma str.cma dynlink.cma ../../lib/why3/why3.cma use_api.ml"
End:
*)
......@@ -286,7 +286,9 @@ let rec ty denv env impl { e_loc = loc; e_node = n } = match n with
| Enot _ | Eequ _ | Edob _ | Enum _ -> error ~loc TypeExpected
let t_int_const s = t_const (Number.ConstInt (Number.int_const_dec s))
(* unused
let t_real_const r = t_const (Number.ConstReal r)
*)
let rec term denv env impl { e_loc = loc; e_node = n } = match n with
| Eapp (aw,al) ->
......
......@@ -133,15 +133,22 @@ let ctype ty =
match ty with
| TVoid _attr -> Mlw_ty.ity_unit
| TInt (_, _) -> Mlw_ty.ity_pur Ty.ts_int []
| TFloat (_, _)
| TPtr (_, _)
| TArray (_, _, _, _)
| TFun (_, _, _, _)
| TNamed (_, _)
| TComp (_, _, _)
| TEnum (_, _)
| TBuiltin_va_list _
-> Self.not_yet_implemented "ctype"
| TFloat (_, _) ->
Self.not_yet_implemented "ctype TFloat"
| TPtr (_, _) ->
Self.not_yet_implemented "ctype TPtr"
| TArray (_, _, _, _) ->
Self.not_yet_implemented "ctype TArray"
| TFun (_, _, _, _) ->
Self.not_yet_implemented "ctype TFun"
| TNamed (_, _) ->
Self.not_yet_implemented "ctype TNamed"
| TComp (_, _, _) ->
Self.not_yet_implemented "ctype TComp"
| TEnum (_, _) ->
Self.not_yet_implemented "ctype TEnum"
| TBuiltin_va_list _ ->
Self.not_yet_implemented "ctype TBuiltin_va_list"
let logic_types = Hashtbl.create 257
......@@ -285,7 +292,7 @@ let get_lvar lv =
let program_vars = Hashtbl.create 257
let create_var v =
let create_var_full v =
let id = Ident.id_fresh v.vname in
let ty = ctype v.vtype in
let def = Mlw_expr.e_app (mk_ref ty) [any ty] in
......@@ -298,7 +305,9 @@ let create_var v =
Self.result "create program variable %s (%d)" v.vname v.vid;
*)
Hashtbl.add program_vars v.vid (vs,true,ty);
let_defn
let_defn,vs
let create_var v = fst (create_var_full v)
let get_var v =
try
......@@ -328,19 +337,29 @@ let get_lsymbol li =
let result_vsymbol =
ref (Term.create_vsymbol (Ident.id_fresh "result") unit_type)
let tlval (host,offset) =
type label = Here | Old | At of string
let tlval ~label (host,offset) =
match host,offset with
| TResult _, TNoOffset -> Term.t_var !result_vsymbol
| TVar lv, TNoOffset ->
begin
match lv.lv_origin with
| None -> Term.t_var (get_lvar lv)
| Some v ->
let (v,is_mutable,_ty) = get_var v in
if is_mutable then
t_app get_logic_fun [Term.t_var v.Mlw_ty.pv_vs]
else
Term.t_var v.Mlw_ty.pv_vs
let t =
match lv.lv_origin with
| None -> Term.t_var (get_lvar lv)
| Some v ->
let (v,is_mutable,_ty) = get_var v in
if is_mutable then
t_app get_logic_fun [Term.t_var v.Mlw_ty.pv_vs]
else
Term.t_var v.Mlw_ty.pv_vs
in
match label with
| Here -> t
| Old -> Mlw_wp.t_at_old t
| At _lab ->
(* t_app Mlw_wp.fs_at [t; ??? lab] *)
Self.not_yet_implemented "tlval TVar/At"
end
| TVar _, (TField (_, _)|TModel (_, _)|TIndex (_, _)) ->
Self.not_yet_implemented "tlval TVar"
......@@ -349,12 +368,10 @@ let tlval (host,offset) =
| TMem _, _ ->
Self.not_yet_implemented "tlval Mem"
type label = Here | Old | At of string
let rec term_node ~label t =
match t with
| TConst cst -> Term.t_const (logic_constant cst)
| TLval lv -> tlval lv
| TLval lv -> tlval ~label lv
| TBinOp (op, t1, t2) -> bin (term ~label t1) op (term ~label t2)
| TUnOp (op, t) -> unary op (term ~label t)
| TCastE (_, _) -> Self.not_yet_implemented "term_node TCastE"
......@@ -944,11 +961,19 @@ let global (theories,lemmas,functions) g =
{ acc with AST.prog_vars =
(intern_string vi.vname, g)::acc.AST.prog_vars }
*)
Self.not_yet_implemented "WARNING: Variable %s not translated" vi.vname
let _,pv = create_var_full vi in
let sym = Mlw_expr.LetV pv in
(theories,lemmas,(Mlw_decl.create_val_decl sym)::functions)
| GVarDecl(_funspec,vi,_location) ->
Self.error "WARNING: Variable %s not translated" vi.vname;
(theories,lemmas,functions)
begin match vi.vname with
| "Frama_C_bzero" | "Frama_C_copy_block" ->
(theories,lemmas,functions)
| _ ->
let _,pv = create_var_full vi in
let sym = Mlw_expr.LetV pv in
(theories,lemmas,(Mlw_decl.create_val_decl sym)::functions)
end
| GAnnot (a, loc) ->
let (t,l) = logic_decl ~in_axiomatic:false a loc (theories,lemmas) in
(t,l,functions)
......
......@@ -13,7 +13,7 @@ PLUGIN_BFLAGS:= -I $(WHYLIB)
PLUGIN_OFLAGS:= -I $(WHYLIB)
PLUGIN_LINK_BFLAGS:= -I $(WHYLIB)
PLUGIN_LINK_OFLAGS:= -I $(WHYLIB)
PLUGIN_TESTS_DIRS := basic
PLUGIN_TESTS_DIRS := basic demo
OCAMLLEX = @OCAMLLEX@
......@@ -23,5 +23,5 @@ literals.ml: literals.mll
include $(FRAMAC_SHARE)/Makefile.dynamic
tests::
grep Status tests/basic/result/*
grep 'Task\|Ergo' tests/basic/result/*.res.log tests/demo/result/*.res.log
......@@ -9,7 +9,6 @@ int f(int x) {
return x+1;
}
#if 0
int g;
......@@ -19,7 +18,6 @@ void h(int x) {
g += x;
}
#endif
/*
Local Variables:
......
[kernel] preprocessing with "gcc -C -E -I. tests/basic/axiomatic.c"
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] creating logic symbol 739 (f1)
[jessie3] creating logic symbol 743 (occ)
[jessie3] creating logic symbol 748 (singleton)
......
[kernel] preprocessing with "gcc -C -E -I. tests/basic/constants.c"
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] found 5 logic decl(s)
[jessie3] made 1 theory(ies)
[jessie3] made 0 function(s)
......
[kernel] preprocessing with "gcc -C -E -I. tests/basic/forty-two.c"
[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
[jessie3] processing function g
[jessie3] found 0 logic decl(s)
......
[kernel] preprocessing with "gcc -C -E -I. tests/basic/generic.c"
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] creating logic symbol 740 (occ)
[jessie3] creating logic symbol 742 (singleton)
[jessie3] creating logic symbol 745 (bag_union)
......
[kernel] preprocessing with "gcc -C -E -I. tests/basic/incr.c"
[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
[jessie3] processing function h
[jessie3] found 0 logic decl(s)
[jessie3] made 0 theory(ies)
[jessie3] made 1 function(s)
[jessie3] made 3 function(s)
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
......@@ -24,6 +23,10 @@
goal WP_parameter_f :
forall x:int.
forall us_retres:int. us_retres = (x + 1) -> us_retres = (x + 1)
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
[kernel] preprocessing with "gcc -C -E -I. tests/basic/lemma.c"
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] found 7 logic decl(s)
[jessie3] made 1 theory(ies)
[jessie3] made 0 function(s)
......
/* run.config
OPT: -journal-disable -jessie3
*/
//@ lemma mean: \forall integer x, y; x <= y ==> x <= (x+y)/2 <= y;
/*@ predicate sorted{L}(long *t, integer a, integer b) =
@ \forall integer i,j; a <= i <= j <= b ==> t[i] <= t[j];
@*/
/*@ requires n >= 0 && \valid(t+(0..n-1));
@ requires sorted(t,0,n-1);
@ ensures -1 <= \result < n;
@ ensures \result >= 0 ==> t[\result] == v;
@ ensures \result == -1 ==>
@ \forall integer k; 0 <= k < n ==> t[k] != v;
@*/
int binary_search(long t[], int n, long v) {
int l = 0, u = n-1;
/*@ loop invariant 0 <= l && u <= n-1;
@ loop invariant
@ \forall integer k; 0 <= k < n && t[k] == v ==> l <= k <= u;
@ loop variant u-l;
@*/
while (l <= u ) {
int m = (l + u) / 2;
//@ assert l <= m <= u;
if (t[m] < v) l = m + 1;
else if (t[m] > v) u = m - 1;
else return m;
}
return -1;
}
/*
Local Variables:
compile-command: "frama-c -add-path ../.. -jessie3 binary_search.c"
End:
*/
[kernel] preprocessing with "gcc -C -E -I. tests/demo/binary_search.c"
[kernel] Plug-in jessie3 aborted: unimplemented feature.
You may send a feature request at http://bts.frama-c.com with:
'[Plug-in jessie3] bin'.
[kernel] preprocessing with "gcc -C -E -I. tests/basic/isqrt.c"
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[kernel] preprocessing with "gcc -C -E -I. tests/demo/isqrt.c"
[jessie3] creating logic symbol 739 (sqr)
[jessie3] processing function isqrt
[jessie3] found 1 logic decl(s)
......
this directory collects the results of tests
......@@ -138,7 +138,7 @@ let run_normal dir filter_provers =
let print_float_list =
Pp.print_list_delim ~start:Pp.lsquare ~stop:Pp.rsquare ~sep:Pp.semi Pp.float
let rec grab_valid_time provers_time provers pa =
let grab_valid_time provers_time provers pa =
let prover = pa.Session.proof_prover in
if Whyconf.Sprover.mem prover provers then
match pa.Session.proof_state with
......
......@@ -248,7 +248,7 @@ let rec ask_yn () =
| "n" -> false
| _ -> ask_yn ()
let rec ask_yn_nonblock ~callback =
let ask_yn_nonblock ~callback =
let b = Buffer.create 3 in
let s = String.create 1 in
Format.printf "(y/n)@.";
......
......@@ -11,7 +11,6 @@
open Why3
open Why3session_lib
open Whyconf
open Session
open Format
......
......@@ -41,7 +41,9 @@ exception UnboundTheory of qualid
exception UnboundType of string list
*)
exception UnboundTypeVar of string
(* unused
exception UnboundSymbol of qualid
*)
let error = Loc.error
let errorm = Loc.errorm
......@@ -76,8 +78,10 @@ let () = Exn_printer.register (fun fmt e -> match e with
*)
| UnboundTypeVar s ->
Format.fprintf fmt "Unbound type variable '%s" s
(* unused
| UnboundSymbol q ->
Format.fprintf fmt "Unbound symbol '%a'" print_qualid q
*)
| _ -> raise e)
(* TODO: let type_only = Debug.test_flag Typing.debug_type_only in *)
......
......@@ -21,7 +21,10 @@ val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty
val fs_at : Term.lsymbol
(* unused
val fs_old : Term.lsymbol
*)
val t_at_old : Term.term -> Term.term
val th_mark_at : Theory.theory
val th_mark_old : Theory.theory
......
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