Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (10 years ago)
Author:
campbell
Message:

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r758 r797  
    483483(* init *)
    484484
     485axiom InitDataStoreFailed : String.
     486
    485487definition add_globals : ∀F,V:Type[0].
    486488       genv F × mem → list (ident × (list init_data) × region × V) →
     
    495497        match alloc_init_data st init r with [ pair st' b ⇒
    496498          let g' ≝ add_symbol ? id b g in
    497           do st'' ← opt_to_res ? (store_init_data_list F g' st' b OZ init);
     499          do st'' ← opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g' st' b OZ init);
    498500            OK ? 〈g', st''〉
    499501        ] ] ] ])
Note: See TracChangeset for help on using the changeset viewer.