Changeset 1515 for src/Clight/test


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (8 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/insertsort.test.ma

    r1513 r1515  
    2626
    2727example labelled_exec:
    28   (do p ← clight_label myprog;
     28  (let p ≝ clight_label myprog in
    2929   do s ← exec_up_to clight_fullexec p 1000
    3030     [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)];
Note: See TracChangeset for help on using the changeset viewer.