Changeset 1515 for src/Clight/test/insertsort.test.ma

Timestamp:

Nov 18, 2011, 1:03:14 PM (9 years ago)

Author:

campbell

Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

• fix interpretation for - on positives
• move eq_nat_dec to a more appropriate place
• split out costs from other identifiers in ASM
• use identifier abstractions in back-end

File:

• src/Clight/test/insertsort.test.ma (modified) (1 diff)

src/Clight/test/insertsort.test.ma

@@ -26 +26 @@
 
 example labelled_exec: 
-  (do p ← clight_label myprog;
+  (let p ≝ clight_label myprog in
    do s ← exec_up_to clight_fullexec p 1000
      [EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0)];