Ignore:
Timestamp:
Sep 16, 2011, 6:39:05 PM (8 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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.