Changeset 3043 for extracted/costInj.mli


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/costInj.mli

    r2951 r3043  
    116116  RTLabs_syntax.rTLabs_program -> Bool.bool
    117117
     118val check_program_cost_injectivity_prf :
     119  RTLabs_syntax.rTLabs_program -> __ Errors.res
     120
Note: See TracChangeset for help on using the changeset viewer.