From 07f2bfbd62568e2e0d983ccb33d020bf6985e874 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 29 Mar 2020 18:30:01 +0200 Subject: nop insertion at entrypoint --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 8aa5e98a..ec5e2cd0 100644 --- a/Makefile +++ b/Makefile @@ -94,7 +94,7 @@ BACKEND=\ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ ForwardMoves.v ForwardMovesproof.v \ - FirstNop.v \ + FirstNop.v FirstNopproof.v \ Allnontrap.v Allnontrapproof.v \ Allocation.v Allocproof.v \ Tunneling.v Tunnelingproof.v \ -- cgit From fd00d28f8065acf9b09a6510e1612a91e30ca29c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 10:12:09 +0200 Subject: more on injection --- Makefile | 1 + 1 file changed, 1 insertion(+) (limited to 'Makefile') diff --git a/Makefile b/Makefile index ec5e2cd0..4cf9ccf1 100644 --- a/Makefile +++ b/Makefile @@ -86,6 +86,7 @@ BACKEND=\ Kildall.v Liveness.v \ ValueDomain.v ValueAOp.v ValueAnalysis.v \ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ + Inject.v \ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ CSE2deps.v CSE2depsproof.v \ CSE2.v CSE2proof.v \ -- cgit From 27c8e10f4e0a3eee6bf9feb03d0f12990f74badd Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 18:46:50 +0200 Subject: use inject_l --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 4cf9ccf1..f005d048 100644 --- a/Makefile +++ b/Makefile @@ -86,7 +86,7 @@ BACKEND=\ Kildall.v Liveness.v \ ValueDomain.v ValueAOp.v ValueAnalysis.v \ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ - Inject.v \ + Inject.v Injectproof.v \ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ CSE2deps.v CSE2depsproof.v \ CSE2.v CSE2proof.v \ -- cgit From 6379f6291eea909426f074db67837b04a1dec9ae Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 14:24:05 +0200 Subject: attempt at compiling --- Makefile | 1 + 1 file changed, 1 insertion(+) (limited to 'Makefile') diff --git a/Makefile b/Makefile index f005d048..b7fed0d4 100644 --- a/Makefile +++ b/Makefile @@ -91,6 +91,7 @@ BACKEND=\ CSE2deps.v CSE2depsproof.v \ CSE2.v CSE2proof.v \ CSE3analysis.v CSE3analysisproof.v CSE3.v CSE3proof.v \ + LICM.v LICMproof.v \ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ -- cgit