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

Convert library functions to new specifications #1079

Merged
merged 23 commits into from
Aug 3, 2023
Merged

Convert library functions to new specifications #1079

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
856dccb
Add fopencookie to libraryFunctions
karoliineh Jun 7, 2023
8753565
Remove functions already defined in libraries from invalidate_actions
karoliineh Jun 7, 2023
a0b3909
Add failwith to prevent goblint devs from adding functions already in…
karoliineh Jun 7, 2023
81db593
Convert all math.h functions to new specifications
karoliineh Jun 8, 2023
e94f1c4
Convert some __builtin functions to new specifications
karoliineh Jun 8, 2023
96a59cb
Convert most file-related functions to new specifications
karoliineh Jun 9, 2023
ce50eb4
Fix fprintf: add VarArgs
karoliineh Jun 9, 2023
c272f14
Mark and add thread-unsafe functions in libraryFunctions, relates to …
karoliineh Jun 9, 2023
a42b964
Convert all pthread functions to new specifications
karoliineh Jun 13, 2023
8c44ac7
Convert linux kernel functions from classify to new specifications
karoliineh Jun 13, 2023
2ef2e7f
Remove GetResource from libraryFunctions
karoliineh Jun 13, 2023
30d5aea
Convert most functions from classify to new specifications
karoliineh Jun 13, 2023
01ce504
Convert all __pthread functions to new specifications
karoliineh Jun 13, 2023
6a1445a
Convert some more lib-funs to new specifications
karoliineh Jun 16, 2023
2d56046
Convert memmove library functions. fixes #1121
karoliineh Jul 28, 2023
fe2cdff
Add missing argument to __builtin___memmove_chk
karoliineh Aug 1, 2023
1f53318
Apply suggestions from code review
karoliineh Aug 2, 2023
5c8bcfb
Implement comments from code review
karoliineh Aug 2, 2023
66ab9fb
Merge branch 'master' into libfuns-spec
karoliineh Aug 2, 2023
f2fd9b5
Update src/analyses/libraryFunctions.ml
karoliineh Aug 2, 2023
ab339c5
Move back accidentally moved library functions
sim642 Aug 3, 2023
2267095
Remove LibraryFunctions trailing whitespace, fix one VarArgs
sim642 Aug 3, 2023
ed231fa
Fix access analysis to not dereference non-pointer types
sim642 Aug 3, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/analyses/accessAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ struct
let access_one_top ?(force=false) ?(deref=false) ctx (kind: AccessKind.t) reach exp =
if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)\n" CilType.Exp.pretty exp AccessKind.pretty kind reach deref;
if force || !collect_local || !emit_single_threaded || ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) then (
if deref then
if deref && Cil.isPointerType (Cilfacade.typeOf exp) then (* avoid dereferencing integers to unknown pointers, which cause many spurious type-based accesses *)
do_access ctx kind reach exp;
if M.tracing then M.tracei "access" "distribute_access_exp\n";
Access.distribute_access_exp (do_access ctx Read false) exp;
Expand Down
Loading