Changeset 2807


Ignore:
Timestamp:
Mar 7, 2013, 5:43:15 PM (7 years ago)
Author:
mckinna
Message:

Yet another ErrorMessage?
Removed corresponding axiom in ERTL/ERTL_semantics.ma

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r2801 r2807  
    112112  return set_regs ERTL_state env' st.
    113113
    114 axiom FunctionNotFound : errmsg.
    115 
    116114definition eval_ertl_seq:
    117115 ∀F. ∀globals. genv_gen F globals →
     
    119117   res (state ERTL_state) ≝
    120118 λF,globals,ge,stm,id,st.
    121  ! framesize ← opt_to_res … FunctionNotFound (stack_sizes … ge id);
     119 ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
    122120 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
    123121  match stm with
  • src/common/ErrorMessages.ma

    r2796 r2807  
    7575 | BlockInFramesCorrupted : ErrorMessage
    7676 | FrameErrorOnPush : ErrorMessage
    77  | FrameErrorOnPop : ErrorMessage.
     77 | FrameErrorOnPop : ErrorMessage
     78 | FunctionNotFound : ErrorMessage
     79 .
Note: See TracChangeset for help on using the changeset viewer.