← Back to branch summary

~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to src/logic/why_output.mli

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/logic/why_output.mli
 
1
(**************************************************************************)
 
2
(*                                                                        *)
 
3
(*  This file is part of Frama-C.                                         *)
 
4
(*                                                                        *)
 
5
(*  Copyright (C) 2007-2008                                               *)
 
6
(*    CEA   (Commissariat � l'�nergie Atomique)                           *)
 
7
(*    INRIA (Institut National de Recherche en Informatique et en         *)
 
8
(*           Automatique)                                                 *)
 
9
(*                                                                        *)
 
10
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
 
11
(*  Lesser General Public License as published by the Free Software       *)
 
12
(*  Foundation, version 2.1.                                              *)
 
13
(*                                                                        *)
 
14
(*  It is distributed in the hope that it will be useful,                 *)
 
15
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
 
16
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
 
17
(*  GNU Lesser General Public License for more details.                   *)
 
18
(*                                                                        *)
 
19
(*  See the GNU Lesser General Public License version v2.1                *)
 
20
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
 
21
(*                                                                        *)
 
22
(**************************************************************************)
 
23
 
 
24
(* $Id: why_output.mli,v 1.12 2008/11/28 16:34:34 uid530 Exp $ *)
 
25
(** Why interface *)
 
26
 
 
27
open Fol
 
28
open Format
 
29
 
 
30
val pure_type : formatter -> pure_type -> unit
 
31
val term : formatter -> term -> unit
 
32
val predicate : formatter -> predicate -> unit
 
33
val decl : formatter -> decl -> unit
 
34
 
 
35
(** Output to file [file] the given predicate in why syntax *)
 
36
val output : string option -> file:string -> decl list -> unit
 
37
 
 
38
(** [prove basename prelude p] 
 
39
* First call [output] (see above) and generate a tmp file with
 
40
* [basename] and then call why, and then ergo *)
 
41
val prove : string -> string option -> decl list -> unit
 
42
 
 
43
(*                      
 
44
Local Variables:
 
45
compile-command: "make -C ../.."
 
46
End:
 
47
*)