Tutorial `signs.ml`: More robust testing

[Ang9876]

The tutorial signs.ml is broken because the following eval code does not handle the negative number properly (caused by the change in CIL).

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.

[michael-schwarz]

Thanks for the report!

Beyond the immediate fix, we should think about how to prevent our tutorial analysis silently breaking again:

• My first thought would be to commit the solution also (signsSolution.ml) and then duplicating the tests so they are also run with the solution. The downside is that then anyone can look at solution (do we care, or is that the student's problem if they peek).
• Alternatively we could supply the solution as a patch only and then have a regression test that uses the patched version and remove the SKIP. The problem with that is as soon as someone does the tutorial, the patch will no longer apply cleanly, leading to confusing error messages even if there is no actual problem.

I'm leaning towards the first. Any thoughts @sim642 @karoliineh @vesalvojdani @DrMichaelPetter @arkocal ?

[sim642]

Having to duplicate the tests is a bit annoying. I think @vesalvojdani has an intern working on the testing half of GobExec but I don't know about the progress or if goblint/GobExec#7 is on the agenda.

I think it'd be fine to have the solution also committed somewhere. Perhaps not immediately next to the template but into a subdirectory or a sibling directory to slightly reduce the temptation.
I have been using the signs tutorial as a possible homework in a course but if we commit the solution I should probably stop offering it as a graded thing.

[michael-schwarz]

I have been using the signs tutorial as a possible homework in a course but if we commit the solution I should probably stop offering it as a graded thing.

We could also try something like having the sample solution as a Github secret and then having a test that replaces the analysis file with the secret? I think offering a graded homework is nice, maybe we can find a way to keep this option.

[michael-schwarz]

The testing aspect of this still remains open.