Forked from
Prevosto Virgile / AnaStat-Frama-C-24-25
1 commit behind the upstream repository.
-
Virgile Prevosto authoredVirgile Prevosto authored
example_interval_eval_exp.py 957 B
from syntax import *
from interval_analysis import eval_aexp, eval_bexp, abstract_env, Interval
x: ArithExpr = AEVar("x")
y: ArithExpr = AEVar("y")
# x - y * (x / y)
test_aexp: ArithExpr = AEBop(Bop.ADD,x, AEUop(Uop.OPP,AEBop(Bop.MUL,y,AEBop(Bop.DIV,x,y))))
# ! (x - y <= y * (x - x/y))
test_bexp: BoolExpr = BENeg(BELeq(AEBop(Bop.ADD,x,AEUop(Uop.OPP,y)),test_aexp))
def test(env: abstract_env) -> None:
res_a = eval_aexp(env,test_aexp)
res_b = eval_bexp(env,test_bexp)
print(f'In environment { {var: str(i) for (var,i) in env.items()} }')
print(f"{test_aexp} -> {res_a}")
print(f"{test_bexp} -> {res_b}")
test({ 'x': Interval(20,20), 'y': Interval(2,2) })
test({ 'x': Interval(10,20), 'y': Interval(1,2) })
test({ 'x': Interval(-30,0), 'y': Interval(-10,0) })
test({ 'x': Interval(-20,20), 'y': Interval(0,0) })
test({ 'x': Interval(0,20), 'y': Interval(2,5) })
test({ 'x': Interval(-10,20), 'y': Interval(-5,-2) })
test({})