Revision 3e209698
Added by Pierre-Loïc Garoche almost 9 years ago
| src/main_lustre_compiler.ml | ||
|---|---|---|
| 255 | 255 |
Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*) |
| 256 | 256 |
end |
| 257 | 257 |
| "horn" -> begin |
| 258 |
let fmt = Format.std_formatter in |
|
| 258 |
let source_file = basename ^ ".smt2" in (* Could be changed *) |
|
| 259 |
let source_out = open_out source_file in |
|
| 260 |
let fmt = formatter_of_out_channel source_out in |
|
| 259 | 261 |
Horn_backend.translate fmt basename normalized_prog machine_code |
| 260 | 262 |
end |
| 261 | 263 |
| _ -> assert false |
Also available in: Unified diff
First fully working version of horn backend.
Has to be called with "-horn -node main_node"
The test script compute the smt2 file and calls z3 on them.