Changeset 1224 for src/Clight


Ignore:
Timestamp:
Sep 16, 2011, 6:39:05 PM (9 years ago)
Author:
sacerdot
Message:

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

Location:
src/Clight
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r1139 r1224  
    540540@opt_bind_OK #x cases x; #sp #b #esb
    541541@opt_bind_OK #f #ef
    542 whd; % [ whd in ⊢ (???(??%)) // | @(initial_state_intro … Ege Em esb ef) ]
     542whd; % [ whd in ⊢ (???(??%)) @Ege | @(initial_state_intro … Ege Em esb ef) ]
    543543qed.
    544544
  • src/Clight/Csyntax.ma

    r1139 r1224  
    318318  data.  See module [AST] for more details. *)
    319319
    320 definition clight_program : Type[0] ≝ program clight_fundef (list init_data × type).
     320definition clight_program : Type[0] ≝ program (λ_.clight_fundef) (list init_data × type).
    321321
    322322(* * * Operations over types *)
  • src/Clight/SimplifyCasts.ma

    r1198 r1224  
    194194
    195195definition simplify_program : clight_program → clight_program ≝
    196 transform_program ??? simplify_fundef.
     196λp. transform_program … p simplify_fundef.
  • src/Clight/label.ma

    r1056 r1224  
    187187
    188188definition clight_label : clight_program → res clight_program ≝
    189   transform_partial_program ??? label_fundef.
     189 λp. transform_partial_program … p label_fundef.
  • src/Clight/test/search.c.ma

    r1139 r1224  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef ((list init_data) × type)
     4definition myprog := mk_program (λ_.clight_fundef) ((list init_data) × type)
     5  []
    56  [〈ident_of_nat 0 (* search *), CL_Internal (
    67     mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
     
    181182  )〉]
    182183  (ident_of_nat 7)
    183   []
    184184.
    185185
  • src/Clight/toCminor.ma

    r1207 r1224  
    691691  let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
    692692  let globals ≝ fun_globals @ var_globals in
    693   transform_partial_program2 ???? (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)) p.
     693  transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)).
Note: See TracChangeset for help on using the changeset viewer.