Source file errors.ml

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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
(******************************************************************************)
(*                                                                            *)
(*     The Alt-Ergo theorem prover                                            *)
(*     Copyright (C) 2006-2013                                                *)
(*                                                                            *)
(*     Sylvain Conchon                                                        *)
(*     Evelyne Contejean                                                      *)
(*                                                                            *)
(*     Francois Bobot                                                         *)
(*     Mohamed Iguernelala                                                    *)
(*     Stephane Lescuyer                                                      *)
(*     Alain Mebsout                                                          *)
(*                                                                            *)
(*     CNRS - INRIA - Universite Paris Sud                                    *)
(*                                                                            *)
(*     This file is distributed under the terms of the Apache Software        *)
(*     License version 2.0                                                    *)
(*                                                                            *)
(*  ------------------------------------------------------------------------  *)
(*                                                                            *)
(*     Alt-Ergo: The SMT Solver For Software Verification                     *)
(*     Copyright (C) 2013-2018 --- OCamlPro SAS                               *)
(*                                                                            *)
(*     This file is distributed under the terms of the Apache Software        *)
(*     License version 2.0                                                    *)
(*                                                                            *)
(******************************************************************************)

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
  | DuplicatePattern of string
  | WrongLabel of Hstring.t * Ty.t
  | WrongNumberOfLabels
  | Notrigger
  | CannotGeneralize
  | SyntaxError
  | ThExtError of string
  | ThSemTriggerError
  | WrongDeclInTheory
  | ShouldBeADT of Ty.t
  | MatchNotExhaustive of Hstring.t list
  | MatchUnusedCases of Hstring.t list
  | NotAdtConstr of string * Ty.t

(* this is a typing error *)
exception Error of error * Loc.t

(* these two exception are used by the lexer and the parser *)
exception Lexical_error of Loc.t * string
exception Syntax_error of Loc.t * string


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)
  | DuplicatePattern s ->
    fprintf fmt "pattern %s is bound several times" 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"
  | ThExtError s ->
    fprintf fmt "Theory extension %S not recognized" s
  | ThSemTriggerError ->
    fprintf fmt "Semantic triggers are only allowed inside Theories"
  | WrongDeclInTheory ->
    fprintf fmt
      "Currently, this kind of declarations are not allowed inside theories"
  | ShouldBeADT ty ->
    fprintf fmt "%a is not an algebraic, a record or an enumeration datatype"
      Ty.print ty

  | MatchNotExhaustive missing ->
    fprintf fmt
      "Pattern-matching is not exhaustive. These cases are missing: %a"
      (Util.print_list ~sep:" |" ~pp:Hstring.print) missing

  | MatchUnusedCases dead ->
    fprintf fmt
      "Pattern-matching contains unreachable cases. These cases are removed: %a"
      (Util.print_list ~sep:" |" ~pp:Hstring.print) dead

  | NotAdtConstr (lbl, ty) ->
    fprintf fmt
      "The symbol %s is not a constructor of the type %a" lbl Ty.print ty

let error e l = raise (Error(e,l))
let warning e l =
  if Options.unsat_mode () then Format.fprintf err_formatter "; ";
  Loc.report err_formatter l;
  report err_formatter e;
  Format.eprintf "@."