Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndVal.ma

    r2176 r2286  
    3939qed.
    4040
    41 let rec check_be_ptr ptr n t on t ≝
     41(* let rec check_be_ptr ptr n t on t ≝
    4242match t with
    4343[ nil ⇒ eqb (size_pointer (*ptype ptr*)) n
     
    4747    | _ ⇒ false
    4848    ]
    49 ].
     49]. *)
    5050
    5151let rec check_be_null  n t on t ≝
     
    8787    match h with
    8888    [ BVundef ⇒ Vundef
     89    | BVnonzero ⇒ Vundef
    8990    | BVByte b ⇒ build_integer_val ty l
    90     | BVptr ptr pt ⇒ if eqb (part_no  pt) O ∧ check_be_ptr ptr (S O) t then Vptr ptr else Vundef
     91    | BVptr _ _ _ ⇒
     92      match pointer_of_bevals l with
     93      [ OK ptr ⇒ Vptr ptr
     94      | Error _ ⇒ Vundef
     95      ]
    9196    | BVnull  pt ⇒ if eqb (part_no  pt) O ∧ check_be_null  (S O) t then Vnull  else Vundef
    9297    ]
Note: See TracChangeset for help on using the changeset viewer.