资源描述：
《shape analysis with structural invariant checkers》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、ShapeAnalysiswithStructuralInvariantCheckersBor-YuhEvanChangXavierRivalGeorgeNeculaElectricalEngineeringandComputerSciencesUniversityofCaliforniaatBerkeleyTechnicalReportNo.UCB/EECS-2007-80http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-80.htmlJune4,2007Copyright©2007,bytheauthor(
2、s).Allrightsreserved.Permissiontomakedigitalorhardcopiesofallorpartofthisworkforpersonalorclassroomuseisgrantedwithoutfeeprovidedthatcopiesarenotmadeordistributedforprofitorcommercialadvantageandthatcopiesbearthisnoticeandthefullcitationonthefirstpage.Tocopyotherwise,torepublish,topostonser
3、versortoredistributetolists,requirespriorspecificpermission.AcknowledgementThisresearchwassupportedinpartbytheNationalScienceFoundationundergrantsCCR-0326577,CCF-0524784,andCNS-0509544;andanNSFGraduateResearchFellowship.Anyopinions,findings,conclusionsorrecommendationsexpressedinthismateria
4、larethoseoftheauthorsanddonotnecessarilyreflecttheviewsoftheNationalScienceFoundation.ShapeAnalysiswithStructuralInvariantCheckers?Bor-YuhEvanChang1,XavierRival1,2,andGeorgeC.Necula11UniversityofCalifornia,Berkeley,California,USA2EcoleNormaleSup´erieure,Paris,France´{bec,rival,necula}@cs.be
5、rkeley.eduAbstract.Developer-supplieddatastructurespecificationsareimpor-tanttoshapeanalyses,astheytelltheanalysiswhatinformationshouldbetrackedinordertoobtainthedesiredshapeinvariants.Weobservethatdatastructurecheckingcode(e.g.,usedintestingordynamicanal-ysis)providesshapeinformationthatcan
6、alsobeusedinstaticanalysis.Inthispaper,weproposealightweight,automaticshapeanalysisbasedonthesedeveloper-suppliedstructuralinvariantcheckers.Inparticular,wesetupaparametricabstractdomain,whichisinstantiatedwithsuchcheckerspecificationstosummarizememoryregionsusingbothnotionsofcompleteandpart
7、ialcheckerevaluations.Theanalysisthenautomati-callyderivesastrategyforcanonicalizingorweakeningshapeinvariants.1IntroductionPointermanipulationisfundamentalinalmostallsoftwaredevelopedinimpera-tiveprogramminglanguagestoday.Forthisreason,verifyingproperti
