Changeset 797 for src/Cminor/test


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/Cminor/test/sum-bad.ma

    r761 r797  
    7272.
    7373
    74 example exec: exec_up_to Cminor_fullexec myprog 1000 [ ] = Error ?.
    75 normalize  (* you can examine the result here *)
    76 @refl
     74example exec: exec_up_to Cminor_fullexec myprog 1000 [ ] = Error ??.
     75[normalize  (* you can examine the result here *)
     76 @refl
     77|skip
     78]
    7779qed.
    7880
    7981include "Cminor/initialisation.ma".
    8082
    81 example exec2: exec_up_to Cminor_fullexec (replace_init myprog) 1000 [ ] = Error ?.
    82 normalize  (* you can examine the result here *)
    83 @refl
     83example exec2: exec_up_to Cminor_fullexec (replace_init myprog) 1000 [ ] = Error ??.
     84[normalize  (* you can examine the result here *)
     85 @refl
     86|skip
     87]
    8488qed.
Note: See TracChangeset for help on using the changeset viewer.