Changeset 2946 for src/ERTLptr/ERTLptr_semantics.ma

Timestamp:

Mar 24, 2013, 11:29:01 AM (8 years ago)

Author:

tranquil

Message:

main novelties:

• there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
• a premain is added semantically to the global env, so initial cost label and main call and return are observed
• proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File:

• src/ERTLptr/ERTLptr_semantics.ma (modified) (1 diff)

src/ERTLptr/ERTLptr_semantics.ma

@@ -60 +60 @@
   
 definition ERTLptr_semantics ≝
-  mk_sem_graph_params ERTLptr ERTLptr_sem_uns.
+  mk_sem_graph_params ERTLptr ERTLptr_sem_uns ERTLptr_premain.