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.

Sign up for GitHub

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

Jump to bottom

Convert library functions to new specifications #1079

Merged
merged 23 commits into from
Aug 3, 2023
Merged

Convert library functions to new specifications #1079

merged 23 commits into from
Aug 3, 2023

Conversation

karoliineh
Copy link
Member

Relates to #1029.

A contribution to the effort of converting all library functions to new specifications.

@karoliineh karoliineh self-assigned this Jun 7, 2023
@karoliineh
Copy link
Member Author

The following thread-unsafe functions remain to be added to libraryFunctions.ml:

  • ecvt()
  • ftw()
  • nftw()
  • setkey()
  • wcsrtombs()
  • wcstombs()
  • wctomb()

@karoliineh karoliineh mentioned this pull request Jun 9, 2023
Merged
@sim642 sim642 mentioned this pull request Jul 28, 2023
Closed
@sim642 sim642 linked an issue Jul 31, 2023 that may be closed by this pull request
Incorrect memmove library function specification #1121
Closed
@karoliineh karoliineh marked this pull request as ready for review August 1, 2023 13:11
sim642
sim642 requested changes Aug 2, 2023
View reviewed changes
Copy link
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Under "Files changed" you can add all suggestions to a batch to make a single commit instead of ~20 one liners.

src/analyses/libraryFunctions.ml Outdated Show resolved Hide resolved
src/analyses/libraryFunctions.ml Outdated Show resolved Hide resolved
src/analyses/libraryFunctions.ml Outdated Show resolved Hide resolved
src/analyses/libraryFunctions.ml Outdated Show resolved Hide resolved
src/analyses/libraryFunctions.ml Outdated Show resolved Hide resolved
src/analyses/libraryFunctions.ml Outdated Show resolved Hide resolved
src/analyses/libraryFunctions.ml Outdated Show resolved Hide resolved
src/analyses/libraryFunctions.ml Outdated Show resolved Hide resolved
src/analyses/libraryFunctions.ml Outdated Show resolved Hide resolved
src/analyses/libraryFunctions.ml Outdated Show resolved Hide resolved
@sim642 sim642 mentioned this pull request Jun 9, 2023
Closed
7 tasks
@sim642 sim642 added this to the v2.2.0 milestone Aug 3, 2023
@sim642 sim642 merged commit babc881 into master Aug 3, 2023
@sim642 sim642 deleted the libfuns-spec branch August 3, 2023 12:14
@sim642 sim642 mentioned this pull request Sep 13, 2023
Closed
sim642 added a commit to sim642/opam-repository that referenced this pull request Sep 13, 2023
@sim642
[new release] goblint (2.2.0)
eb80bce 
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
Reviewers

@sim642 sim642 sim642 approved these changes

Assignees

@karoliineh karoliineh

Labels
benchmarking cleanup Refactoring, clean-up precision
Projects
None yet
Milestone
v2.2.0
Development

Successfully merging this pull request may close these issues.

Incorrect memmove library function specification
2 participants
@karoliineh @sim642