lustrec/src/backends/Horn/horn_backend_collecting_sem.mli @ a7062da6
1 |
open Utils |
---|---|
2 |
open Machine_code_types |
3 |
|
4 |
val cex_computation: machine_t list -> Format.formatter -> ident -> machine_t -> unit |
5 |
val get_cex: machine_t list -> Format.formatter -> machine_t -> unit |
6 |
val collecting_semantics: machine_t list -> Format.formatter -> ident -> machine_t -> unit |
7 |
val check_prop: machine_t list -> Format.formatter -> machine_t -> unit |