Asllib.ASTUtilsSourceThis module provides some tools to work on ASL ASTs.
A dummy position.
annotated v start end is v with location specified as from start to end.
desc v is v.desc
Add a dummy location annotation to a value.
A dummy location
Removes the value from an annotated record.
add_pos_from_pos_of (__POS_OF__ e) is annotated s s' e where s and s' correspond to e's position in the ocaml file.
add_pos_from loc v is v with the location data from loc.
add_pos_from loc v is v with the location data from loc.
add_pos_from_st a' a is a with the location from a'.
If both arguments are physically equal, then the result is also physically equal.
val map2_desc :
('a AST.annotated -> 'b AST.annotated -> 'c) ->
'a AST.annotated ->
'b AST.annotated ->
'c AST.annotatedFolder on two annotated types.
integer, without the position annotation.
integer_exact e is the integer type constrained to be equal to e.
integer_exact' e is integer_exact e without the position annotation.
stmt_from_list [s1; ... sn] is s1; ... sn in ASL.
literal v is the expression evaluated to v.
var_ x is the expression x.
Builds a binary operation from to sub-expressions.
fresh_var "doc" is a fresh variable whose name begins with "doc".
Creates a fresh dummy variable for a global ignored variable.
is_global_ignored s is true iff s has been created with global_ignored ().
val constraint_binop :
AST.binop ->
AST.int_constraint list ->
AST.int_constraint list ->
AST.int_constraintsconstraint_binop PLUS cs1 cs2 is the set of constraints given by the element wise application of PLUS.
Builds a mask from specified positions.
Flip all the 0/1 in the mask. Doesn't change the 'x'.
slices_to_positions as_int slices evaluates slices and returns a list of all queried positions in the correct order.
Sorts the fields of a record to allow an element wise comparison.
Returns the name of the bitfield in question.
Returns the slices corresponding to this bitfield.
bitfield_find_opt name bfs is Some (bf) if there exists bf in bfs with name, None otherwise.
bitfields_find_slices_opt name bfs is Some (slices) if there exists a bitfield with name name and slices slices.
Most of those take a cmp_expr argument that is the static analyser expression comparison.
val constraints_equal :
(AST.expr -> AST.expr -> bool) ->
AST.int_constraint list ->
AST.int_constraint list ->
boolpatch ~src ~patches replaces in src the global identifiers defined by patches.
subst_expr substs e replaces the variables used inside e by their associated expression in substs, if any.
Warning: constants and statically-evaluated parts are not changed, for example: E_Slice (E_Var "y", [Slice_Single (E_Var "y")]) will become after subst_expr [("y", E_Var "x")]: E_Slice (E_Var "x", [Slice_Single (E_Var "y")])
rename_locals f ast is ast where all instances of variables x are replaced with f x.
is_simple_expr e is true if e does not contain any call to any other subprogram. It has false negative.
use_constant_decl d is the set of other declared names required to have in the environment to be able to type-check d.
identifier_of_decl d is the name of the global element defined by d.
pair a b is (a, b).
pair' b a is (b, a).
list_equal elt_equal li1 li2 is true iff li1 and li2 are element-wise equal.
An element wise comparaison for lists.
list_cross f [a1; ... an] [b1; ... bm] is the list of all f ai bj in a non-specified order.
list_concat_map f l gives the same result as List.concat (List.map f l). Tail-recursive. Taken from stdlib 4.10.
fold_left_map is a combination of fold_left and map that threads an accumulator through calls to f. Taken from stdlib 4.11.