Changeset 2649 for extracted/cexec.ml


Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/cexec.ml

    r2601 r2649  
    3939open Identifiers
    4040
    41 open Floats
    42 
    4341open Integers
    4442
     
    7169open Proper
    7270
     71open ErrorMessages
     72
    7373open Option
    7474
     
    7979open Positive
    8080
    81 open Char
    82 
    83 open String
    84 
    8581open PreIdentifiers
    8682
     
    116112
    117113open Csem
    118 
    119 (** val valueIsNotABoolean : String.string **)
    120 let valueIsNotABoolean = "value is not a boolean"
    121   (* failwith "AXIOM TO BE REALIZED" *)
    122114
    123115(** val exec_bool_of_val :
     
    125117let exec_bool_of_val v ty =
    126118  match v with
    127   | Values.Vundef -> Errors.Error (Errors.msg valueIsNotABoolean)
     119  | Values.Vundef ->
     120    Errors.Error (Errors.msg ErrorMessages.ValueIsNotABoolean)
    128121  | Values.Vint (sz, i) ->
    129122    (match ty with
    130      | Csyntax.Tvoid -> Errors.Error (Errors.msg TypeComparison.typeMismatch)
     123     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    131124     | Csyntax.Tint (sz', x) ->
    132125       AST.intsize_eq_elim sz sz' i (fun i0 -> Errors.OK
     
    134127           (BitVector.eq_bv (AST.bitsize_of_intsize sz') i0
    135128             (BitVector.zero (AST.bitsize_of_intsize sz'))))) (Errors.Error
    136          (Errors.msg TypeComparison.typeMismatch))
     129         (Errors.msg ErrorMessages.TypeMismatch))
    137130     | Csyntax.Tpointer x ->
    138        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     131       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    139132     | Csyntax.Tarray (x, x0) ->
    140        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     133       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    141134     | Csyntax.Tfunction (x, x0) ->
    142        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     135       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    143136     | Csyntax.Tstruct (x, x0) ->
    144        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     137       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    145138     | Csyntax.Tunion (x, x0) ->
    146        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     139       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    147140     | Csyntax.Tcomp_ptr x ->
    148        Errors.Error (Errors.msg TypeComparison.typeMismatch))
     141       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    149142  | Values.Vnull ->
    150143    (match ty with
    151      | Csyntax.Tvoid -> Errors.Error (Errors.msg TypeComparison.typeMismatch)
     144     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    152145     | Csyntax.Tint (x, x0) ->
    153        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     146       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    154147     | Csyntax.Tpointer x -> Errors.OK Bool.False
    155148     | Csyntax.Tarray (x, x0) ->
    156        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     149       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    157150     | Csyntax.Tfunction (x, x0) ->
    158        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     151       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    159152     | Csyntax.Tstruct (x, x0) ->
    160        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     153       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    161154     | Csyntax.Tunion (x, x0) ->
    162        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     155       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    163156     | Csyntax.Tcomp_ptr x ->
    164        Errors.Error (Errors.msg TypeComparison.typeMismatch))
     157       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    165158  | Values.Vptr x ->
    166159    (match ty with
    167      | Csyntax.Tvoid -> Errors.Error (Errors.msg TypeComparison.typeMismatch)
     160     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    168161     | Csyntax.Tint (x0, x1) ->
    169        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     162       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    170163     | Csyntax.Tpointer x0 -> Errors.OK Bool.True
    171164     | Csyntax.Tarray (x0, x1) ->
    172        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     165       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    173166     | Csyntax.Tfunction (x0, x1) ->
    174        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     167       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    175168     | Csyntax.Tstruct (x0, x1) ->
    176        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     169       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    177170     | Csyntax.Tunion (x0, x1) ->
    178        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     171       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    179172     | Csyntax.Tcomp_ptr x0 ->
    180        Errors.Error (Errors.msg TypeComparison.typeMismatch))
    181 
    182 (** val badCast : String.string **)
    183 let badCast = "bad cast"
    184   (* failwith "AXIOM TO BE REALIZED" *)
     173       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    185174
    186175(** val try_cast_null :
     
    192181  | Bool.True ->
    193182    (match ty with
    194      | Csyntax.Tvoid -> Errors.Error (Errors.msg badCast)
     183     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
    195184     | Csyntax.Tint (sz', x) ->
    196185       (match AST.eq_intsize sz sz' with
    197186        | Bool.True ->
    198187          (match ty' with
    199            | Csyntax.Tvoid -> Errors.Error (Errors.msg badCast)
    200            | Csyntax.Tint (x0, x1) -> Errors.Error (Errors.msg badCast)
     188           | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
     189           | Csyntax.Tint (x0, x1) ->
     190             Errors.Error (Errors.msg ErrorMessages.BadCast)
    201191           | Csyntax.Tpointer x0 -> Errors.OK Values.Vnull
    202192           | Csyntax.Tarray (x0, x1) -> Errors.OK Values.Vnull
    203193           | Csyntax.Tfunction (x0, x1) -> Errors.OK Values.Vnull
    204            | Csyntax.Tstruct (x0, x1) -> Errors.Error (Errors.msg badCast)
    205            | Csyntax.Tunion (x0, x1) -> Errors.Error (Errors.msg badCast)
    206            | Csyntax.Tcomp_ptr x0 -> Errors.Error (Errors.msg badCast))
    207         | Bool.False -> Errors.Error (Errors.msg TypeComparison.typeMismatch))
    208      | Csyntax.Tpointer x -> Errors.Error (Errors.msg badCast)
    209      | Csyntax.Tarray (x, x0) -> Errors.Error (Errors.msg badCast)
    210      | Csyntax.Tfunction (x, x0) -> Errors.Error (Errors.msg badCast)
    211      | Csyntax.Tstruct (x, x0) -> Errors.Error (Errors.msg badCast)
    212      | Csyntax.Tunion (x, x0) -> Errors.Error (Errors.msg badCast)
    213      | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg badCast))
    214   | Bool.False -> Errors.Error (Errors.msg badCast)
     194           | Csyntax.Tstruct (x0, x1) ->
     195             Errors.Error (Errors.msg ErrorMessages.BadCast)
     196           | Csyntax.Tunion (x0, x1) ->
     197             Errors.Error (Errors.msg ErrorMessages.BadCast)
     198           | Csyntax.Tcomp_ptr x0 ->
     199             Errors.Error (Errors.msg ErrorMessages.BadCast))
     200        | Bool.False -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
     201     | Csyntax.Tpointer x -> Errors.Error (Errors.msg ErrorMessages.BadCast)
     202     | Csyntax.Tarray (x, x0) ->
     203       Errors.Error (Errors.msg ErrorMessages.BadCast)
     204     | Csyntax.Tfunction (x, x0) ->
     205       Errors.Error (Errors.msg ErrorMessages.BadCast)
     206     | Csyntax.Tstruct (x, x0) ->
     207       Errors.Error (Errors.msg ErrorMessages.BadCast)
     208     | Csyntax.Tunion (x, x0) ->
     209       Errors.Error (Errors.msg ErrorMessages.BadCast)
     210     | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg ErrorMessages.BadCast))
     211  | Bool.False -> Errors.Error (Errors.msg ErrorMessages.BadCast)
    215212
    216213(** val ptr_like_type : Csyntax.type0 -> Bool.bool **)
     
    230227let exec_cast m v ty ty' =
    231228  match v with
    232   | Values.Vundef -> Errors.Error (Errors.msg badCast)
     229  | Values.Vundef -> Errors.Error (Errors.msg ErrorMessages.BadCast)
    233230  | Values.Vint (sz, i) ->
    234231    (match ty with
    235      | Csyntax.Tvoid -> Errors.Error (Errors.msg TypeComparison.typeMismatch)
     232     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    236233     | Csyntax.Tint (sz1, si1) ->
    237234       AST.intsize_eq_elim sz sz1 i (fun i0 ->
    238235         match ty' with
    239          | Csyntax.Tvoid -> Errors.Error (Errors.msg badCast)
     236         | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
    240237         | Csyntax.Tint (sz2, si2) ->
    241238           Errors.OK (Values.Vint (sz2, (Csem.cast_int_int sz1 si1 sz2 i0)))
     
    255252               (Obj.magic (try_cast_null m sz1 i0 ty ty')) (fun r ->
    256253               Obj.magic (Errors.OK r)))
    257          | Csyntax.Tstruct (x, x0) -> Errors.Error (Errors.msg badCast)
    258          | Csyntax.Tunion (x, x0) -> Errors.Error (Errors.msg badCast)
    259          | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg badCast))
    260          (Errors.Error (Errors.msg badCast))
     254         | Csyntax.Tstruct (x, x0) ->
     255           Errors.Error (Errors.msg ErrorMessages.BadCast)
     256         | Csyntax.Tunion (x, x0) ->
     257           Errors.Error (Errors.msg ErrorMessages.BadCast)
     258         | Csyntax.Tcomp_ptr x ->
     259           Errors.Error (Errors.msg ErrorMessages.BadCast)) (Errors.Error
     260         (Errors.msg ErrorMessages.BadCast))
    261261     | Csyntax.Tpointer x ->
    262262       Obj.magic
     
    275275           Obj.magic (Errors.OK r)))
    276276     | Csyntax.Tstruct (x, x0) ->
    277        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     277       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    278278     | Csyntax.Tunion (x, x0) ->
    279        Errors.Error (Errors.msg TypeComparison.typeMismatch)
     279       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    280280     | Csyntax.Tcomp_ptr x ->
    281        Errors.Error (Errors.msg TypeComparison.typeMismatch))
     281       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    282282  | Values.Vnull ->
    283283    (match Bool.andb (ptr_like_type ty) (ptr_like_type ty') with
    284284     | Bool.True -> Errors.OK Values.Vnull
    285      | Bool.False -> Errors.Error (Errors.msg badCast))
     285     | Bool.False -> Errors.Error (Errors.msg ErrorMessages.BadCast))
    286286  | Values.Vptr ptr ->
    287287    (match Bool.andb (ptr_like_type ty) (ptr_like_type ty') with
    288288     | Bool.True -> Errors.OK (Values.Vptr ptr)
    289      | Bool.False -> Errors.Error (Errors.msg badCast))
     289     | Bool.False -> Errors.Error (Errors.msg ErrorMessages.BadCast))
    290290
    291291(** val load_value_of_type' :
     
    295295  let { Types.fst = loc; Types.snd = ofs } = l in
    296296  Csem.load_value_of_type ty m loc ofs
    297 
    298 (** val badlyTypedTerm : String.string **)
    299 let badlyTypedTerm = "badly typed term"
    300   (* failwith "AXIOM TO BE REALIZED" *)
    301 
    302 (** val unknownIdentifier : String.string **)
    303 let unknownIdentifier = "unknown identifier"
    304   (* failwith "AXIOM TO BE REALIZED" *)
    305 
    306 (** val badLvalueTerm : String.string **)
    307 let badLvalueTerm = "bad lvalue term"
    308   (*failwith "AXIOM TO BE REALIZED"*)
    309 
    310 (** val failedLoad : String.string **)
    311 let failedLoad = "failed load"
    312   (* failwith "AXIOM TO BE REALIZED" *)
    313 
    314 (** val failedOp : String.string **)
    315 let failedOp = "failed op"
    316   (* failwith "AXIOM TO BE REALIZED" *)
    317297
    318298(** val exec_expr :
     
    324304   | Csyntax.Econst_int (sz, i) ->
    325305     (match ty with
    326       | Csyntax.Tvoid -> Errors.Error (Errors.msg badlyTypedTerm)
     306      | Csyntax.Tvoid ->
     307        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
    327308      | Csyntax.Tint (sz', x) ->
    328309        (match AST.eq_intsize sz sz' with
     
    330311           Errors.OK { Types.fst = (Values.Vint (sz, i)); Types.snd =
    331312             Events.e0 }
    332          | Bool.False -> Errors.Error (Errors.msg badlyTypedTerm))
    333       | Csyntax.Tpointer x -> Errors.Error (Errors.msg badlyTypedTerm)
    334       | Csyntax.Tarray (x, x0) -> Errors.Error (Errors.msg badlyTypedTerm)
    335       | Csyntax.Tfunction (x, x0) -> Errors.Error (Errors.msg badlyTypedTerm)
    336       | Csyntax.Tstruct (x, x0) -> Errors.Error (Errors.msg badlyTypedTerm)
    337       | Csyntax.Tunion (x, x0) -> Errors.Error (Errors.msg badlyTypedTerm)
    338       | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg badlyTypedTerm))
     313         | Bool.False ->
     314           Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
     315      | Csyntax.Tpointer x ->
     316        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     317      | Csyntax.Tarray (x, x0) ->
     318        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     319      | Csyntax.Tfunction (x, x0) ->
     320        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     321      | Csyntax.Tstruct (x, x0) ->
     322        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     323      | Csyntax.Tunion (x, x0) ->
     324        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     325      | Csyntax.Tcomp_ptr x ->
     326        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
    339327   | Csyntax.Evar x ->
    340328     Obj.magic
     
    343331         Monad.m_bind0 (Monad.max_def Errors.res0)
    344332           (Obj.magic
    345              (Errors.opt_to_res (Errors.msg failedLoad)
     333             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
    346334               (load_value_of_type' ty m l))) (fun v ->
    347335           Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
     
    352340         Monad.m_bind0 (Monad.max_def Errors.res0)
    353341           (Obj.magic
    354              (Errors.opt_to_res (Errors.msg failedLoad)
     342             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
    355343               (load_value_of_type' ty m l))) (fun v ->
    356344           Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
     
    361349         match ty with
    362350         | Csyntax.Tvoid ->
    363            Obj.magic (Errors.Error (Errors.msg badlyTypedTerm))
     351           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
    364352         | Csyntax.Tint (x, x0) ->
    365            Obj.magic (Errors.Error (Errors.msg badlyTypedTerm))
     353           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
    366354         | Csyntax.Tpointer x ->
    367355           let { Types.fst = loc; Types.snd = ofs } = lo in
     
    370358             tr })
    371359         | Csyntax.Tarray (x, x0) ->
    372            Obj.magic (Errors.Error (Errors.msg badlyTypedTerm))
     360           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
    373361         | Csyntax.Tfunction (x, x0) ->
    374            Obj.magic (Errors.Error (Errors.msg badlyTypedTerm))
     362           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
    375363         | Csyntax.Tstruct (x, x0) ->
    376            Obj.magic (Errors.Error (Errors.msg badlyTypedTerm))
     364           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
    377365         | Csyntax.Tunion (x, x0) ->
    378            Obj.magic (Errors.Error (Errors.msg badlyTypedTerm))
     366           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
    379367         | Csyntax.Tcomp_ptr x ->
    380            Obj.magic (Errors.Error (Errors.msg badlyTypedTerm))))
     368           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))))
    381369   | Csyntax.Eunop (op0, a) ->
    382370     Obj.magic
     
    385373         Monad.m_bind0 (Monad.max_def Errors.res0)
    386374           (Obj.magic
    387              (Errors.opt_to_res (Errors.msg failedOp)
     375             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
    388376               (Csem.sem_unary_operation op0 v1 (Csyntax.typeof a))))
    389377           (fun v -> Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
     
    396384           Monad.m_bind0 (Monad.max_def Errors.res0)
    397385             (Obj.magic
    398                (Errors.opt_to_res (Errors.msg failedOp)
     386               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
    399387                 (Csem.sem_binary_operation op0 v1 (Csyntax.typeof a1) v2
    400388                   (Csyntax.typeof a2) m ty))) (fun v ->
     
    437425                         (Values.of_bool b2)) with
    438426                 | Types.None ->
    439                    Obj.magic (Errors.Error (Errors.msg badlyTypedTerm))
     427                   Obj.magic (Errors.Error
     428                     (Errors.msg ErrorMessages.BadlyTypedTerm))
    440429                 | Types.Some v20 ->
    441430                   Obj.magic (Errors.OK { Types.fst = v20; Types.snd =
     
    444433             (match Csem.cast_bool_to_target ty (Types.Some Values.vfalse) with
    445434              | Types.None ->
    446                 Obj.magic (Errors.Error (Errors.msg badlyTypedTerm))
     435                Obj.magic (Errors.Error
     436                  (Errors.msg ErrorMessages.BadlyTypedTerm))
    447437              | Types.Some vfls ->
    448438                Obj.magic (Errors.OK { Types.fst = vfls; Types.snd = tr1 })))))
     
    457447             (match Csem.cast_bool_to_target ty (Types.Some Values.vtrue) with
    458448              | Types.None ->
    459                 Obj.magic (Errors.Error (Errors.msg badlyTypedTerm))
     449                Obj.magic (Errors.Error
     450                  (Errors.msg ErrorMessages.BadlyTypedTerm))
    460451              | Types.Some vtr ->
    461452                Obj.magic (Errors.OK { Types.fst = vtr; Types.snd = tr1 }))
     
    469460                         (Values.of_bool b2)) with
    470461                 | Types.None ->
    471                    Obj.magic (Errors.Error (Errors.msg badlyTypedTerm))
     462                   Obj.magic (Errors.Error
     463                     (Errors.msg ErrorMessages.BadlyTypedTerm))
    472464                 | Types.Some v20 ->
    473465                   Obj.magic (Errors.OK { Types.fst = v20; Types.snd =
     
    475467   | Csyntax.Esizeof ty' ->
    476468     (match ty with
    477       | Csyntax.Tvoid -> Errors.Error (Errors.msg badlyTypedTerm)
     469      | Csyntax.Tvoid ->
     470        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
    478471      | Csyntax.Tint (sz, x) ->
    479472        Errors.OK { Types.fst = (Values.Vint (sz,
    480473          (AST.repr0 sz (Csyntax.sizeof ty')))); Types.snd = Events.e0 }
    481       | Csyntax.Tpointer x -> Errors.Error (Errors.msg badlyTypedTerm)
    482       | Csyntax.Tarray (x, x0) -> Errors.Error (Errors.msg badlyTypedTerm)
    483       | Csyntax.Tfunction (x, x0) -> Errors.Error (Errors.msg badlyTypedTerm)
    484       | Csyntax.Tstruct (x, x0) -> Errors.Error (Errors.msg badlyTypedTerm)
    485       | Csyntax.Tunion (x, x0) -> Errors.Error (Errors.msg badlyTypedTerm)
    486       | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg badlyTypedTerm))
     474      | Csyntax.Tpointer x ->
     475        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     476      | Csyntax.Tarray (x, x0) ->
     477        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     478      | Csyntax.Tfunction (x, x0) ->
     479        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     480      | Csyntax.Tstruct (x, x0) ->
     481        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     482      | Csyntax.Tunion (x, x0) ->
     483        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     484      | Csyntax.Tcomp_ptr x ->
     485        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
    487486   | Csyntax.Efield (x, x0) ->
    488487     Obj.magic
     
    491490         Monad.m_bind0 (Monad.max_def Errors.res0)
    492491           (Obj.magic
    493              (Errors.opt_to_res (Errors.msg failedLoad)
     492             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
    494493               (load_value_of_type' ty m l))) (fun v ->
    495494           Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
     
    506505and exec_lvalue' ge0 en m e' ty =
    507506  match e' with
    508   | Csyntax.Econst_int (x, x0) -> Errors.Error (Errors.msg badLvalueTerm)
     507  | Csyntax.Econst_int (x, x0) ->
     508    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
    509509  | Csyntax.Evar id ->
    510     (match Identifiers.lookup0 AST.symbolTag en id with
     510    (match Identifiers.lookup0 PreIdentifiers.SymbolTag en id with
    511511     | Types.None ->
    512512       Obj.magic
    513513         (Monad.m_bind0 (Monad.max_def Errors.res0)
    514514           (Obj.magic
    515              (Errors.opt_to_res (List.Cons ((Errors.MSG unknownIdentifier),
    516                (List.Cons ((Errors.CTX (AST.symbolTag, id)), List.Nil))))
     515             (Errors.opt_to_res (List.Cons ((Errors.MSG
     516               ErrorMessages.UnknownIdentifier), (List.Cons ((Errors.CTX
     517               (PreIdentifiers.SymbolTag, id)), List.Nil))))
    517518               (Globalenvs.find_symbol ge0 id))) (fun l ->
    518519           Obj.magic (Errors.OK { Types.fst = { Types.fst = l; Types.snd =
     
    527528        match v with
    528529        | Values.Vundef ->
    529           Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))
     530          Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    530531        | Values.Vint (x, x0) ->
    531           Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))
     532          Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    532533        | Values.Vnull ->
    533           Obj.magic (Errors.Error (Errors.msg TypeComparison.typeMismatch))
     534          Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    534535        | Values.Vptr ptr ->
    535536          Obj.magic (Errors.OK { Types.fst = { Types.fst =
    536537            ptr.Pointers.pblock; Types.snd = ptr.Pointers.poff }; Types.snd =
    537538            tr })))
    538   | Csyntax.Eaddrof x -> Errors.Error (Errors.msg badLvalueTerm)
    539   | Csyntax.Eunop (x, x0) -> Errors.Error (Errors.msg badLvalueTerm)
    540   | Csyntax.Ebinop (x, x0, x1) -> Errors.Error (Errors.msg badLvalueTerm)
    541   | Csyntax.Ecast (x, x0) -> Errors.Error (Errors.msg badLvalueTerm)
    542   | Csyntax.Econdition (x, x0, x1) -> Errors.Error (Errors.msg badLvalueTerm)
    543   | Csyntax.Eandbool (x, x0) -> Errors.Error (Errors.msg badLvalueTerm)
    544   | Csyntax.Eorbool (x, x0) -> Errors.Error (Errors.msg badLvalueTerm)
    545   | Csyntax.Esizeof x -> Errors.Error (Errors.msg badLvalueTerm)
     539  | Csyntax.Eaddrof x ->
     540    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
     541  | Csyntax.Eunop (x, x0) ->
     542    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
     543  | Csyntax.Ebinop (x, x0, x1) ->
     544    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
     545  | Csyntax.Ecast (x, x0) ->
     546    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
     547  | Csyntax.Econdition (x, x0, x1) ->
     548    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
     549  | Csyntax.Eandbool (x, x0) ->
     550    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
     551  | Csyntax.Eorbool (x, x0) ->
     552    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
     553  | Csyntax.Esizeof x ->
     554    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
    546555  | Csyntax.Efield (a, i) ->
    547556    (match Csyntax.typeof a with
    548      | Csyntax.Tvoid -> Errors.Error (Errors.msg badlyTypedTerm)
    549      | Csyntax.Tint (x, x0) -> Errors.Error (Errors.msg badlyTypedTerm)
    550      | Csyntax.Tpointer x -> Errors.Error (Errors.msg badlyTypedTerm)
    551      | Csyntax.Tarray (x, x0) -> Errors.Error (Errors.msg badlyTypedTerm)
    552      | Csyntax.Tfunction (x, x0) -> Errors.Error (Errors.msg badlyTypedTerm)
     557     | Csyntax.Tvoid ->
     558       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     559     | Csyntax.Tint (x, x0) ->
     560       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     561     | Csyntax.Tpointer x ->
     562       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     563     | Csyntax.Tarray (x, x0) ->
     564       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     565     | Csyntax.Tfunction (x, x0) ->
     566       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
    553567     | Csyntax.Tstruct (id, fList) ->
    554568       Obj.magic
     
    567581           (Obj.magic (exec_lvalue ge0 en m a)) (fun lofs tr ->
    568582           Obj.magic (Errors.OK { Types.fst = lofs; Types.snd = tr })))
    569      | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg badlyTypedTerm))
    570   | Csyntax.Ecost (x, x0) -> Errors.Error (Errors.msg badLvalueTerm)
     583     | Csyntax.Tcomp_ptr x ->
     584       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
     585  | Csyntax.Ecost (x, x0) ->
     586    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
    571587(** val exec_lvalue :
    572588    Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr ->
     
    599615  let { Types.fst = m1; Types.snd = b1 } =
    600616    GenMem.alloc m (Z.z_of_nat Nat.O) (Z.z_of_nat (Csyntax.sizeof ty))
    601       AST.XData
    602617  in
    603   exec_alloc_variables (Identifiers.add AST.symbolTag en id (Types.pi1 b1))
    604     m1 vars
    605 
    606 (** val wrongNumberOfParameters : String.string **)
    607 let wrongNumberOfParameters = "wrong number of parameters"
    608   (* failwith "AXIOM TO BE REALIZED"*)
    609 
    610 (** val failedStore : String.string **)
    611 let failedStore = "failed store"
    612   (* failwith "AXIOM TO BE REALIZED"*)
     618  exec_alloc_variables (Identifiers.add PreIdentifiers.SymbolTag en id b1) m1
     619    vars
    613620
    614621(** val exec_bind_parameters :
     
    620627    (match vs with
    621628     | List.Nil -> Errors.OK m
    622      | List.Cons (x, x0) -> Errors.Error (Errors.msg wrongNumberOfParameters))
     629     | List.Cons (x, x0) ->
     630       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters))
    623631  | List.Cons (idty, params') ->
    624632    let { Types.fst = id; Types.snd = ty } = idty in
    625633    (match vs with
    626      | List.Nil -> Errors.Error (Errors.msg wrongNumberOfParameters)
     634     | List.Nil ->
     635       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
    627636     | List.Cons (v1, vl) ->
    628637       Obj.magic
    629638         (Monad.m_bind0 (Monad.max_def Errors.res0)
    630639           (Obj.magic
    631              (Errors.opt_to_res (List.Cons ((Errors.MSG unknownIdentifier),
    632                (List.Cons ((Errors.CTX (AST.symbolTag, id)), List.Nil))))
    633                (Identifiers.lookup0 AST.symbolTag e1 id))) (fun b ->
     640             (Errors.opt_to_res (List.Cons ((Errors.MSG
     641               ErrorMessages.UnknownIdentifier), (List.Cons ((Errors.CTX
     642               (PreIdentifiers.SymbolTag, id)), List.Nil))))
     643               (Identifiers.lookup0 PreIdentifiers.SymbolTag e1 id)))
     644           (fun b ->
    634645           Monad.m_bind0 (Monad.max_def Errors.res0)
    635646             (Obj.magic
    636                (Errors.opt_to_res (List.Cons ((Errors.MSG failedStore),
    637                  (List.Cons ((Errors.CTX (AST.symbolTag, id)), List.Nil))))
     647               (Errors.opt_to_res (List.Cons ((Errors.MSG
     648                 ErrorMessages.FailedStore), (List.Cons ((Errors.CTX
     649                 (PreIdentifiers.SymbolTag, id)), List.Nil))))
    638650                 (Csem.store_value_of_type ty m b Pointers.zero_offset v1)))
    639651             (fun m1 -> Obj.magic (exec_bind_parameters e1 m1 params' vl)))))
     
    675687  Csem.store_value_of_type ty m loc ofs v
    676688
    677 (** val nonsenseState : String.string **)
    678 let nonsenseState = "nonsense state"
    679   (*failwith "AXIOM TO BE REALIZED"*)
    680 
    681 (** val returnMismatch : String.string **)
    682 let returnMismatch = "return mismatch"
    683   (*failwith "AXIOM TO BE REALIZED"*)
    684 
    685 (** val unknownLabel : String.string **)
    686 let unknownLabel = "unkown label"
    687   (*failwith "AXIOM TO BE REALIZED"*)
    688 
    689 (** val badFunctionValue : String.string **)
    690 let badFunctionValue = "bad function value"
    691   (*failwith "AXIOM TO BE REALIZED"*)
    692 
    693689(** val exec_step :
    694690    Csem.genv0 -> Csem.state0 -> (IO.io_out, IO.io_in, (Events.trace,
     
    705701             (Values.Vundef, k,
    706702             (GenMem.free_list m (Csem.blocks_of_env e1)))) }
    707          | Csyntax.Tint (x, x0) -> IOMonad.Wrong (Errors.msg nonsenseState)
    708          | Csyntax.Tpointer x -> IOMonad.Wrong (Errors.msg nonsenseState)
    709          | Csyntax.Tarray (x, x0) -> IOMonad.Wrong (Errors.msg nonsenseState)
     703         | Csyntax.Tint (x, x0) ->
     704           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     705         | Csyntax.Tpointer x ->
     706           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     707         | Csyntax.Tarray (x, x0) ->
     708           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    710709         | Csyntax.Tfunction (x, x0) ->
    711            IOMonad.Wrong (Errors.msg nonsenseState)
     710           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    712711         | Csyntax.Tstruct (x, x0) ->
    713            IOMonad.Wrong (Errors.msg nonsenseState)
    714          | Csyntax.Tunion (x, x0) -> IOMonad.Wrong (Errors.msg nonsenseState)
    715          | Csyntax.Tcomp_ptr x -> IOMonad.Wrong (Errors.msg nonsenseState))
     712           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     713         | Csyntax.Tunion (x, x0) ->
     714           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     715         | Csyntax.Tcomp_ptr x ->
     716           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState))
    716717      | Csem.Kseq (s0, k') ->
    717718        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s0, k',
     
    753754             (Values.Vundef, k,
    754755             (GenMem.free_list m (Csem.blocks_of_env e1)))) }
    755          | Csyntax.Tint (x3, x4) -> IOMonad.Wrong (Errors.msg nonsenseState)
    756          | Csyntax.Tpointer x3 -> IOMonad.Wrong (Errors.msg nonsenseState)
     756         | Csyntax.Tint (x3, x4) ->
     757           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     758         | Csyntax.Tpointer x3 ->
     759           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    757760         | Csyntax.Tarray (x3, x4) ->
    758            IOMonad.Wrong (Errors.msg nonsenseState)
     761           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    759762         | Csyntax.Tfunction (x3, x4) ->
    760            IOMonad.Wrong (Errors.msg nonsenseState)
     763           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    761764         | Csyntax.Tstruct (x3, x4) ->
    762            IOMonad.Wrong (Errors.msg nonsenseState)
     765           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    763766         | Csyntax.Tunion (x3, x4) ->
    764            IOMonad.Wrong (Errors.msg nonsenseState)
    765          | Csyntax.Tcomp_ptr x3 -> IOMonad.Wrong (Errors.msg nonsenseState)))
     767           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     768         | Csyntax.Tcomp_ptr x3 ->
     769           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)))
    766770   | Csyntax.Sassign (a1, a2) ->
    767771     Obj.magic
     
    774778           Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    775779             (Obj.magic
    776                (IOMonad.opt_to_io (Errors.msg failedStore)
     780               (IOMonad.opt_to_io (Errors.msg ErrorMessages.FailedStore)
    777781                 (store_value_of_type' (Csyntax.typeof a1) m l v2)))
    778782             (fun m' ->
     
    790794           Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    791795             (Obj.magic
    792                (IOMonad.opt_to_io (Errors.msg badFunctionValue)
     796               (IOMonad.opt_to_io (Errors.msg ErrorMessages.BadFunctionValue)
    793797                 (Globalenvs.find_funct ge0 vf))) (fun fd ->
    794798             Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
     
    873877   | Csyntax.Sbreak ->
    874878     (match k with
    875       | Csem.Kstop -> IOMonad.Wrong (Errors.msg nonsenseState)
     879      | Csem.Kstop -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    876880      | Csem.Kseq (s', k') ->
    877881        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
     
    887891          Csyntax.Sskip, k', e1, m)) }
    888892      | Csem.Kfor3 (x, x0, x1, x2) ->
    889         IOMonad.Wrong (Errors.msg nonsenseState)
     893        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    890894      | Csem.Kswitch k' ->
    891895        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    892896          Csyntax.Sskip, k', e1, m)) }
    893897      | Csem.Kcall (x, x0, x1, x2) ->
    894         IOMonad.Wrong (Errors.msg nonsenseState))
     898        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState))
    895899   | Csyntax.Scontinue ->
    896900     (match k with
    897       | Csem.Kstop -> IOMonad.Wrong (Errors.msg nonsenseState)
     901      | Csem.Kstop -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    898902      | Csem.Kseq (s', k') ->
    899903        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
     
    924928          (Csem.Kfor3 (a2, a3, s', k')), e1, m)) }
    925929      | Csem.Kfor3 (x, x0, x1, x2) ->
    926         IOMonad.Wrong (Errors.msg nonsenseState)
     930        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    927931      | Csem.Kswitch k' ->
    928932        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    929933          Csyntax.Scontinue, k', e1, m)) }
    930934      | Csem.Kcall (x, x0, x1, x2) ->
    931         IOMonad.Wrong (Errors.msg nonsenseState))
     935        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState))
    932936   | Csyntax.Sreturn a_opt ->
    933937     (match a_opt with
     
    938942             (Values.Vundef, (Csem.call_cont k),
    939943             (GenMem.free_list m (Csem.blocks_of_env e1)))) }
    940          | Csyntax.Tint (x, x0) -> IOMonad.Wrong (Errors.msg returnMismatch)
    941          | Csyntax.Tpointer x -> IOMonad.Wrong (Errors.msg returnMismatch)
     944         | Csyntax.Tint (x, x0) ->
     945           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
     946         | Csyntax.Tpointer x ->
     947           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
    942948         | Csyntax.Tarray (x, x0) ->
    943            IOMonad.Wrong (Errors.msg returnMismatch)
     949           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
    944950         | Csyntax.Tfunction (x, x0) ->
    945            IOMonad.Wrong (Errors.msg returnMismatch)
     951           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
    946952         | Csyntax.Tstruct (x, x0) ->
    947            IOMonad.Wrong (Errors.msg returnMismatch)
     953           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
    948954         | Csyntax.Tunion (x, x0) ->
    949            IOMonad.Wrong (Errors.msg returnMismatch)
    950          | Csyntax.Tcomp_ptr x -> IOMonad.Wrong (Errors.msg returnMismatch))
     955           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
     956         | Csyntax.Tcomp_ptr x ->
     957           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
    951958      | Types.Some a ->
    952959        (match TypeComparison.type_eq_dec f.Csyntax.fn_return Csyntax.Tvoid with
    953          | Types.Inl _ -> IOMonad.Wrong (Errors.msg returnMismatch)
     960         | Types.Inl _ ->
     961           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
    954962         | Types.Inr _ ->
    955963           Obj.magic
     
    968976         match v with
    969977         | Values.Vundef ->
    970            Obj.magic (IOMonad.Wrong (Errors.msg TypeComparison.typeMismatch))
     978           Obj.magic (IOMonad.Wrong (Errors.msg ErrorMessages.TypeMismatch))
    971979         | Values.Vint (sz, n) ->
    972980           (match Csyntax.typeof a with
    973981            | Csyntax.Tvoid ->
    974982              Obj.magic (IOMonad.Wrong
    975                 (Errors.msg TypeComparison.typeMismatch))
     983                (Errors.msg ErrorMessages.TypeMismatch))
    976984            | Csyntax.Tint (sz', x) ->
    977985              (match TypeComparison.sz_eq_dec sz sz' with
     
    980988                   (Obj.magic
    981989                     (IOMonad.opt_to_io
    982                        (Errors.msg TypeComparison.typeMismatch)
     990                       (Errors.msg ErrorMessages.TypeMismatch)
    983991                       (Csem.select_switch sz n sl))) (fun sl' ->
    984992                   Obj.magic
     
    988996               | Types.Inr _ ->
    989997                 Obj.magic (IOMonad.Wrong
    990                    (Errors.msg TypeComparison.typeMismatch)))
     998                   (Errors.msg ErrorMessages.TypeMismatch)))
    991999            | Csyntax.Tpointer x ->
    9921000              Obj.magic (IOMonad.Wrong
    993                 (Errors.msg TypeComparison.typeMismatch))
     1001                (Errors.msg ErrorMessages.TypeMismatch))
    9941002            | Csyntax.Tarray (x, x0) ->
    9951003              Obj.magic (IOMonad.Wrong
    996                 (Errors.msg TypeComparison.typeMismatch))
     1004                (Errors.msg ErrorMessages.TypeMismatch))
    9971005            | Csyntax.Tfunction (x, x0) ->
    9981006              Obj.magic (IOMonad.Wrong
    999                 (Errors.msg TypeComparison.typeMismatch))
     1007                (Errors.msg ErrorMessages.TypeMismatch))
    10001008            | Csyntax.Tstruct (x, x0) ->
    10011009              Obj.magic (IOMonad.Wrong
    1002                 (Errors.msg TypeComparison.typeMismatch))
     1010                (Errors.msg ErrorMessages.TypeMismatch))
    10031011            | Csyntax.Tunion (x, x0) ->
    10041012              Obj.magic (IOMonad.Wrong
    1005                 (Errors.msg TypeComparison.typeMismatch))
     1013                (Errors.msg ErrorMessages.TypeMismatch))
    10061014            | Csyntax.Tcomp_ptr x ->
    10071015              Obj.magic (IOMonad.Wrong
    1008                 (Errors.msg TypeComparison.typeMismatch)))
     1016                (Errors.msg ErrorMessages.TypeMismatch)))
    10091017         | Values.Vnull ->
    1010            Obj.magic (IOMonad.Wrong (Errors.msg TypeComparison.typeMismatch))
     1018           Obj.magic (IOMonad.Wrong (Errors.msg ErrorMessages.TypeMismatch))
    10111019         | Values.Vptr x ->
    1012            Obj.magic (IOMonad.Wrong (Errors.msg TypeComparison.typeMismatch))))
     1020           Obj.magic (IOMonad.Wrong (Errors.msg ErrorMessages.TypeMismatch))))
    10131021   | Csyntax.Slabel (lbl, s') ->
    10141022     IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s', k, e1,
     
    10171025     (match Csem.find_label lbl f.Csyntax.fn_body (Csem.call_cont k) with
    10181026      | Types.None ->
    1019         IOMonad.Wrong (List.Cons ((Errors.MSG unknownLabel), (List.Cons
    1020           ((Errors.CTX (AST.symbolTag, lbl)), List.Nil))))
     1027        IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.UnknownLabel),
     1028          (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, lbl)),
     1029          List.Nil))))
    10211030      | Types.Some sk' ->
    10221031        let { Types.fst = s'; Types.snd = k' } = sk' in
     
    10711080   | Csem.Kstop ->
    10721081     (match res1 with
    1073       | Values.Vundef -> IOMonad.Wrong (Errors.msg returnMismatch)
     1082      | Values.Vundef ->
     1083        IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
    10741084      | Values.Vint (sz, r) ->
    10751085        (match sz with
    1076          | AST.I8 -> (fun x -> IOMonad.Wrong (Errors.msg returnMismatch))
    1077          | AST.I16 -> (fun x -> IOMonad.Wrong (Errors.msg returnMismatch))
     1086         | AST.I8 ->
     1087           (fun x -> IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
     1088         | AST.I16 ->
     1089           (fun x -> IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
    10781090         | AST.I32 ->
    10791091           (fun r5 ->
    10801092             IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Finalstate
    10811093               r5) })) r
    1082       | Values.Vnull -> IOMonad.Wrong (Errors.msg returnMismatch)
    1083       | Values.Vptr x -> IOMonad.Wrong (Errors.msg returnMismatch))
    1084    | Csem.Kseq (x, x0) -> IOMonad.Wrong (Errors.msg nonsenseState)
    1085    | Csem.Kwhile (x, x0, x1) -> IOMonad.Wrong (Errors.msg nonsenseState)
    1086    | Csem.Kdowhile (x, x0, x1) -> IOMonad.Wrong (Errors.msg nonsenseState)
    1087    | Csem.Kfor2 (x, x0, x1, x2) -> IOMonad.Wrong (Errors.msg nonsenseState)
    1088    | Csem.Kfor3 (x, x0, x1, x2) -> IOMonad.Wrong (Errors.msg nonsenseState)
    1089    | Csem.Kswitch x -> IOMonad.Wrong (Errors.msg nonsenseState)
     1094      | Values.Vnull ->
     1095        IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
     1096      | Values.Vptr x ->
     1097        IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
     1098   | Csem.Kseq (x, x0) ->
     1099     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     1100   | Csem.Kwhile (x, x0, x1) ->
     1101     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     1102   | Csem.Kdowhile (x, x0, x1) ->
     1103     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     1104   | Csem.Kfor2 (x, x0, x1, x2) ->
     1105     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     1106   | Csem.Kfor3 (x, x0, x1, x2) ->
     1107     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     1108   | Csem.Kswitch x -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    10901109   | Csem.Kcall (r, f, e1, k') ->
    10911110     (match r with
     
    10981117          (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    10991118            (Obj.magic
    1100               (IOMonad.opt_to_io (Errors.msg failedStore)
     1119              (IOMonad.opt_to_io (Errors.msg ErrorMessages.FailedStore)
    11011120                (store_value_of_type' ty m l res1))) (fun m' ->
    11021121            Obj.magic
    11031122              (IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    11041123                Csyntax.Sskip, k', e1, m')) })))))
    1105 | Csem.Finalstate r -> IOMonad.Wrong (Errors.msg nonsenseState)
    1106 
    1107 (** val mainMissing : String.string **)
    1108 let mainMissing = "main missing"
    1109   (*failwith "AXIOM TO BE REALIZED"*)
     1124| Csem.Finalstate r -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    11101125
    11111126(** val make_global0 : Csyntax.clight_program -> Csem.genv0 **)
     
    11221137      Monad.m_bind0 (Monad.max_def Errors.res0)
    11231138        (Obj.magic
    1124           (Errors.opt_to_res (Errors.msg mainMissing)
     1139          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    11251140            (Globalenvs.find_symbol ge0 p.AST.prog_main))) (fun b ->
    11261141        Monad.m_bind0 (Monad.max_def Errors.res0)
    11271142          (Obj.magic
    1128             (Errors.opt_to_res (Errors.msg mainMissing)
     1143            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    11291144              (Globalenvs.find_funct_ptr ge0 b))) (fun f ->
    11301145          Obj.magic (Errors.OK (Csem.Callstate (f, List.Nil, Csem.Kstop,
Note: See TracChangeset for help on using the changeset viewer.