Module TypedC.Pred

type unop =

1. | Extract of Units.In_bits.t * Units.In_bits.t
   (*

   start index, length

   *)

type binop =

1. | Add
2. | Sub
3. | Mul
4. | Div
5. | And
6. | Or
7. | Mod
8. | Concat of Units.In_bits.t * Units.In_bits.t
   (*

   Size 1, size 2. First argument is the most significant

   *)

type expr =

1. | Const of Z.t
2. | Val of value
3. | Self
4. | Unop of unop * expr
5. | Binop of binop * expr * expr

type cmpop =

1. | Equal
2. | NotEqual
3. | ULt
4. | SLt
5. | ULeq
6. | SLeq
7. | UGeq
8. | SGeq
9. | UGt
10. | SGt

type mutval = {

1. id : int;
2. mutable value : bool;

}

type t =

1. | True
2. | Cmp of cmpop * expr * expr
3. | And of t * t
4. | Mutval of mutval * t

Predicate on a structure field or array element, which is supposed to be true at all times.

val evaluate_mutval : mutval -> t -> t

given a mutval, evaluate the value of the associated predicate

val init_mutval : t -> t

val is_true : t -> bool

check if a predicate can be immediately reduced to true, this is not trivial since mutval exists

val true_ : t

returns the true predicate

val equal : t -> t -> bool

val pp_binop : Stdlib.Format.formatter -> binop -> unit

val pp_cmpop : Stdlib.Format.formatter -> cmpop -> unit

val pp : Stdlib.Format.formatter -> t -> unit

val array_length_to_expr : array_length -> expr

val conjunction : t -> t -> t

Conjoint two predicate. Ignores true (void) predicates