Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (9 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/Clight/CexecSound.ma

    r744 r797  
    6464        cases (try_cast_null m i (Tint sz1 si1) t);
    6565        [ 1,3,5: #v'' #H' #e @H' @e
    66         | *: #_ whd in ⊢ (??%? → ?); #H destruct (H);
     66        | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H);
    6767        ]
    6868    ]
     
    7474        cases (try_cast_null m i t ty');
    7575        [ 1,3,5: #v'' #H' #e @H' @e
    76         | *: #_ whd in ⊢ (??%? → ?); #H destruct (H);
     76        | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H);
    7777        ]
    7878  ]
     
    303303    lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer locr Tvoid)))
    304304    >H' #H'' @H''
    305 | #_ whd @I
     305| #msg #_ whd @I
    306306] qed.
    307307
     
    351351      @opt_bind_OK #m' #STORE
    352352      lapply (refl ? (exec_bind_parameters en m' ps' vs))
    353       cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %) [2: #_ %]
     353      cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %) [2: #msg #_ %]
    354354      #m'' #BIND
    355355      @(bind_parameters_cons … GET STORE)
     
    394394              [ % // | @(bool_of … Hb) ]
    395395            ]
    396         | #_ //;
     396        | #msg #_ //;
    397397        ]
    398398    | #ex #s1 #s2 #k' @step_skip_or_continue_for2 % //;
Note: See TracChangeset for help on using the changeset viewer.