Skip to content

GitLab

why3
why3
Commit dbe86ac8 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

headers

parent 2f978a5f
Hide whitespace changes
Inline Side-by-side
Showing with 436 additions and 125 deletions
src/coq-plugin/g_whytac.ml4
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
(*i camlp4deps: "parsing/grammar.cma" i*)
......
src/coq-plugin/whytac.ml
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
open Names
open Nameops
......
src/ide/ide_main.ml
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
(* POUR L'INSTANT, CE NE SONT ICI QUE DES EXPRIENCES
MERCI DE NE PAS CONSIDRER CE CODE COMME DFINITIF
......
src/manager/db.ml
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
open Sqlite3
......
src/manager/db.mli
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
(** {1 Proof manager database} *)
......
src/manager/orm_schema.ml
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
#load "printer_utils.cmo"
#load "sql_orm_header.cmo"
#load "sql_orm.cmo"
......
src/manager/state.mli
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
(** {1 Proof manager database} *)
......
src/manager/test.ml
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
open Format
open Why
......
src/printer/alt_ergo.ml
View file @ dbe86ac8
......@@ -16,6 +16,7 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Register
open Format
open Pp
......
src/printer/smt.ml
View file @ dbe86ac8
......@@ -16,6 +16,7 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Register
open Format
open Pp
......
src/printer/tptp.ml
View file @ dbe86ac8
......@@ -16,6 +16,7 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Register
open Format
open Pp
......
src/programs/pgm_effect.ml
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
open Why
open Util
......@@ -39,5 +57,8 @@ type t = {
let empty = { reads = R.empty; writes = R.empty; raises = E.empty }
let add_read r t = { t with reads = R.add r t.reads }
let add_write r t = { t with writes = R.add r t.writes }
let add_raise e t = { t with raises = E.add e t.raises }
src/programs/pgm_effect.mli
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
open Why
open Term
......@@ -13,5 +31,8 @@ type t = private {
val empty : t
val add_read : reference -> t -> t
val add_write : reference -> t -> t
val add_raise : lsymbol -> t -> t
src/programs/pgm_itree.ml
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
open Why
......
src/programs/pgm_parser.mly
View file @ dbe86ac8
......@@ -288,8 +288,6 @@ expr:
{ mk_expr (Efun ($2, $4)) }
| MATCH list1_expr_sep_comma WITH option_bar match_cases END
{ mk_expr (Ematch ($2, $5)) }
| GHOST expr
{ mk_expr (Eghost $2) }
| LABEL uident COLON expr
{ mk_expr (Elabel ($2, $4)) }
| WHILE expr DO loop_annotation expr DONE
......
src/programs/pgm_ptree.ml
View file @ dbe86ac8
......@@ -91,7 +91,6 @@ and expr_desc =
| Etry of expr * (ident * ident option * expr) list
(* annotations *)
| Eassert of assertion_kind * lexpr
| Eghost of expr
| Elabel of ident * expr
| Ecast of expr * Ptree.pty
| Eany of type_c
......
src/programs/pgm_ttree.ml
View file @ dbe86ac8
......@@ -95,7 +95,6 @@ and dexpr_desc =
| DEtry of dexpr * (Term.lsymbol * string option * dexpr) list
| DEassert of assertion_kind * Ptree.lexpr
| DEghost of dexpr
| DElabel of string * dexpr
| DEany of dtype_c
......@@ -164,7 +163,6 @@ and expr_desc =
| Etry of expr * (Term.lsymbol * Term.vsymbol option * expr) list
| Eassert of assertion_kind * Term.fmla
| Eghost of expr
| Elabel of string * expr
| Eany of type_c
......
src/programs/pgm_typing.ml
View file @ dbe86ac8
......@@ -384,9 +384,6 @@ and dexpr_desc env loc = function
| Pgm_ptree.Eassert (k, le) ->
DEassert (k, lexpr le), (dty_unit env.uc)
| Pgm_ptree.Eghost e1 ->
let e1 = dexpr env e1 in
DEghost e1, e1.dexpr_type
| Pgm_ptree.Elabel ({id=l}, e1) ->
let ty = dty_label env.uc in
let env = { env with denv = Typing.add_var l ty env.denv } in
......@@ -581,8 +578,6 @@ and expr_desc uc env denv = function
| DEassert (k, f) ->
let f = Typing.type_fmla denv env f in
Eassert (k, f)
| DEghost e1 ->
Eghost (expr uc env e1)
| DElabel (s, e1) ->
let ty = Denv.ty_of_dty (Typing.find_var s e1.dexpr_denv) in
let v = create_vsymbol (id_fresh s) ty in
......
src/programs/pgm_typing.mli
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
open Why
open Theory
......
src/programs/pgm_wp.ml
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
open Why
open Ident
open Term
open Decl
open Theory
open Pgm_ttree
open Pgm_itree
module E = Pgm_effect
(* translation to intermediate trees and effect inference *)
let rec expr e =
let ty = e.Pgm_ttree.expr_type in
let loc = e.Pgm_ttree.expr_loc in
let d, ef = expr_desc loc ty e.Pgm_ttree.expr_desc in
{ expr_desc = d; expr_type = ty; expr_effect = ef; expr_loc = loc }
and expr_desc _loc ty = function
| Pgm_ttree.Econstant c ->
Elogic (t_const c ty), E.empty
| _ ->
assert false (*TODO*)
and recfun _ =
assert false (*TODO*)
(* weakest preconditions *)
let wp _l _e = f_true (* TODO *)
......@@ -16,13 +55,18 @@ let add_wp_decl uc l f =
add_decl uc d
let decl uc = function
| Dlet (l, e) ->
| Pgm_ttree.Dlet (l, e) ->
let e = expr e in
let f = wp l e in
add_wp_decl uc l f
| Dletrec dl ->
let add_one uc (l, def) = let f = wp_recfun l def in add_wp_decl uc l f in
| Pgm_ttree.Dletrec dl ->
let add_one uc (l, def) =
let def = recfun def in
let f = wp_recfun l def in
add_wp_decl uc l f
in
List.fold_left add_one uc dl
| Dparam _ ->
| Pgm_ttree.Dparam _ ->
uc
let file uc dl =
......
src/programs/pgm_wp.mli
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
open Why
open Theory
......
src/tptp2why/tptp2why.ml
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
(** this is a tool to convert tptp files (.p files) to .why files *)
open TptpTree
......
src/tptp2why/tptpLexer.mll
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
{
open Format
......
src/tptp2why/tptpParser.mly
View file @ dbe86ac8
/**************************************************************************/
/* */
/* Copyright (C) 2010- */
/* Francois Bobot */
/* Jean-Christophe Filliatre */
/* Johannes Kanig */
/* Andrei Paskevich */
/* */
/* This software is free software; you can redistribute it and/or */
/* modify it under the terms of the GNU Library General Public */
/* License version 2.1, with the special exception on linking */
/* described in file LICENSE. */
/* */
/* This software 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. */
/* */
/**************************************************************************/
%{
......
src/tptp2why/tptpTranslate.ml
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
(** module to translate from the basic abstract tree from the parser
to a proper why internal representation to be pretty-printed *)
......
src/tptp2why/tptpTranslate.mli
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
val theory_of_decls : string -> TptpTree.decl list -> Why.Theory.theory
......
src/tptp2why/tptpTree.ml
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
(** abstract tree representation *)
type atom = string
......
src/util/rc.mli
View file @ dbe86ac8
(**************************************************************************)
(* *)
(* The Why platform for program certification *)
(* Copyright (C) 2002-2008 *)
(* Romain BARDOU *)
(* Jean-François COUCHOT *)
(* Mehdi DOGGUY *)
(* Jean-Christophe FILLIÂTRE *)
(* Thierry HUBERT *)
(* Claude MARCHÉ *)
(* Yannick MOY *)
(* Christine PAULIN *)
(* Yann RÉGIS-GIANAS *)
(* Nicolas ROUSSET *)
(* Xavier URBAIN *)</