File: errors.ml

package info (click to toggle)
alt-ergo 0.95.2-3
  • links: PTS, VCS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 1,528 kB
  • ctags: 3,449
  • sloc: ml: 19,645; makefile: 354
file content (137 lines) | stat: -rw-r--r-- 5,371 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
(******************************************************************************)
(*     The Alt-Ergo theorem prover                                            *)
(*     Copyright (C) 2006-2013                                                *)
(*     CNRS - INRIA - Universite Paris Sud                                    *)
(*                                                                            *)
(*     Sylvain Conchon                                                        *)
(*     Evelyne Contejean                                                      *)
(*                                                                            *)
(*     Francois Bobot                                                         *)
(*     Mohamed Iguernelala                                                    *)
(*     Stephane Lescuyer                                                      *)
(*     Alain Mebsout                                                          *)
(*                                                                            *)
(*   This file is distributed under the terms of the CeCILL-C licence         *)
(******************************************************************************)

open Loc
open Format

type error = 
  | BitvExtract of int*int
  | BitvExtractRange of int*int
  | ClashType of string
  | ClashLabel of string * string
  | ClashParam of string
  | TypeDuplicateVar of string
  | UnboundedVar of string
  | UnknownType of string
  | WrongArity of string * int
  | SymbAlreadyDefined of string 
  | SymbUndefined of string
  | NotAPropVar of string
  | NotAPredicate of string
  | Unification of Ty.t * Ty.t
  | ShouldBeApply of string
  | WrongNumberofArgs of string
  | ShouldHaveType of Ty.t * Ty.t
  | ShouldHaveTypeIntorReal of Ty.t
  | ShouldHaveTypeInt of Ty.t
  | ShouldHaveTypeBitv of Ty.t
  | ArrayIndexShouldHaveTypeInt
  | ShouldHaveTypeArray
  | ShouldHaveTypeRecord of Ty.t
  | ShouldBeARecord
  | ShouldHaveLabel of string * string
  | NoLabelInType of Hstring.t * Ty.t
  | ShouldHaveTypeProp
  | NoRecordType of Hstring.t
  | DuplicateLabel of Hstring.t
  | WrongLabel of Hstring.t * Ty.t
  | WrongNumberOfLabels
  | Notrigger 
  | CannotGeneralize
  | SyntaxError

exception Error of error * loc
exception Warning of error * loc

let report fmt = function
  | BitvExtract(i,j) -> 
    fprintf fmt "bitvector extraction malformed (%d>%d)" i j
  | BitvExtractRange(n,j) -> 
    fprintf fmt "extraction out of range (%d>%d)" j n
  | ClashType s -> 
    fprintf fmt "the type %s is already defined" s
  | ClashParam s -> 
    fprintf fmt "parameter %s is bound twice" s
  | ClashLabel (s,t) -> 
    fprintf fmt "the label %s already appears in type %s" s t
  | CannotGeneralize -> 
    fprintf fmt "cannot generalize the type of this expression"
  | TypeDuplicateVar s ->
    fprintf fmt "duplicate type variable %s" s
  | UnboundedVar s ->
    fprintf fmt "unbounded variable %s" s
  | UnknownType s -> 
    fprintf fmt "unknown type %s" s
  | WrongArity(s,n) -> 
    fprintf fmt "the type %s has %d arguments" s n
  | SymbAlreadyDefined s -> 
    fprintf fmt "the symbol %s is already defined" s
  | SymbUndefined s -> 
    fprintf fmt "undefined symbol %s" s
  | NotAPropVar s -> 
    fprintf fmt "%s is not a propositional variable" s
  | NotAPredicate s -> 
    fprintf fmt "%s is not a predicate" s
  | Unification(t1,t2) ->
    fprintf fmt "%a and %a cannot be unified" Ty.print t1 Ty.print t2
  | ShouldBeApply s -> 
    fprintf fmt "%s is a function symbol, it should be apply" s
  | WrongNumberofArgs s ->
    fprintf fmt "Wrong number of arguments when applying %s" s
  | ShouldHaveType(ty1,ty2) ->
    fprintf fmt "this expression has type %a but is here used with type %a"
      Ty.print ty1 Ty.print ty2
  | ShouldHaveTypeBitv t -> 
    fprintf fmt "this expression has type %a but it should be a bitvector"
      Ty.print t
  | ShouldHaveTypeIntorReal t ->
    fprintf fmt 
      "this expression has type %a but it should have type int or real"
      Ty.print t
  | ShouldHaveTypeInt t ->
    fprintf fmt 
      "this expression has type %a but it should have type int"
      Ty.print t
  | ShouldHaveTypeArray ->
    fprintf fmt "this expression should have type farray"
  | ShouldHaveTypeRecord t ->
    fprintf fmt "this expression has type %a but it should have a record type"
      Ty.print t
  | ShouldBeARecord ->
    fprintf fmt "this expression should have a record type"
  | ShouldHaveLabel (s, a) ->
    fprintf fmt "this expression has type %s which has no label %s" s a
  | NoLabelInType (lb, ty) ->
    fprintf fmt "no label %s in type %a" (Hstring.view lb) Ty.print ty
  | ShouldHaveTypeProp -> 
    fprintf fmt "this expression should have type prop"
  | NoRecordType s ->
    fprintf fmt "no record type has label %s" (Hstring.view s)
  | DuplicateLabel s -> 
    fprintf fmt "label %s is defined several times" (Hstring.view s)
  | WrongLabel (s, ty) -> 
    fprintf fmt "wrong label %s in type %a" (Hstring.view s) Ty.print ty
  | WrongNumberOfLabels -> 
    fprintf fmt "wrong number of labels"
  | ArrayIndexShouldHaveTypeInt -> 
    fprintf fmt "index of arrays should hava type int"
  | Notrigger -> 
    fprintf fmt "No trigger for this lemma"
  | SyntaxError -> 
    fprintf fmt "syntax error"

let error e l = raise (Error(e,l))
let warning e l = raise (Warning(e,l))