package mopsa
Module Common.Quantified_offset
val bound :
MopsaLib.expr ->
(Stubs.Ast.quant * MopsaLib.var * Stubs.Ast.set) list ->
MopsaLib.expr * MopsaLib.exprCompute symbolic boundaries of a quantified offset.
val is_aligned :
MopsaLib.expr ->
Z.t ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
boolis_aligned o n man flow checks whether the value of an expression o is aligned w.r.t. size sz
val bound_div :
MopsaLib.expr ->
Z.t ->
(Stubs.Ast.quant * MopsaLib.var * Stubs.Ast.set) list ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
(MopsaLib.expr * MopsaLib.expr) Mopsa_utils.Core.Top.with_topCompute symbolic boundaries of offset / den