diff options
Diffstat (limited to 'src/rewrites.ml')
| -rw-r--r-- | src/rewrites.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index a28352f5..87baa746 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -328,6 +328,7 @@ let rewrite_sizeof (Defs defs) = { e_block = (fun es -> let (es, es') = List.split es in (E_block es, E_block es')) ; e_nondet = (fun es -> let (es, es') = List.split es in (E_nondet es, E_nondet es')) ; e_id = (fun id -> (E_id id, E_id id)) + ; e_ref = (fun id -> (E_ref id, E_ref id)) ; e_lit = (fun lit -> (E_lit lit, E_lit lit)) ; e_cast = (fun (typ,(e,e')) -> (E_cast (typ,e), E_cast (typ,e'))) ; e_app = (fun (id,es) -> let (es, es') = List.split es in (E_app (id,es), E_app (id,es'))) @@ -368,6 +369,7 @@ let rewrite_sizeof (Defs defs) = ; e_internal_value = (fun v -> (E_internal_value v, E_internal_value v)) ; e_aux = (fun ((e,e'),annot) -> (E_aux (e,annot), E_aux (e',annot))) ; lEXP_id = (fun id -> (LEXP_id id, LEXP_id id)) + ; lEXP_deref = (fun (e, e') -> (LEXP_deref e, LEXP_deref e')) ; lEXP_memory = (fun (id,es) -> let (es, es') = List.split es in (LEXP_memory (id,es), LEXP_memory (id,es'))) ; lEXP_cast = (fun (typ,id) -> (LEXP_cast (typ,id), LEXP_cast (typ,id))) ; lEXP_tup = (fun tups -> let (tups,tups') = List.split tups in (LEXP_tup tups, LEXP_tup tups')) @@ -2955,6 +2957,12 @@ let rewrite_defs_ocaml = [ (* ("separate_numbs", rewrite_defs_separate_numbs) *) ] +let rewrite_defs_interpreter = [ + ("constraint", rewrite_constraint); + ("trivial_sizeof", rewrite_trivial_sizeof); + ("sizeof", rewrite_sizeof); + ] + let rewrite_defs_sil = [ ("top_sort_defs", top_sort_defs); ("tuple_vector_assignments", rewrite_tuple_vector_assignments); |