← Back to branch summary

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

« back to all changes in this revision

Viewing changes to cil/src/check.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:
cil/src/check.mli
 
1
(**************************************************************************)
 
2
(*                                                                        *)
 
3
(*  Copyright (C) 2001-2003,                                              *)
 
4
(*   George C. Necula    <necula@cs.berkeley.edu>                         *)
 
5
(*   Scott McPeak        <smcpeak@cs.berkeley.edu>                        *)
 
6
(*   Wes Weimer          <weimer@cs.berkeley.edu>                         *)
 
7
(*   Ben Liblit          <liblit@cs.berkeley.edu>                         *)
 
8
(*  All rights reserved.                                                  *)
 
9
(*                                                                        *)
 
10
(*  Redistribution and use in source and binary forms, with or without    *)
 
11
(*  modification, are permitted provided that the following conditions    *)
 
12
(*  are met:                                                              *)
 
13
(*                                                                        *)
 
14
(*  1. Redistributions of source code must retain the above copyright     *)
 
15
(*  notice, this list of conditions and the following disclaimer.         *)
 
16
(*                                                                        *)
 
17
(*  2. Redistributions in binary form must reproduce the above copyright  *)
 
18
(*  notice, this list of conditions and the following disclaimer in the   *)
 
19
(*  documentation and/or other materials provided with the distribution.  *)
 
20
(*                                                                        *)
 
21
(*  3. The names of the contributors may not be used to endorse or        *)
 
22
(*  promote products derived from this software without specific prior    *)
 
23
(*  written permission.                                                   *)
 
24
(*                                                                        *)
 
25
(*  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS   *)
 
26
(*  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT     *)
 
27
(*  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS     *)
 
28
(*  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE        *)
 
29
(*  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,   *)
 
30
(*  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,  *)
 
31
(*  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;      *)
 
32
(*  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER      *)
 
33
(*  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT    *)
 
34
(*  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN     *)
 
35
(*  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE       *)
 
36
(*  POSSIBILITY OF SUCH DAMAGE.                                           *)
 
37
(*                                                                        *)
 
38
(*  File modified by CEA (Commissariat � l'�nergie Atomique).             *)
 
39
(**************************************************************************)
 
40
 
 
41
(* 
 
42
 *
 
43
 * Copyright (c) 2001-2002, 
 
44
 *  George C. Necula    <necula@cs.berkeley.edu>
 
45
 *  Scott McPeak        <smcpeak@cs.berkeley.edu>
 
46
 *  Wes Weimer          <weimer@cs.berkeley.edu>
 
47
 * All rights reserved.
 
48
 * 
 
49
 * Redistribution and use in source and binary forms, with or without
 
50
 * modification, are permitted provided that the following conditions are
 
51
 * met:
 
52
 *
 
53
 * 1. Redistributions of source code must retain the above copyright
 
54
 * notice, this list of conditions and the following disclaimer.
 
55
 *
 
56
 * 2. Redistributions in binary form must reproduce the above copyright
 
57
 * notice, this list of conditions and the following disclaimer in the
 
58
 * documentation and/or other materials provided with the distribution.
 
59
 *
 
60
 * 3. The names of the contributors may not be used to endorse or promote
 
61
 * products derived from this software without specific prior written
 
62
 * permission.
 
63
 *
 
64
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
 
65
 * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
 
66
 * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 
67
 * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
 
68
 * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
 
69
 * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
 
70
 * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
 
71
 * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
 
72
 * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
 
73
 * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 
74
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
75
 *
 
76
 *)
 
77
 
 
78
    (* Checks the well-formedness of the file. Prints warnings and
 
79
     * returns false if errors are found *)
 
80
 
 
81
type checkFlags = 
 
82
    NoCheckGlobalIds   (* Do not check that the global ids have the proper 
 
83
                        * hash value *) 
 
84
 
 
85
val checkFile: checkFlags list -> Cil_types.file -> bool