Revision 09bfc860
Added by Pierre-Loïc Garoche about 3 years ago
| src/tools/tiny/tiny_verifier.ml | ||
|---|---|---|
| 50 | 50 |
let m = Machine_code_common.get_machine machines node_name in |
| 51 | 51 |
let env = (* We add each variables of the node the Tiny env *) |
| 52 | 52 |
Tiny_utils.machine_to_env m in |
| 53 |
let nd = m.mname in
|
|
| 53 |
(*let nd = m.mname in*)
|
|
| 54 | 54 |
(* Building preamble with some bounds on inputs *) |
| 55 | 55 |
(* TODO: deal woth contracts, asserts, ... *) |
| 56 | 56 |
let bounds_inputs = [] in |
Also available in: Unified diff
Cleaning