Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit bdff7246 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Merge branch 'after-release'

parents 52dd5bdc ef5b6175
......@@ -257,12 +257,12 @@ install-all: install install-lib
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli
PLUG_PARSER = genequlin
PLUG_PARSER = genequlin dimacs
PLUG_PRINTER =
PLUG_TRANSFORM =
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
PLUGINS = genequlin tptp
PLUGINS = genequlin dimacs tptp
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
......@@ -1274,7 +1274,7 @@ endif
# API DOC
##########
.PHONY: apidoc
.PHONY: apidoc apidot
MODULESTODOC = \
util/util util/opt util/lists util/strings \
......@@ -1289,15 +1289,31 @@ MODULESTODOC = \
FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC)))
apidoc: $(FILESTODOC)
doc/apidoc:
mkdir -p doc/apidoc
apidoc: doc/apidoc $(FILESTODOC)
$(OCAMLDOC) -d doc/apidoc -html -t "Why3 API documentation" \
-keep-code $(INCLUDES) \
$(LIBINCLUDES) -I lib/why3 $(FILESTODOC)
# could we include also the dependency graph ?
# $(OCAMLDOC) -o doc/apidoc/dg.dot -dot $(INCLUDES) \
# $(LIBINCLUDES) -I lib/why3 $(FILESTODOC)
# could we include also the dependency graph ? -- someone
# At least we can give a way to create it -- francois
apidot: doc/apidoc/dg.svg doc/apidoc/dg.png
#The sed remove configuration for dot that gives bad result
doc/apidoc/dg.dot: doc/apidoc $(FILESTODOC)
$(OCAMLDOC) -o doc/apidoc/dg.dot.tmp -dot $(INCLUDES) \
$(LIBINCLUDES) -I lib/why3 $(FILESTODOC)
sed -e "s/ \(size\|ratio\|rotate\|fontsize\).*$$//" doc/apidoc/dg.dot.tmp > doc/apidoc/dg.dot
rm -f doc/apidoc/dg.dot.tmp
doc/apidoc/dg.svg: doc/apidoc/dg.dot
dot -T svg $< > $@
doc/apidoc/dg.png: doc/apidoc/dg.dot
dot -T png $< > $@
# what is this ? api doc is in why3.lri.fr/api instead...
# install_apidoc: apidoc
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2013 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
{
open Why3
open Stdlib
type vars = Term.term array
let get_indice i =
if i > 0 then (i-1)*2
else if i < 0 then (-i-1)*2+1
else assert false
let init_vars th_uc nb_var =
let a = Array.create (nb_var*2) Term.t_true in
let th = ref th_uc in
for i = nb_var downto -nb_var do
if i <> 0 then
if i > 0 then
let id = Ident.id_fresh (Printf.sprintf "x%i" i) in
let ls = Term.create_psymbol id [] in
th := Theory.add_param_decl !th ls;
a.(get_indice i) <- (Term.ps_app ls [])
else if i < 0 then
a.(get_indice i) <- Term.t_not a.(get_indice (-i))
done;
!th,a
let get_lit vars i =
let i = int_of_string i in
vars.(get_indice i)
exception SyntaxError of string
let syntax_error s = raise (SyntaxError s)
let () = Exn_printer.register (fun fmt e -> match e with
| SyntaxError s -> Format.pp_print_string fmt s
| _ -> raise e)
}
let newline = '\n'
let space = [' ' '\t' '\r']+
let digit = ['0'-'9']
let sign = '-' | '+'
let integer = sign? digit+
rule find_header = parse
| newline { Lexing.new_line lexbuf; find_header lexbuf }
| space { find_header lexbuf }
| 'p'
space+ "cnf"
space+ (digit+ as nb_var)
space+ (digit+ as nb_cls) { int_of_string nb_var,
int_of_string nb_cls }
| 'c' [^'\n']* '\n' { Lexing.new_line lexbuf; find_header lexbuf }
| _
{ syntax_error "Can't find header" }
and clause vars acc = parse
| newline { Lexing.new_line lexbuf; clause vars acc lexbuf }
| space { clause vars acc lexbuf }
| '0' { List.rev acc }
| integer as i { clause vars ((get_lit vars i)::acc) lexbuf }
| _ { syntax_error "Bad clause" }
and file th_uc vars n = parse
| newline { Lexing.new_line lexbuf; file th_uc vars n lexbuf }
| space { file th_uc vars n lexbuf }
| '0' { file th_uc vars n lexbuf }
| integer as i { let l = clause vars [get_lit vars i] lexbuf in
let t = List.fold_left (fun acc t ->
Term.t_or acc t
) Term.t_false l in
let pr = Decl.create_prsymbol
(Ident.id_fresh ("Cl"^(string_of_int n))) in
let th_uc = Theory.add_prop_decl th_uc Decl.Paxiom pr t in
file th_uc vars (n+1) lexbuf
}
| 'c' [^'\n']* ('\n' | eof) { Lexing.new_line lexbuf;
file th_uc vars n lexbuf }
| eof { th_uc }
| _ { syntax_error "Bad clauses" }
{
let parse th_uc filename cin =
let lb = Lexing.from_channel cin in
Loc.set_file filename lb;
Loc.with_location (fun lexbuf ->
let nb_vars, _ = find_header lexbuf in
let th_uc, vars = init_vars th_uc nb_vars in
file th_uc vars 0 lexbuf) lb
let parse _env _path filename cin =
let th_uc = Theory.create_theory (Ident.id_fresh "Cnf") in
let th_uc = parse th_uc filename cin in
let pr = Decl.create_prsymbol (Ident.id_fresh "false") in
let th_uc = Theory.add_prop_decl th_uc Decl.Pgoal pr Term.t_false in
(), Mstr.singleton "Cnf" (Theory.close_theory th_uc)
let library_of_env = Env.register_format "Dimacs" ["cnf"] parse
~desc:"@[<hov>Parser for dimacs format.@]"
}
(*
Local Variables:
compile-command: "unset LANG; make -C ../.."
End:
*)
......@@ -238,16 +238,10 @@ and comment_line = parse
{
let with_location f lb =
if Debug.test_flag Debug.stack_trace then f lb else
try f lb with
| Loc.Located _ as e -> raise e
| e -> raise (Loc.Located (loc lb, e))
let read_channel env path file c =
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let ast = with_location (tptp_file token) lb in
let ast = Loc.with_location (tptp_file token) lb in
(), Tptp_typing.typecheck env path ast
let _library_of_env = Env.register_format "tptp" ["p";"ax"] read_channel
......
......@@ -107,10 +107,6 @@ rule token = parse
{ raise (IllegalCharacter c) }
{
let loc lb = Loc.extract (lexeme_start_p lb, lexeme_end_p lb)
let with_location f lb =
try f lb with e -> raise (Loc.Located (loc lb, e))
let parse_file_gen parse input_lexbuf lexbuf =
let s = Stack.create () in
......@@ -130,7 +126,7 @@ rule token = parse
| _ -> tok in
let lex_dumb = Lexing.from_function (fun _ _ -> assert false) in
Loc.transfer_loc lexbuf lex_dumb;
with_location (parse multifile) lex_dumb
Loc.with_location (parse multifile) lex_dumb
let parse_file = parse_file_gen Driver_parser.file
let parse_file_extract = parse_file_gen Driver_parser.file_extract
......
......@@ -30,5 +30,3 @@ val comment : Lexing.lexbuf -> unit
val string : Lexing.lexbuf -> string
val remove_leading_plus : string -> string
val with_location : (Lexing.lexbuf -> 'a) -> Lexing.lexbuf -> 'a
......@@ -302,20 +302,15 @@ and string = parse
{ Buffer.add_char string_buf c; string lexbuf }
{
let with_location f lb =
if Debug.test_flag Debug.stack_trace then f lb else
try f lb with
| Loc.Located _ as e -> raise e
| e -> raise (Loc.Located (loc lb, e))
let parse_logic_file env path lb =
open_file token (Lexing.from_string "") (Typing.open_file env path);
with_location (logic_file token) lb;
Loc.with_location (logic_file token) lb;
Typing.close_file ()
let parse_program_file inc lb =
open_file token (Lexing.from_string "") inc;
with_location (program_file token) lb
Loc.with_location (program_file token) lb
let token_counter lb =
let rec loop in_annot a p =
......
......@@ -1081,9 +1081,9 @@ new_pdecl:
;
pdecl:
| LET ghost lident_rich labels fun_defn
| LET top_ghost lident_rich labels fun_defn
{ Dlet (add_lab $3 $4, $2, $5) }
| LET ghost lident_rich labels EQUAL fun_expr
| LET top_ghost lident_rich labels EQUAL fun_expr
{ Dlet (add_lab $3 $4, $2, $6) }
| LET REC list1_rec_defn
{ Dletrec $3 }
......@@ -1131,7 +1131,7 @@ list1_rec_defn:
;
rec_defn:
| ghost lident_rich labels list1_binder opt_cast spec EQUAL spec expr
| top_ghost lident_rich labels list1_binder opt_cast spec EQUAL spec expr
{ floc (), add_lab $2 $3, $1, $4, (cast_body $5 $9, spec_union $6 $8) }
;
......@@ -1455,6 +1455,12 @@ ghost:
| GHOST { true }
;
top_ghost:
| /* epsilon */ { Gnone }
| GHOST { Gghost }
| LEMMA { Glemma }
;
/*
Local Variables:
compile-command: "unset LANG; make -C ../.."
......
......@@ -46,6 +46,7 @@ type pty =
| PPTtuple of pty list
type ghost = bool
type top_ghost = Gnone | Gghost | Glemma
type binder = loc * ident option * ghost * pty option
type param = loc * ident option * ghost * pty
......@@ -242,12 +243,12 @@ and expr_desc =
| Eabstract of triple
| Enamed of label * expr
and letrec = loc * ident * ghost * binder list * triple
and letrec = loc * ident * top_ghost * binder list * triple
and triple = expr * spec
type pdecl =
| Dlet of ident * ghost * expr
| Dlet of ident * top_ghost * expr
| Dletrec of letrec list
| Dparam of ident * ghost * type_v
| Dexn of ident * pty
......
......@@ -131,3 +131,10 @@ let () = Exn_printer.register
| _ ->
raise exn)
let loc lb = extract (Lexing.lexeme_start_p lb, Lexing.lexeme_end_p lb)
let with_location f lb =
if Debug.test_flag Debug.stack_trace then f lb else
try f lb with
| Located _ as e -> raise e
| e -> raise (Located (loc lb, e))
......@@ -69,3 +69,5 @@ val error: ?loc:position -> exn -> 'a
exception Message of string
val errorm: ?loc:position -> ('a, Format.formatter, unit, 'b) format4 -> 'a
val with_location: (Lexing.lexbuf -> 'a) -> (Lexing.lexbuf -> 'a)
......@@ -327,19 +327,14 @@ let pdecl_ns uc d = match d.pd_node with
| PDrec fdl -> List.fold_left add_rec uc fdl
| PDexn xs -> add_exn uc xs
(* FIXME: move the choice to Mlw_wp and make it dynamic, not start-time *)
let if_fast_wp f1 f2 x = if Debug.test_flag Mlw_wp.fast_wp then f1 x else f2 x
let wp_val = if_fast_wp Mlw_wp.fast_wp_val Mlw_wp.wp_val
let wp_let = if_fast_wp Mlw_wp.fast_wp_let Mlw_wp.wp_let
let wp_rec = if_fast_wp Mlw_wp.fast_wp_rec Mlw_wp.wp_rec
let pdecl_vc env km th d = match d.pd_node with
let pdecl_vc ~wp env km th d = match d.pd_node with
| PDtype _ | PDdata _ | PDexn _ -> th
| PDval lv -> wp_val env km th lv
| PDlet ld -> wp_let env km th ld
| PDrec rd -> wp_rec env km th rd
| PDval lv -> Mlw_wp.wp_val ~wp env km th lv
| PDlet ld -> Mlw_wp.wp_let ~wp env km th ld
| PDrec rd -> Mlw_wp.wp_rec ~wp env km th rd
let pdecl_vc uc d = add_to_theory (pdecl_vc uc.muc_env uc.muc_known) uc d
let pdecl_vc ~wp uc d =
add_to_theory (pdecl_vc ~wp uc.muc_env uc.muc_known) uc d
let pure_data_decl tdl =
let proj pj = Opt.map (fun pls -> pls.pl_ls) pj in
......@@ -359,7 +354,7 @@ let add_pdecl ~wp uc d =
muc_local = Sid.union uc.muc_local d.pd_news }
in
let uc = pdecl_ns uc d in
let uc = if wp then pdecl_vc uc d else uc in
let uc = pdecl_vc ~wp uc d in
let uc = add_to_theory pdecl_pure uc d in
uc
......
......@@ -579,6 +579,15 @@ let eff_is_empty e =
(* eff_compar is not a side effect *)
not e.eff_diverg
let eff_is_read_only e =
Sreg.is_empty e.eff_writes &&
Sexn.is_empty e.eff_raises &&
Sreg.is_empty e.eff_ghostw &&
Sexn.is_empty e.eff_ghostx &&
Mreg.is_empty e.eff_resets &&
(* eff_compar is not a side effect *)
not e.eff_diverg
let eff_equal e1 e2 =
Sreg.equal e1.eff_reads e2.eff_reads &&
Sreg.equal e1.eff_writes e2.eff_writes &&
......
......@@ -237,6 +237,7 @@ val eff_full_inst : ity_subst -> effect -> effect
val eff_filter : varset -> effect -> effect
val eff_is_empty : effect -> bool
val eff_is_read_only: effect -> bool
(** specification *)
......
......@@ -451,6 +451,13 @@ and dtype_v denv = function
(* expressions *)
let add_lemma_label ~top id = function
| Gnone -> id, false
| Gghost -> id, true
| Glemma when not top ->
errorm ~loc:id.id_loc "lemma functions are only allowed at toplevel"
| Glemma -> { id with id_lab = Lstr Mlw_wp.lemma_label :: id.id_lab }, true
let de_unit ~loc = hidden_ls ~loc Mlw_expr.fs_void
let de_app _loc e el =
......@@ -528,7 +535,7 @@ and de_desc denv loc = function
let e2 = dexpr denv e2 in
DElet (id, gh, e1, e2), e2.de_type
| Ptree.Eletrec (fdl, e1) ->
let fdl = dletrec denv fdl in
let fdl = dletrec ~top:false denv fdl in
let add_one denv (id,_,dvty,_,_) = add_poly id dvty denv in
let denv = List.fold_left add_one denv fdl in
let e1 = dexpr denv e1 in
......@@ -694,7 +701,7 @@ and de_desc denv loc = function
expected_type e1 dity_unit;
DEfor (id, efrom, dir, eto, inv, e1), e1.de_type
and dletrec denv fdl =
and dletrec ~top denv fdl =
(* add all functions into the environment *)
let add_one denv (_,id,_,bl,_) =
let argl = List.map (fun _ -> create_type_variable ()) bl in
......@@ -709,6 +716,7 @@ and dletrec denv fdl =
let denvl = List.map2 bind_one fdl dvtyl in
(* then type-check the bodies *)
let type_one (loc,id,gh,_,tr) (denv,bl,tyl,tyv) =
let id, gh = add_lemma_label ~top id gh in
let tr, (argl, res) = dtriple denv tr in
if argl <> [] then errorm ~loc
"The body of a recursive function must be a first-order value";
......@@ -910,8 +918,8 @@ and rletrec denv fdl =
let dexpr denv e =
rexpr denv (dexpr denv e)
let dletrec denv fdl =
rletrec denv (dletrec denv fdl)
let dletrec ~top denv fdl =
rletrec denv (dletrec ~top denv fdl)
(** stage 2 *)
......@@ -2030,6 +2038,7 @@ let add_decl ~wp loc uc d =
let add_pdecl ~wp loc uc = function
| Dlet (id, gh, e) ->
let id, gh = add_lemma_label ~top:true id gh in
let e = dexpr (create_denv uc) e in
let pd = match e.de_desc with
| DEfun (bl, tr) ->
......@@ -2043,7 +2052,7 @@ let add_pdecl ~wp loc uc = function
create_let_decl def in
add_pdecl_with_tuples ~wp uc pd
| Dletrec fdl ->
let fdl = dletrec (create_denv uc) fdl in
let fdl = dletrec ~top:true (create_denv uc) fdl in
let fdl = expr_rec (create_lenv uc) fdl in
let pd = create_rec_decl fdl in
add_pdecl_with_tuples ~wp uc pd
......
This diff is collapsed.
......@@ -17,6 +17,8 @@ open Mlw_expr
(** WP-only builtins *)
val lemma_label : Ident.label
val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty
......@@ -39,16 +41,11 @@ val full_invariant :
(** Weakest preconditions *)
val wp_val: Env.env -> known_map -> theory_uc -> let_sym -> theory_uc
val wp_let: Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
val wp_rec: Env.env -> known_map -> theory_uc -> fun_defn list -> theory_uc
(** Efficient weakest preconditions *)
val fast_wp: Debug.flag
val wp_val:
wp:bool -> Env.env -> known_map -> theory_uc -> let_sym -> theory_uc
val wp_let:
wp:bool -> Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
val wp_rec:
wp:bool -> Env.env -> known_map -> theory_uc -> fun_defn list -> theory_uc
val fast_wp_val: Env.env -> known_map -> theory_uc -> let_sym -> theory_uc
val fast_wp_let: Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
val fast_wp_rec: Env.env -> known_map -> theory_uc -> fun_defn list -> theory_uc
module LemmaFunction1
use import int.Int
use import ref.Refint
function fact int : int
axiom fact0 : fact 0 = 1
axiom factn : forall n: int. n > 0 -> fact n = n * fact (n - 1)
let rec lemma f (n: int) : unit variant {n}
requires { n >= 0 }
ensures { fact n >= 1 }
=
if n > 0 then f (n-1)
goal g: fact 42 >= 1
end
module LemmaFunction2
use import int.Int
use import array.Array
use import array.ArraySum
let rec lemma sum_nonneg (a: array int) (l u: int) : unit
requires { 0 <= l <= u <= length a }
requires { forall i: int. 0 <= i < length a -> a[i] >= 0 }
variant { u-l }
ensures { sum a l u >= 0 }
=
if u > l then sum_nonneg a (l+1) u
goal g1:
forall a: array int.
(forall i: int. 0 <= i < length a -> a[i] >= 0) ->
sum a 0 (length a) >= 0
end
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