[M3commit] CVS Update: cm3

[Mika Nystrom]

CVSROOT:	/usr/cvs
Changes by:	mika at birch.	11/03/05 01:50:30

Added files:
	cm3/ESC/Simplify/cgi-utils/: README 
	cm3/ESC/Simplify/cgi-utils/src/: CGITrans.i3 CGITrans.m3 
	                                 HTMLUtils.i3 HTMLUtils.m3 cline 
	                                 m3makefile temp 
	cm3/ESC/Simplify/prover/: README 
	cm3/ESC/Simplify/prover/src/: AF.i3 AF.m3 AFTabUndoRec.i3 
	                              CHANGELOG Clause.i3 Clause.m3 
	                              ClauseList.i3 ClauseList.m3 
	                              ClauseListUndoRec.i3 
	                              ClausePrivate.i3 Context.i3 
	                              Context.m3 ContextPrivate.i3 
	                              ContextUndoRec.i3 Enode.i3 
	                              Enode.m3 FPrint.i3 FPrint.m3 
	                              FPrint31.i3 FPrint31.m3 IdSet.i3 
	                              IntPair.i3 IntPair.m3 LNUndoRec.i3 
	                              LOG LabelName.i3 LabelName.m3 
	                              Match.i3 MatchingRule.i3 
	                              MatchingRule.m3 OrdNode.i3 
	                              OrdNode.m3 Orders.i3 Orders.m3 
	                              PairSet.i3 PairSet.m3 
	                              PairSetBits.i3 PairSetBits.m3 
	                              ParentSet.i3 ParentSet.m3 Perf.i3 
	                              Perf.m3 PredDefs.i3 PredDefs.m3 
	                              PredSx.i3 PredSx.m3 PromoteSet.i3 
	                              PromoteSet.m3 PropVar.i3 
	                              PropVar.m3 Prover.i3 Prover.m3 
	                              ProxyProp.i3 ProxyProp.m3 Rat.i3 
	                              Rat.m3 RefListDebug.i3 
	                              RefListDebug.m3 RefListMisc.i3 
	                              RefListMisc.m3 SHIPLOG Satisfy.i3 
	                              Satisfy.m3 SigTab.i3 SigTab.m3 
	                              Signature.i3 Signature.m3 
	                              Simplex.i3 Simplex.m3 SxPrint.i3 
	                              SxPrint.m3 Trit.i3 Trit.m3 cline 
	                              def.ax esc.ax esc.new.ax esc0.ax 
	                              esc1.ax m3makefile m3overrides 
	                              temp 
	cm3/ESC/Simplify/prover/src/gens/: OrdNodePODiGraph.i3.sav 
	                                   OrdNodePODiGraph.m3.sav 
	                                   m3makefile 
	cm3/ESC/Simplify/prover/test/src/: FPTest.m3 m3makefile 
	                                   m3overrides test1.sx test2.sx 
	                                   test3.sx 
	cm3/ESC/Simplify/simplify/: README 
	cm3/ESC/Simplify/simplify/src/: Simplify.1 Simplify.1.html 
	                                Simplify.1.mtex Simplify.m3 
	                                axioms cline esc-axioms 
	                                html-output1 html-output2 
	                                m3makefile m3overrides manfiles 
	                                temp 
	cm3/ESC/Simplify/simplify/test/: Examples.esc.invalid 
	                                 Examples.esc.valid 
	                                 Examples.esc2.invalid 
	                                 Examples.esc3.valid 
	                                 Examples.invalid Examples.valid 
	                                 Makefile OrdersTest.sx 
	                                 PredTest.esc.sx PredTest.sx 
	                                 README escv1.ax escv2.ax 
	                                 escv3.ax necula1.ax necula1.sx 
	                                 saxe1.ax saxe1.input test.ans 
	                                 test.out 
	cm3/ESC/Simplify/simplify/test/perf/: addhi.sx 
	                                      ast.ArrayRefExpr.toString.sx 
	                                      ast.DefaultVisitor.visitTryCatchStmt.sx 
	                                      cat.sx domino6x4x.sx 
	                                      domino6x6x.sx fastclose.sx 
	                                      frd-seek.sx m3tests 
	                                      parser.Lex.scanNumber.sx 
	                                      parser.Parse.Parse.sx 
	                                      parser.test.TestLex.getNextPragma.sx 
	                                      parser.test.TestLex.main.sx 
	                                      runtests simplex.sx 
	                                      tc.CheckInvariants.checkTypeDeclOfSig.sx 
	                                      tc.FlowInsensitiveChecks.checkTypeDeclElem.sx 
	                                      tc.PrepTypeDeclaration.getRootInterface.sx 
	                                      tc.Types.binaryNumericPromotion.sx 
	                                      tc.Types.isCharType.sx 
	                                      tests 

Log message:
	Initial checkin of Greg Nelson's Simplify theorem prover, used by
	the Modula-3 Extended Static Checker, the Java Extended Static
	Checker, and other programs.
	
	I have verified that the code builds and runs under CM3 but I haven't
	yet adjusted the build system to incorporate the code.
	
	It's in the ESC subdirectory in the hope that HP will release the
	rest of ESC soon.
	
	Copyrights in the files may be misleading: all this code has long
	since been released by DEC/Compaq/HP.
	
	I downloaded it from sort.ucd.ie and made some very minor adjustments
	to get it to build with the current CM3.