Ignore:
Timestamp:
Oct 17, 2011, 5:41:44 PM (8 years ago)
Author:
sacerdot
Message:

1) New versions of pointer_of_beval/beval_of_pointer with a stricter dependent

type. They allow to close several proof obligations.

2) Globalenvs no longer uses -1 as a valid function block. It starts with -2
3) joint/semantics.ma uses a -2 block for the fake address used to signal the

end of program execution. Differently from what happens in OCaml, the block
is not allocated.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1385 r1395  
    4545
    4646(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
    47   Maybe there is a better way to organize the code!!! *)
    48 definition graph_succ_p: label → address → res address.
    49  #l #_ generalize in match (refl … (address_of_pointer (pointer_of_label l)))
    50  cases (address_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
    51   [ #res #_ @(OK … res)
    52   | #msg cases (pointer_of_label l) * * #q #com #off #E1 destruct #E2 normalize in E2; destruct ]
    53 qed.
     47 But I can't use it directly because this one uses a concrete definition of
     48 pointer_of_label and it is used to istantiate the more_sem_params record
     49 where the abstract version is declared as a field. Is there a better way
     50 to organize the code? *)
     51definition graph_succ_p: label → address → res address ≝
     52 λl.λ_.address_of_pointer (pointer_of_label l).
    5453
    5554axiom BadProgramCounter: String.
     
    6059   state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝
    6160 λparams1,sem_params,globals,ge,st.
    62   do p ← pointer_of_address (pc … st) ;
     61  do p ← code_pointer_of_address (pc … st) ;
    6362  let b ≝ pblock p in
    6463  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     
    7271   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
    7372 λparams1,sem_params,globals,ge,st.
    74   do p ← pointer_of_address (pc … st) ;
     73  do p ← code_pointer_of_address (pc … st) ;
    7574  do f ← graph_fetch_function … ge st ;
    7675  do l ← label_of_pointer p;
Note: See TracChangeset for help on using the changeset viewer.