diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/abstract_linker_script.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/abstract_linker_script.ml | 59 |
1 files changed, 0 insertions, 59 deletions
diff --git a/lib/ocaml_rts/linksem/abstract_linker_script.ml b/lib/ocaml_rts/linksem/abstract_linker_script.ml deleted file mode 100644 index 547b3b2d..00000000 --- a/lib/ocaml_rts/linksem/abstract_linker_script.ml +++ /dev/null @@ -1,59 +0,0 @@ -(*Generated by Lem from abstract_linker_script.lem.*) -open Lem_basic_classes -open Lem_list -open Lem_num - -type binary_relation - = Eq0 - | Lt0 - -type binary_connective - = And0 (** Conjunction *) - | Or0 (** Disjunction *) - -(** The type [expression] denotes addresses, whether known or to be ascertained. - *) -type expression - = Var0 of string (** Ranges over memory addresses *) - | Const of Nat_big_num.num (** Fixed memory address *) - -(* These are *one-place* predicates on unsigned integer solutions (usually representing - * addresses). Implicitly, every binary relation is being applied to the solution. HMM: is - * this sane? Taking my lead from KLEE / SMT solver formulae. What we're describing is a - * big SMT instance; it's sane if we can always factor the instances we want into this - * form, i.e. into a big conjunction of per-variable formulae where each two-place relation - * has the variable in one of its places. - * - * Could try to claim it follows from taking CNF and assigning - * each conjunct to one of the variables it contains. But what if that conjunct is a big - * disjunction including some other binary operators applied to two other variables? - * Might need to factor those out into a "global" extra conjunct. YES. *) -type value_formula - = VFTrue - | VFFalse - | VFBinaryRelation of (binary_relation * expression) - | VFBinaryConnective of (binary_connective * value_formula * value_formula) - | VFNot of value_formula - -type memory_image_formula - = MIFTrue - | MIFFalse - | MIFExists of (string * memory_image_formula) - | MIFBinaryRelation of (binary_relation * expression * expression) - | MIFBinaryConnective of (binary_connective * memory_image_formula * memory_image_formula) - | MIFAssertValueFormula of (expression * value_formula) - | MIFNot of memory_image_formula - -type memory_image0 - = MemoryImage of memory_image_formula - -(*val mk_range : natural -> natural -> value_formula*) -let rec mk_range left right:value_formula= - (if Nat_big_num.equal left right then - VFTrue - else if Nat_big_num.less right left then - VFFalse - else - let l = (Const left) in - let r = (Const right) in - VFBinaryConnective(And0, VFBinaryRelation(Lt0, r), VFNot(VFBinaryRelation(Lt0, l)))) |