Ignore:
Timestamp:
Mar 29, 2013, 6:38:26 PM (7 years ago)
Author:
sacerdot
Message:

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/costCheck.ml

    r3001 r3043  
    216216    | AST.Internal fn0 ->
    217217      Bool.andb (check_well_cost_fn fn0) (check_sound_cost_fn fn0)
    218     | AST.External x -> Bool.True) (AST.prog_funct p)
    219 
     218    | AST.External x -> Bool.True) p.AST.prog_funct
     219
     220(** val check_cost_program_prf :
     221    RTLabs_syntax.rTLabs_program -> __ Errors.res **)
     222let check_cost_program_prf p =
     223  (match check_cost_program p with
     224   | Bool.True -> (fun _ -> Errors.OK __)
     225   | Bool.False ->
     226     (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadCostLabelling))) __
     227
Note: See TracChangeset for help on using the changeset viewer.