Skip to content

Generalize global constraint variables to module V: Printable.S in each analysis #473

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

Merged
merged 44 commits into from
Dec 6, 2021
Merged

Generalize global constraint variables to module V: Printable.S in each analysis #473

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
44 commits
Select commit Hold shift + click to select a range
09ff824
Add V module to Spec for global constraint variables (issue #469)
sim642 Dec 1, 2021
8b03bf4
Add 'v type parameter to ctx for global constraint variables (issue #…
sim642 Dec 1, 2021
0346c9e
Remove unused Basetype.Variables.loopSep
sim642 Dec 1, 2021
f338cf6
Use 'v type parameter in ctx operations for global constraint variabl…
sim642 Dec 1, 2021
8003376
Fix V equal and compare in MCP2 using DomVariantPrintable (issue #469)
sim642 Dec 1, 2021
e8bc4dd
Add return signatures to DomainListPrintableSpec functors
sim642 Dec 1, 2021
e9f8bbd
Refactor DomVariantPrintable
sim642 Dec 1, 2021
a1746df
Add DomVariantLattice for MCP2.G to avoid excessive bottom values
sim642 Dec 1, 2021
6b1f904
Update g2html for generalized globals
sim642 Dec 1, 2021
2a93f21
Use thread ID instead of varinfo for thread analysis globals
sim642 Dec 1, 2021
3824f9c
Use thread ID instead of varinfo for threadJoins analysis globals
sim642 Dec 1, 2021
2d596a0
Use named unit instead of varinfo for arinc analysis globals
sim642 Dec 1, 2021
e356ab2
Use named unit instead of varinfo for extract_arinc analysis globals
sim642 Dec 1, 2021
f1c7ef4
Remove unused open List in MCP
sim642 Dec 1, 2021
2519dd1
Use empty type for Analyses.DefaultSpec.V
sim642 Dec 1, 2021
7e71713
Clean up old GVar code
sim642 Dec 1, 2021
c5e84c6
Merge branch 'master' into general-globals
sim642 Dec 1, 2021
d173e14
Use named unit instead of varinfo for region analysis globals
sim642 Dec 1, 2021
e664d94
Fix Gobview compilation with general globals
sim642 Dec 1, 2021
a860fdb
Use default unit lattice for globals in analyses without global varia…
sim642 Dec 2, 2021
a0dee0a
Extend global variable module to BasePriv
sim642 Dec 2, 2021
0091038
Refactor ProtectionBasedPriv globals
sim642 Dec 2, 2021
00c36ff
Add base test requiring sides-pp
sim642 Dec 2, 2021
39fbd0b
Make unprotected and protected protection globals distinguishable in …
sim642 Dec 3, 2021
5c6239b
Extend global variable module to ApronPriv
sim642 Dec 3, 2021
644f96d
Make dune output original paths for copied alternative modules
sim642 Dec 3, 2021
8e75e26
Refactor Apron PerMutexMeetPrivTID globals
sim642 Dec 3, 2021
7e52f6c
Refactor per-mutex priv globals
sim642 Dec 3, 2021
0781828
Add mutex offsets to per-mutex priv globals
sim642 Dec 3, 2021
a84ee83
Inline CommonPriv.MutexGlobals
sim642 Dec 3, 2021
21464e3
Inline mutex_global and mutex_addr_to_varinfo
sim642 Dec 3, 2021
3ff0d05
Change lock-centered global domain from Prod to Lift2
sim642 Dec 3, 2021
45bf506
Use named unit instead of varinfo for Apron protection priv
sim642 Dec 3, 2021
e4e762c
Remove unused APRON_GLOBAL varinfos from Apron per-mutex privs
sim642 Dec 3, 2021
16f5ae4
Add MUTEX_INITS to per-mutex priv globals
sim642 Dec 3, 2021
fe883c5
Refactor Apron mutex-meet-tid with MutexGlobals.V
sim642 Dec 3, 2021
f0cafc7
Clean up Apron mutex-meet-tid global handling
sim642 Dec 3, 2021
7937179
Add thread return globals to base analysis
sim642 Dec 3, 2021
7223532
Use thread return globals directly in base
sim642 Dec 3, 2021
192ce50
Remove thread return syncs from base privs
sim642 Dec 3, 2021
abc9c1f
Remove now-unused to_varinfo from thread IDs
sim642 Dec 3, 2021
32b1fd5
Merge branch 'master' into general-globals
sim642 Dec 3, 2021
009b2b3
Fix LMust indentation in Apron mutex-meet-tid
sim642 Dec 3, 2021
3c9305f
Fix base Lift2 top in join from eval_exp
sim642 Dec 6, 2021
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 g2html
Open in desktop
Submodule g2html updated 1 files
+10 −9 resources/globals.xsl
2 changes: 1 addition & 1 deletion gobview
Open in desktop
Submodule gobview updated 1 files
+1 −1 src/state/gvGoblint.ml
2 changes: 2 additions & 0 deletions src/analyses/apron/apronAnalysis.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,10 @@ struct
module D = ApronComponents (AD) (Priv.D)
module G = Priv.G
module C = D
module V = Priv.V

open AD
open (ApronDomain: (sig module V: (module type of ApronDomain.V) end)) (* open only V from ApronDomain (to shadow V of Spec), but don't open D (to not shadow D here) *)

open ApronPrecCompareUtil
(* Result map used for comparison of results *)
Expand Down
Loading