Changeset 2967 for src


Ignore:
Timestamp:
Mar 26, 2013, 6:54:12 PM (7 years ago)
Author:
sacerdot
Message:

Semantics changed so that a terminating joint program that returns an undefined
value is recognized as a terminating program that returns a dummy integer
(the maximum allowed one). This because the front-end type for termination is
int option and it does not discriminate between "non final" and "final with
no value". How is that possible in the front-end?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2952 r2967  
    235235 if eq_program_counter (pc … st) exit_pc' then
    236236   let ret ≝ call_dest_for_main ?? p in
    237    res_to_opt … (! vals ← read_result … ge ret st ;
     237   match (! vals ← read_result … ge ret st ;
    238238               Word_of_list_beval vals)
     239   with
     240   [ OK v ⇒ Some ? v
     241   | Error _ ⇒ Some … (maximum ?) ]
    239242 else None ?.
    240243
Note: See TracChangeset for help on using the changeset viewer.