"Fossies" - the Fresh Open Source Software Archive  

Source code changes of the file "projects/CodeThorn/src/codethorn.C" between
rose-0.11.53.0.tar.gz and rose-0.11.54.0.tar.gz

About: ROSE is a compiler infrastructure to build source-to-source program transformation and analysis tools for large-scale C, C++, UPC, Fortran, OpenMP, Java, Python and PHP applications.

codethorn.C  (rose-0.11.53.0):codethorn.C  (rose-0.11.54.0)
skipping to change at line 59 skipping to change at line 59
#include "CtxCallStrings.h" // for setting call string options #include "CtxCallStrings.h" // for setting call string options
#include "AnalysisReporting.h" #include "AnalysisReporting.h"
// Z3-based analyser / SSA // Z3-based analyser / SSA
#if HAVE_Z3 #if HAVE_Z3
#include "z3-prover-connection/SSAGenerator.h" #include "z3-prover-connection/SSAGenerator.h"
#include "z3-prover-connection/ReachabilityAnalyzerZ3.h" #include "z3-prover-connection/ReachabilityAnalyzerZ3.h"
#endif #endif
#include "ConstantConditionAnalysis.h" #include "ConstantConditionAnalysis.h"
#include "MemoryViolationAnalysis.h"
#include "ReadWriteTraceAnalysis.h"
#include "CodeThornLib.h" #include "CodeThornLib.h"
#include "LTLThornLib.h" #include "LTLThornLib.h"
#include "CppStdUtilities.h" #include "CppStdUtilities.h"
using namespace std; using namespace std;
using namespace CodeThorn; using namespace CodeThorn;
using namespace boost; using namespace boost;
#include "Rose/Diagnostics.h" #include "Rose/Diagnostics.h"
skipping to change at line 251 skipping to change at line 253
// exit early // exit early
if(ctOpt.status) cout<<color("normal")<<"done."<<endl; if(ctOpt.status) cout<<color("normal")<<"done."<<endl;
exit(0); exit(0);
} }
SAWYER_MESG(logger[INFO])<<"registered string literals: "<<analyzer->getVari ableIdMapping()->numberOfRegisteredStringLiterals()<<endl; SAWYER_MESG(logger[INFO])<<"registered string literals: "<<analyzer->getVari ableIdMapping()->numberOfRegisteredStringLiterals()<<endl;
analyzer->initLabeledAssertNodes(project); analyzer->initLabeledAssertNodes(project);
CodeThorn::optionallyInitializePatternSearchSolver(ctOpt,analyzer,tc); CodeThorn::optionallyInitializePatternSearchSolver(ctOpt,analyzer,tc);
AbstractValue::pointerSetsEnabled=ctOpt.pointerSetsEnabled; AbstractValue::pointerSetsEnabled=ctOpt.pointerSetsEnabled;
if(ctOpt.constantConditionAnalysisFileName.size()>0) { if(ctOpt.constantConditionAnalysisFileName.size()>0) {
analyzer->getEStateTransferFunctions()->setReadWriteListener(new ConstantC analyzer->getEStateTransferFunctions()->registerReadWriteListener(new Cons
onditionAnalysis()); tantConditionAnalysis(),"constant-condition");
}
if(ctOpt.nullPointerAnalysis||ctOpt.generateReports) {
analyzer->getEStateTransferFunctions()->registerReadWriteListener(new Memo
ryViolationAnalysis(),"memory-violation");
}
if(ctOpt.readWriteTrace) {
analyzer->getEStateTransferFunctions()->registerReadWriteListener(new Read
WriteTraceAnalysis(),"read-write-trace");
} }
if(ctOpt.runSolver) { if(ctOpt.runSolver) {
analyzer->runAnalysisPhase2(tc); analyzer->runAnalysisPhase2(tc);
} else { } else {
cout<<"STATUS: skipping solver run."<<endl; cout<<"STATUS: skipping solver run."<<endl;
} }
analyzer->printStatusMessageLine("========================================== ===================="); analyzer->printStatusMessageLine("========================================== ====================");
optionallyWriteSVCompWitnessFile(ctOpt, analyzer); optionallyWriteSVCompWitnessFile(ctOpt, analyzer);
 End of changes. 2 change blocks. 
2 lines changed or deleted 12 lines changed or added

Home  |  About  |  Features  |  All  |  Newest  |  Dox  |  Diffs  |  RSS Feeds  |  Screenshots  |  Comments  |  Imprint  |  Privacy  |  HTTP(S)