F. Model checking software at compile time(10)

4.3PropertyImplementationinGoanna

4.2ModelCheckingwithNuSMV

PartsoftheNuSMVcoderesultingfromthetranslationofthelabelledCFGareshowninFigure4.AsdescribedinSection3.3weintroduceoneenumeratedtypevariable,i.e.,location,rangingoverthecontrollocations(i.e.thenodesintheCFG),describethetransitionrelationasasetoftransitionsfromlocationstoasetoflocations,anduseDEFINEdeclarationstoassociatelabelstocertainloca-tions.Notethat,forclarityofpresentation,weusetheweakuntiloperandWintheCTLspeci cation,whichdoesnotex-istinNuSMVsyntax,butcanbeequallyexpressedthroughotherexistingoperators.

UsingNuSMVforcheckingproperty(1)(describedinSection3.1)ontheannotatedCFGnowrevealsaviolationoftheNuSMVspeci cationfromFigure4.GoannaautomaticallyexaminestheviolationreportedbyNuSMVandconcludesthatthereisanincorrectuseofvariablea—infact,thereisapathintheprogram

6

InordertoimplementsuchapropertyinourGoannatool,weonlyneedtoidentifythenodesofinterest(asde-scribedinSection4.1),describetheirrelationshipsinCTLformulasandprinttheseformulasinNuSMVsyntaxtoNuSMV’sinput le(asdescribedinSubsection4.2).AnimplementationofourexamplepropertyisshowninpseudocodeinFigure5.Inthecode,we rst ndthesetofallvariablesthataredeclaredinafunction,becausethesearetheonesthatneedtobecheckedforproperinitialization.Foreachofthesevariables,wethenprinttheCTLspeci -cationstotheNuSMVinput le(thefunctionNuSMV()simplyprintstexttoNuSMV’sinput le).Inthenextstep,foreveryvariableinthesetofdeclaredvariables,wesearchforthesetofnodesintheASTwherethevariableisassignedavalueandwhereitisused,respectively.ForthissearchweusethefunctionFindAST()thatidenti- esnodesintheASTaccordingtospeci cpatterns.Fi-nally,fromthesethreesets,wegetthecorrespondingsetsoflocationsoftherespectivenodesintheCFGbyusingthefunctionCFGlocations().Thatfunctiontranslates