Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Three incremental tests failing with the cfg comparison #835

Closed
3 tasks
stilscher opened this issue Sep 16, 2022 · 2 comments · Fixed by #841
Closed
3 tasks

Three incremental tests failing with the cfg comparison #835

stilscher opened this issue Sep 16, 2022 · 2 comments · Fixed by #841
Assignees
Labels
Milestone

Comments

@stilscher
Copy link
Member

stilscher commented Sep 16, 2022

Currently three incremental test cases fail when the cfg comparison is activated. The first two throw a Not_found exception, for the third the result is not as expected.

  • 03/02 reluctant-int-annotation
  • 03/03 reluctant-int-annotation-dyn
  • 13/05 race-call-remove

Since the cfg comparison often breaks when new features are introduced and the only the AST comparison is considered when adapting the incremental pre-processing for the solver, I would suggest to run the incremental tests also with the cfg comparison in the regular regression test runs.

Testing 03/02 precision-annotation/reluctant-int-annotation      Status: 2 (exception)

  - Timings:
  - TOTAL                           0.007 s
  -   parse                           0.002 s
  -   convert to CIL                  0.003 s
  -   mergeCIL                        0.002 s
  -   compareCilFiles                 0.001 s
  -     createCFG                       0.001 s
  -       handle                          0.001 s
  -       iter_connect                    0.001 s
  -         computeSCCs                     0.001 s

Testing 03/03 precision-annotation/reluctant-int-annotation-dyn  Status: 2 (exception)

  - Timings:
  - TOTAL                           0.008 s
  -   parse                           0.003 s
  -   convert to CIL                  0.003 s
  -   mergeCIL                        0.002 s
  -   compareCilFiles                 0.001 s
  -     createCFG                       0.001 s
  -       handle                          0.001 s
  -       iter_connect                    0.001 s
  -         computeSCCs                     0.001 s

03/02 failed!

Expected assert, but registered nothing on reluctant-int-annotation-dyn:10
  __goblint_check(in == 17);
Expected fail, but registered nothing on reluctant-int-annotation-dyn:21
  __goblint_check(a); // FAIL!
Expected assert, but registered nothing on reluctant-int-annotation-dyn:23
  __goblint_check(a == 17);
03/03 failed!

Expected norace, but registered race on race-call-remove:7
  g++; // NORACE (unique thread)
Expected norace, but registered race on race-call-remove:12
  g++; // NORACE
13/05 failed!

3 test(s) failed: ["03/02 reluctant-int-annotation", "03/03 reluctant-int-annotation-dyn", "13/05 race-call-remove"]
@stilscher stilscher self-assigned this Sep 16, 2022
@stilscher stilscher added the bug label Sep 16, 2022
@sim642
Copy link
Member

sim642 commented Sep 16, 2022

Some of the incremental tests might have been written in a way that assumes AST comparison: for example, a change being made to a function with the purpose of reanalyzing the entire function from scratch.

@stilscher
Copy link
Member Author

You could still achieve this by setting the configuration option force-reanalyze. I would find that more transparent because I think that there should not be any hidden assumption regarding the kind of comparison.

@stilscher stilscher linked a pull request Nov 15, 2022 that will close this issue
1 task
@sim642 sim642 added this to the v2.2.0 milestone Nov 25, 2022
sim642 added a commit to sim642/opam-repository that referenced this issue Sep 13, 2023
CHANGES:

* Add `setjmp`/`longjmp` analysis (goblint/analyzer#887, goblint/analyzer#970, goblint/analyzer#1015, goblint/analyzer#1019).
* Refactor race analysis to lazy distribution (goblint/analyzer#1084, goblint/analyzer#1089, goblint/analyzer#1136, goblint/analyzer#1016).
* Add thread-unsafe library function call analysis (goblint/analyzer#723, goblint/analyzer#1082).
* Add mutex type analysis and mutex API analysis (goblint/analyzer#800, goblint/analyzer#839, goblint/analyzer#1073).
* Add interval set domain and string literals domain (goblint/analyzer#901, goblint/analyzer#966, goblint/analyzer#994, goblint/analyzer#1048).
* Add affine equalities analysis (goblint/analyzer#592).
* Add use-after-free analysis (goblint/analyzer#1050, goblint/analyzer#1114).
* Add dead code elimination transformation (goblint/analyzer#850, goblint/analyzer#979).
* Add taint analysis for partial contexts (goblint/analyzer#553, goblint/analyzer#952).
* Add YAML witness validation via unassume (goblint/analyzer#796, goblint/analyzer#977, goblint/analyzer#1044, goblint/analyzer#1045, goblint/analyzer#1124).
* Add incremental analysis rename detection (goblint/analyzer#774, goblint/analyzer#777).
* Fix address sets unsoundness (goblint/analyzer#822, goblint/analyzer#967, goblint/analyzer#564, goblint/analyzer#1032, goblint/analyzer#998, goblint/analyzer#1031).
* Fix thread escape analysis unsoundness (goblint/analyzer#939, goblint/analyzer#984, goblint/analyzer#1074, goblint/analyzer#1078).
* Fix many incremental analysis issues (goblint/analyzer#627, goblint/analyzer#836, goblint/analyzer#835, goblint/analyzer#841, goblint/analyzer#932, goblint/analyzer#678, goblint/analyzer#942, goblint/analyzer#949, goblint/analyzer#950, goblint/analyzer#957, goblint/analyzer#955, goblint/analyzer#954, goblint/analyzer#960, goblint/analyzer#959, goblint/analyzer#1004, goblint/analyzer#558, goblint/analyzer#1010, goblint/analyzer#1091).
* Fix server mode for abstract debugging (goblint/analyzer#983, goblint/analyzer#990, goblint/analyzer#997, goblint/analyzer#1000, goblint/analyzer#1001, goblint/analyzer#1013, goblint/analyzer#1018, goblint/analyzer#1017, goblint/analyzer#1026, goblint/analyzer#1027).
* Add documentation for configuration JSON schema and OCaml API (goblint/analyzer#999, goblint/analyzer#1054, goblint/analyzer#1055, goblint/analyzer#1053).
* Add many library function specifications (goblint/analyzer#962, goblint/analyzer#996, goblint/analyzer#1028, goblint/analyzer#1079, goblint/analyzer#1121, goblint/analyzer#1135, goblint/analyzer#1138).
* Add OCaml 5.0 support (goblint/analyzer#1003, goblint/analyzer#945, goblint/analyzer#1162).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants