Skip to content
Snippets Groups Projects
Forked from Prevosto Virgile / AnaStat-Frama-C-24-25
1 commit behind the upstream repository.
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({})