|
Last change
on this file since 1383 was
1383,
checked in by sacerdot, 9 years ago
|
|
Potential bug fixed and bug found: the way pointers and labels are put in
bijection must be different between LIN and graph-like languages (bug fixed).
Moreover, in both cases it must be possible to retrieve the function from the
address and the easiest (only?) way to do that is to use the block of the
address to store the block of the function, and put the offsets in bijection
with labels/offsets, preventing pointer mangling since the pointer is in
the Code region (found, to be fixed).
|
|
File size:
734 bytes
|
| Line | |
|---|
| 1 | include "LIN/joint_LTL_LIN_semantics.ma". |
|---|
| 2 | include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *) |
|---|
| 3 | |
|---|
| 4 | definition lin_succ_pc: unit → address → res address := |
|---|
| 5 | λ_.λaddr. addr_add addr 1. |
|---|
| 6 | |
|---|
| 7 | axiom lin_pointer_of_label: label → Σp:pointer. ptype p = Code. |
|---|
| 8 | |
|---|
| 9 | axiom NotFound: String. |
|---|
| 10 | axiom lin_fetch_statement: |
|---|
| 11 | ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc lin_pointer_of_label) → res (pre_lin_statement globals).(* ≝ |
|---|
| 12 | λglobals,ge,st. |
|---|
| 13 | let pc ≝ pc … st in |
|---|
| 14 | ?. |
|---|
| 15 | let fn ≝ ? in |
|---|
| 16 | opt_to_res ? [MSG NotFound] (lookup … (lin_params …) (joint_if_code … fn) ?(*label???*)). |
|---|
| 17 | *) |
|---|
| 18 | |
|---|
| 19 | definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc lin_pointer_of_label … lin_fetch_statement. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
