ITADN

Tutorial `signs.ml`: More robust testing

#2013OpenAng9876 创建于 2026-04-30
A
Ang9876commented
The tutorial [signs.ml](src/analyses/tutorials/signs.ml) is broken because the following [`eval` code](https://github.com/goblint/analyzer/blob/b0c1a3280ceeb613fab44f9f74fec8ad7ef5e067/src/analyses/tutorials/signs.ml#L61) does not handle the negative number properly (caused by the [change](https://github.com/goblint/cil/pull/216) in CIL). ``` ocaml let eval (d: D.t) (exp: exp): SL.t = match exp with | Const (CInt (i, _, _)) -> SL.top () (* TODO: Fix me! *) | Lval (Var x, NoOffset) -> D.find x d | _ -> SL.top () ``` Negative numbers are always evaluated to `SL.top()` through the last branch.
4 条评论